← Copula mathematical handbook

Continuity of rank coefficients under convergence of copulas

If a family of bivariate copulas converges pointwise to a copula D, then Spearman's rho, Kendall's tau, Blomqvist's beta, Gini's gamma and Spearman's footrule converge to the corresponding coefficients of D. This is the continuity axiom in Scarsini's definition of a measure of concordance (Nelsen, An Introduction to Copulas, 2nd ed., Definition 5.1.7, property 7).

Pointwise convergence of copula CDFs is uniform (tendstoUniformly_cdf_of_tendsto). The linear coefficients follow from dominated convergence. For Kendall's tau the integrand and the integrating measure both move; we split ∫ Cₙ dCₙ = ∫ (Cₙ - D) dCₙ + ∫ Cₙ dD, using the symmetry of the concordance integral (integral_cdf_swap), and control the first term by the uniform distance.

theorem ProbabilityTheory.Copula.tendsto_integral_cdf_of_tendsto {ι : Type u_1} {l : Filter ι} {d : ℕ} [l.IsCountablyGenerated] (C : ι → Copula d) (D : Copula d) (h : ∀ (u : Fin d → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))) (μ : MeasureTheory.Measure (Fin d → ↑unitInterval)) [MeasureTheory.IsFiniteMeasure μ] : Filter.Tendsto (fun (n : ι) => ∫ (x : Fin d → ↑unitInterval), (C n).cdf x ∂μ) l (nhds (∫ (x : Fin d → ↑unitInterval), D.cdf x ∂μ))

Integrals of copula CDFs against a fixed finite measure converge under pointwise convergence of the copulas.

theorem ProbabilityTheory.Copula.tendsto_spearmanRho_of_tendsto {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (C : ι → Copula 2) (D : Copula 2) (h : ∀ (u : Fin 2 → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))) : Filter.Tendsto (fun (n : ι) => (C n).spearmanRho) l (nhds D.spearmanRho)

Spearman's rho is continuous under pointwise convergence of copulas.

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

Blomqvist's beta is continuous under pointwise convergence of copulas.

theorem ProbabilityTheory.Copula.tendsto_spearmanFootrule_of_tendsto {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (C : ι → Copula 2) (D : Copula 2) (h : ∀ (u : Fin 2 → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))) : Filter.Tendsto (fun (n : ι) => (C n).spearmanFootrule) l (nhds D.spearmanFootrule)

Spearman's footrule is continuous under pointwise convergence of copulas.

theorem ProbabilityTheory.Copula.tendsto_giniGamma_of_tendsto {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (C : ι → Copula 2) (D : Copula 2) (h : ∀ (u : Fin 2 → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))) : Filter.Tendsto (fun (n : ι) => (C n).giniGamma) l (nhds D.giniGamma)

Gini's gamma is continuous under pointwise convergence of copulas.

theorem ProbabilityTheory.Copula.tendsto_kendallTau_of_tendsto {ι : Type u_1} {l : Filter ι} [l.IsCountablyGenerated] (C : ι → Copula 2) (D : Copula 2) (h : ∀ (u : Fin 2 → ↑unitInterval), Filter.Tendsto (fun (n : ι) => (C n).cdf u) l (nhds (D.cdf u))) : Filter.Tendsto (fun (n : ι) => (C n).kendallTau) l (nhds D.kendallTau)

Kendall's tau is continuous under pointwise convergence of copulas.