← Copula mathematical handbook

Uniform convergence of copula distribution functions

Every copula CDF is d-Lipschitz for the maximum metric on the cube (Copula.lipschitzWith_cdf). Hence any family of copula CDFs is uniformly equicontinuous, and by the Arzelà–Ascoli theorem of mathlib, pointwise convergence of copula CDFs along a filter is automatically uniform on the compact cube. The starting point is Nelsen, An Introduction to Copulas, 2nd ed., Theorem 2.2.4 (the Lipschitz condition, §2.2).

theorem ProbabilityTheory.Copula.IsClassical.abs_sub_le_dim_mul_dist {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (u v : Fin d → ↑unitInterval) : |F u - F v| ≤ ↑d * dist u v

The Lipschitz estimate of a function satisfying the classical copula conditions, stated with the real constant d.

theorem ProbabilityTheory.Copula.abs_cdf_sub_le_dim_mul_dist {d : ℕ} (C : Copula d) (u v : Fin d → ↑unitInterval) : |C.cdf u - C.cdf v| ≤ ↑d * dist u v

The Lipschitz estimate of a copula CDF, stated with the real constant d.

theorem ProbabilityTheory.Copula.uniformEquicontinuous_of_isClassical {d : ℕ} {ι : Type u_1} {G : ι → (Fin d → ↑unitInterval) → ℝ} (hG : ∀ (n : ι), IsClassical (G n)) : UniformEquicontinuous G

Any family of functions satisfying the classical copula conditions is uniformly equicontinuous on the cube.

theorem ProbabilityTheory.Copula.uniformEquicontinuous_cdf {d : ℕ} {ι : Type u_1} (C : ι → Copula d) : UniformEquicontinuous fun (n : ι) => (C n).cdf

Any family of copula CDFs is uniformly equicontinuous on the cube (consequence of Nelsen, Theorem 2.2.4).

theorem ProbabilityTheory.Copula.equicontinuous_cdf {d : ℕ} {ι : Type u_1} (C : ι → Copula d) : Equicontinuous fun (n : ι) => (C n).cdf

Any family of copula CDFs is equicontinuous on the cube.

theorem ProbabilityTheory.Copula.tendstoUniformly_cdf_of_tendsto {d : ℕ} {ι : Type u_1} {l : Filter ι} (C : ι → Copula d) (D : Copula d) (h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))) : TendstoUniformly (fun (n : ι) => (C n).cdf) D.cdf l

Pointwise convergence of copula CDFs along a filter implies uniform convergence on the cube (Nelsen, §2.2, via Theorem 2.2.4).

theorem ProbabilityTheory.Copula.tendstoUniformly_cdf_iff {d : ℕ} {ι : Type u_1} {l : Filter ι} (C : ι → Copula d) (D : Copula d) : TendstoUniformly (fun (n : ι) => (C n).cdf) D.cdf l ↔ ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))

Pointwise and uniform convergence of copula CDFs along a filter coincide.

theorem ProbabilityTheory.Copula.tendstoUniformly_cdf_atTop {d : ℕ} {C : ℕ → Copula d} {D : Copula d} (h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => (C n).cdf u) Filter.atTop (nhds (D.cdf u))) : TendstoUniformly (fun (n : ℕ) => (C n).cdf) D.cdf Filter.atTop

Sequence version: pointwise convergence of copula CDFs is uniform.