← Copula mathematical handbook

Finite probability measures approximating classical copula data

Successive binary cuts produce finite atomic measures. Rectangle additivity normalizes their weights, and clipping rectangles proves a uniform CDF error bound in terms of the mesh width.

theorem ProbabilityTheory.Copula.IsClassical.rectangleIncrement_clip_le {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (a b u : Fin d → ↑unitInterval) (hab : a ≤ b) : rectangleIncrement F (a ⊓ u) (b ⊓ u) ≤ rectangleIncrement F a b

inductive ProbabilityTheory.Copula.ClassicalConstruction.Division {d : ℕ} : (Fin d → ↑unitInterval) → (Fin d → ↑unitInterval) → Type

A finite division built by cuts along coordinate hyperplanes.

• leaf {d : ℕ} {a b : Fin d → ↑unitInterval} (hab : a ≤ b) : Division a b
• cut {d : ℕ} {a b : Fin d → ↑unitInterval} (i : Fin d) (t : ↑unitInterval) (hat : a i ≤ t) (htb : t ≤ b i) (left : Division a (Function.update b i t)) (right : Division (Function.update a i t) b) : Division a b

theorem ProbabilityTheory.Copula.ClassicalConstruction.Division.ordered {d : ℕ} {a b : Fin d → ↑unitInterval} (D : Division a b) : a ≤ b

def ProbabilityTheory.Copula.ClassicalConstruction.Division.All {d : ℕ} (P : (Fin d → ↑unitInterval) → (Fin d → ↑unitInterval) → Prop) {a b : Fin d → ↑unitInterval} : Division a b → Prop

A property holding on every leaf of a division.

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.ClassicalConstruction.Division.All P (ProbabilityTheory.Copula.ClassicalConstruction.Division.leaf hab) = P x✝¹ x✝

theorem ProbabilityTheory.Copula.ClassicalConstruction.Division.All.mono {d : ℕ} {a b : Fin d → ↑unitInterval} {P Q : (Fin d → ↑unitInterval) → (Fin d → ↑unitInterval) → Prop} {D : Division a b} (h : All P D) (hPQ : ∀ (a b : Fin d → ↑unitInterval), P a b → Q a b) : All Q D

noncomputable def ProbabilityTheory.Copula.ClassicalConstruction.Division.measure {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) {a b : Fin d → ↑unitInterval} : Division a b → MeasureTheory.Measure (Fin d → ↑unitInterval)

Put each rectangle's weight at its upper corner.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.ClassicalConstruction.Division.measure_univ {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} {a b : Fin d → ↑unitInterval} (hF : IsClassical F) (D : Division a b) : (measure F D) Set.univ = ENNReal.ofReal (rectangleIncrement F a b)

theorem ProbabilityTheory.Copula.ClassicalConstruction.Division.measure_Iic_le {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} {a b : Fin d → ↑unitInterval} (hF : IsClassical F) (D : Division a b) (u : Fin d → ↑unitInterval) : (measure F D) (Set.Iic u) ≤ ENNReal.ofReal (rectangleIncrement F (a ⊓ u) (b ⊓ u))

theorem ProbabilityTheory.Copula.ClassicalConstruction.Division.le_measure_Iic {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} {a b : Fin d → ↑unitInterval} (hF : IsClassical F) (D : Division a b) {ε : ℝ} (hmesh : All (fun (a b : Fin d → ↑unitInterval) => ∀ (i : Fin d), ↑(b i) - ↑(a i) ≤ ε) D) (u w : Fin d → ↑unitInterval) (hw : ∀ (i : Fin d), w i = 0 ∨ ↑(w i) + ε ≤ ↑(u i)) : ENNReal.ofReal (rectangleIncrement F (a ⊓ w) (b ⊓ w)) ≤ (measure F D) (Set.Iic u)

noncomputable def ProbabilityTheory.Copula.ClassicalConstruction.Division.grid {d : ℕ} (l : List (Fin d)) (a b : Fin d → ↑unitInterval) (hab : a ≤ b) : Division a b

Repeated bisection in the coordinates listed in l.

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.Copula.ClassicalConstruction.Division.grid [] a b hab = ProbabilityTheory.Copula.ClassicalConstruction.Division.leaf hab

theorem ProbabilityTheory.Copula.ClassicalConstruction.Division.grid_mesh {d : ℕ} (l : List (Fin d)) (a b : Fin d → ↑unitInterval) (hab : a ≤ b) : All (fun (x y : Fin d → ↑unitInterval) => ∀ (i : Fin d), ↑(y i) - ↑(x i) ≤ (↑(b i) - ↑(a i)) * (1 / 2) ^ List.count i l) (grid l a b hab)

noncomputable def ProbabilityTheory.Copula.ClassicalConstruction.probability {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (D : Division (fun (x : Fin d) => 0) fun (x : Fin d) => 1) : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)

A finite probability measure attached to a division of the whole cube.

Equations

• ProbabilityTheory.Copula.ClassicalConstruction.probability hF D = ⟨ProbabilityTheory.Copula.ClassicalConstruction.Division.measure F D, ⋯⟩

theorem ProbabilityTheory.Copula.ClassicalConstruction.cdf_probability_bounds {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (D : Division (fun (x : Fin d) => 0) fun (x : Fin d) => 1) {ε : ℝ} (hε : 0 ≤ ε) (hmesh : Division.All (fun (a b : Fin d → ↑unitInterval) => ∀ (i : Fin d), ↑(b i) - ↑(a i) ≤ ε) D) (u : Fin d → ↑unitInterval) : F u - ↑d * ε ≤ (↑(probability hF D)).real (Set.Iic u) ∧ (↑(probability hF D)).real (Set.Iic u) ≤ F u

noncomputable def ProbabilityTheory.Copula.ClassicalConstruction.approximation {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (n : ℕ) : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)

The dyadic atomic approximation of classical CDF data.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.ClassicalConstruction.approximation_bounds {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (n : ℕ) (u : Fin d → ↑unitInterval) : F u - ↑d * (1 / 2) ^ n ≤ (↑(approximation hF n)).real (Set.Iic u) ∧ (↑(approximation hF n)).real (Set.Iic u) ≤ F u

theorem ProbabilityTheory.Copula.ClassicalConstruction.approximation_cdf_tendsto {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (u : Fin d → ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => (↑(approximation hF n)).real (Set.Iic u)) Filter.atTop (nhds (F u))

CDFs of the finite atomic approximations converge to the classical function.