← Copula mathematical handbook

The classical characterization of finite-dimensional copulas

Atomic approximations have uniformly convergent CDFs. Compactness of probability measures on the unit cube gives a weakly convergent subsequence. The portmanteau inequalities and the derived Lipschitz estimate identify its CDF, including on the boundary. No continuity or countable-additivity assumption is added.

theorem ProbabilityTheory.Copula.IsClassical.exists_probabilityMeasure {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) : ∃ (μ : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)), ∀ (u : Fin d → ↑unitInterval), (↑μ).real (Set.Iic u) = F u

A classical copula function is the CDF of a probability measure on the cube.

theorem ProbabilityTheory.Copula.IsClassical.existsUnique {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) : ∃! C : Copula d, C.cdf = F

The classical characterization, valid in every finite dimension including zero.

noncomputable def ProbabilityTheory.Copula.ofClassical {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (hF : IsClassical F) : Copula d

Build the unique copula represented by classical boundary and rectangle data.

Equations

• ProbabilityTheory.Copula.ofClassical F hF = Exists.choose ⋯

@[simp]

theorem ProbabilityTheory.Copula.cdf_ofClassical {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (hF : IsClassical F) : (ofClassical F hF).cdf = F

@[simp]

theorem ProbabilityTheory.Copula.ofClassical_cdf {d : ℕ} (C : Copula d) : ofClassical C.cdf ⋯ = C

theorem ProbabilityTheory.Copula.isClassical_iff_existsUnique {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} : IsClassical F ↔ ∃! C : Copula d, C.cdf = F