← Copula mathematical handbook

The classical copula conditions

This module states the classical boundary and rectangle conditions and proves them for the CDF of every bundled copula. Normalization is explicit so that dimension zero is covered. The converse is proved in Copula.Classical.Characterization.

structure ProbabilityTheory.Copula.IsClassical {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) : Prop

The classical conditions on a copula function. Continuity is not assumed.

• normalized : (F fun (x : Fin d) => 1) = 1

  The top corner has mass one, including in dimension zero.

• grounded (u : Fin d → ↑unitInterval) (i : Fin d) : u i = 0 → F u = 0

  A zero coordinate makes the function vanish.

• marginal (i : Fin d) (u : ↑unitInterval) : F (Function.update (fun (x : Fin d) => 1) i u) = ↑u

  The one-coordinate boundary faces are uniform.

• increasing (a b : Fin d → ↑unitInterval) : a ≤ b → 0 ≤ rectangleIncrement F a b

  Every ordered rectangle has a nonnegative increment.

theorem ProbabilityTheory.Copula.isClassical_cdf {d : ℕ} (C : Copula d) : IsClassical C.cdf

Every measure-based copula satisfies the classical copula conditions.

theorem ProbabilityTheory.Copula.unique_representation {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) {C D : Copula d} (hC : C.cdf = F) (hD : D.cdf = F) : C = D

There can be at most one copula measure representing a given function.

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

Turn a probability-measure representation of classical CDF data into a copula. This is the marginal-identification step; it does not assume or assert an extension theorem.

Equations

• hF.ofMeasure μ hμ = { measure := μ, marginal_eq := ⋯ }

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

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

In the empty dimension the classical characterization is complete.

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

In dimension one the classical conditions force the uniform CDF.