← Copula mathematical handbook

Uniform CDF distance and exchangeability asymmetry

The uniform distance is the supremum of the pointwise absolute CDF difference. uniformMetricSpace bundles its metric laws without imposing a global topology instance on copulas. The bivariate exchangeability defect compares a copula with its transpose.

noncomputable def ProbabilityTheory.Copula.cdfContinuousMap {d : ℕ} (C : Copula d) : C(Fin d → ↑unitInterval, ℝ)

The CDF bundled as a continuous function on the compact cube.

Equations

• C.cdfContinuousMap = { toFun := C.cdf, continuous_toFun := ⋯ }

theorem ProbabilityTheory.Copula.cdfContinuousMap_injective {d : ℕ} : Function.Injective cdfContinuousMap

noncomputable def ProbabilityTheory.Copula.uniformCDFDistance {d : ℕ} (C D : Copula d) : ℝ

Uniform (supremum) distance between two copula CDFs.

Equations

• C.uniformCDFDistance D = dist C.cdfContinuousMap D.cdfContinuousMap

@[instance_reducible]

noncomputable def ProbabilityTheory.Copula.uniformMetricSpace (d : ℕ) : MetricSpace (Copula d)

The uniform metric, available as a local instance when needed.

Equations

• ProbabilityTheory.Copula.uniformMetricSpace d = MetricSpace.induced ProbabilityTheory.Copula.cdfContinuousMap ⋯ inferInstance

theorem ProbabilityTheory.Copula.uniformCDFDistance_eq_iSup {d : ℕ} (C D : Copula d) : C.uniformCDFDistance D = ⨆ (u : Fin d → ↑unitInterval), |C.cdf u - D.cdf u|

theorem ProbabilityTheory.Copula.uniformCDFDistance_nonneg {d : ℕ} (C D : Copula d) : 0 ≤ C.uniformCDFDistance D

theorem ProbabilityTheory.Copula.uniformCDFDistance_comm {d : ℕ} (C D : Copula d) : C.uniformCDFDistance D = D.uniformCDFDistance C

@[simp]

theorem ProbabilityTheory.Copula.uniformCDFDistance_self {d : ℕ} (C : Copula d) : C.uniformCDFDistance C = 0

theorem ProbabilityTheory.Copula.uniformCDFDistance_eq_zero_iff {d : ℕ} (C D : Copula d) : C.uniformCDFDistance D = 0 ↔ C = D

theorem ProbabilityTheory.Copula.tendsto_uniformCDFDistance_iff {d : ℕ} {α : Type u_1} (F : α → Copula d) (C : Copula d) (l : Filter α) : Filter.Tendsto (fun (a : α) => (F a).uniformCDFDistance C) l (nhds 0) ↔ TendstoUniformly (fun (a : α) => (F a).cdf) C.cdf l

Convergence in the uniform distance is precisely uniform convergence of CDFs.

theorem ProbabilityTheory.Copula.uniformCDFDistance_triangle {d : ℕ} (C D E : Copula d) : C.uniformCDFDistance E ≤ C.uniformCDFDistance D + D.uniformCDFDistance E

theorem ProbabilityTheory.Copula.abs_cdf_sub_le_uniformCDFDistance {d : ℕ} (C D : Copula d) (u : Fin d → ↑unitInterval) : |C.cdf u - D.cdf u| ≤ C.uniformCDFDistance D

theorem ProbabilityTheory.Copula.uniformCDFDistance_le_iff {d : ℕ} (C D : Copula d) (r : ℝ) : C.uniformCDFDistance D ≤ r ↔ ∀ (u : Fin d → ↑unitInterval), |C.cdf u - D.cdf u| ≤ r

theorem ProbabilityTheory.Copula.uniformCDFDistance_le_one {d : ℕ} (C D : Copula d) : C.uniformCDFDistance D ≤ 1

theorem ProbabilityTheory.Copula.uniformCDFDistance_le_half (C D : Copula 2) : C.uniformCDFDistance D ≤ 1 / 2

The diameter of bivariate copulas in the uniform metric is at most one half.

@[simp]

theorem ProbabilityTheory.Copula.uniformCDFDistance_comonotonic_countermonotonic : (comonotonic 2).uniformCDFDistance countermonotonic = 1 / 2

The two Fréchet extremes attain the bivariate diameter.

theorem ProbabilityTheory.Copula.uniformCDFDistance_mix_le {d : ℕ} (C D E F : Copula d) (a : ↑unitInterval) : (C.mix D a).uniformCDFDistance (E.mix F a) ≤ ↑a * C.uniformCDFDistance E + (1 - ↑a) * D.uniformCDFDistance F

theorem ProbabilityTheory.Copula.uniformCDFDistance_transpose (C D : Copula 2) : C.transpose.uniformCDFDistance D.transpose = C.uniformCDFDistance D

noncomputable def ProbabilityTheory.Copula.exchangeabilityDefect (C : Copula 2) : ℝ

The unnormalized uniform exchangeability defect sup |C(u,v)-C(v,u)|.

Equations

• C.exchangeabilityDefect = C.uniformCDFDistance C.transpose

theorem ProbabilityTheory.Copula.exchangeabilityDefect_nonneg (C : Copula 2) : 0 ≤ C.exchangeabilityDefect

theorem ProbabilityTheory.Copula.exchangeabilityDefect_eq_zero_iff (C : Copula 2) : C.exchangeabilityDefect = 0 ↔ C.IsExchangeable

@[simp]

theorem ProbabilityTheory.Copula.exchangeabilityDefect_transpose (C : Copula 2) : C.transpose.exchangeabilityDefect = C.exchangeabilityDefect

theorem ProbabilityTheory.Copula.exchangeabilityDefect_mix_le (C D : Copula 2) (a : ↑unitInterval) : (C.mix D a).exchangeabilityDefect ≤ ↑a * C.exchangeabilityDefect + (1 - ↑a) * D.exchangeabilityDefect

@[simp]

theorem ProbabilityTheory.Copula.exchangeabilityDefect_independence : (independence 2).exchangeabilityDefect = 0

@[simp]

theorem ProbabilityTheory.Copula.exchangeabilityDefect_comonotonic : (comonotonic 2).exchangeabilityDefect = 0

@[simp]

theorem ProbabilityTheory.Copula.exchangeabilityDefect_countermonotonic : countermonotonic.exchangeabilityDefect = 0

theorem ProbabilityTheory.Copula.exchangeabilityDefect_le_third (C : Copula 2) : C.exchangeabilityDefect ≤ 1 / 3

The universal one-third bound for the unnormalized exchangeability defect.