← Copula mathematical handbook

Sharp upper bounds for the Schweizer–Wolff σ and Hoeffding's Φ²

Nelsen, An Introduction to Copulas, 2nd ed., §5.3.1: the normalized L¹ and L² distances to independence satisfy σ(C) ≤ 1 and Φ²(C) ≤ 1, with equality if and only if C = M or C = W. The uniform version satisfies κ(C) ≤ 1 with equality if and only if |β(C)| = 1.

The proof works sectionwise. For fixed v, the section F(u) = C(u,v) - uv is the primitive of the mean-zero function ∂₁C(·,v) - v. By the primitive comparison lemma (Copula.Rearrangement.PrimitiveIntegral), ∫ |F| ≤ ∫ G and ∫ F² ≤ ∫ G² where G(u) = C↑(u,v) - uv is the section of the SI rearrangement C↑ (upRearr), and the inequalities are strict when F changes sign. Since Π ≤ C↑ ≤ M, 0 ≤ G ≤ M - Π, which gives σ(C) ≤ σ(C↑) ≤ σ(M) = 1 and Φ²(C) ≤ Φ²(C↑) ≤ Φ²(M) = 1. In the equality case almost every section has constant sign and coincides with the section of M (nonnegative case) or of W (nonpositive case); the two cases cannot both occur for sections in (0,1), and continuity in v gives C = M or C = W.

Auxiliary facts on the unit interval

theorem ProbabilityTheory.Copula.integrable_of_continuous_unit {f : ↑unitInterval → ℝ} (hf : Continuous f) : MeasureTheory.Integrable f MeasureTheory.volume

theorem ProbabilityTheory.Copula.integrable_integral_of_continuous {f : ↑unitInterval → ↑unitInterval → ℝ} (hf : Continuous fun (p : ↑unitInterval × ↑unitInterval) => f p.1 p.2) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ∫ (u : ↑unitInterval), f u v) MeasureTheory.volume

A parametric integral of a jointly continuous function is integrable in the parameter.

theorem ProbabilityTheory.Copula.eq_of_le_of_integral_eq_unit {a b : ↑unitInterval → ℝ} (ha : Continuous a) (hb : Continuous b) (hab : ∀ (u : ↑unitInterval), a u ≤ b u) (h : ∫ (u : ↑unitInterval), a u = ∫ (u : ↑unitInterval), b u) : a = b

Two continuous functions a ≤ b on the unit interval with equal integrals coincide.

theorem ProbabilityTheory.Copula.continuous_cdf_pair (C : Copula 2) : Continuous fun (p : ↑unitInterval × ↑unitInterval) => C.cdf ![p.1, p.2]

theorem ProbabilityTheory.Copula.continuous_cdf_section (C : Copula 2) (v : ↑unitInterval) : Continuous fun (u : ↑unitInterval) => C.cdf ![u, v]

theorem ProbabilityTheory.Copula.continuous_cdf_section_right (C : Copula 2) (u : ↑unitInterval) : Continuous fun (v : ↑unitInterval) => C.cdf ![u, v]

theorem ProbabilityTheory.Copula.continuous_cdf_sub_mul_section (C : Copula 2) (v : ↑unitInterval) : Continuous fun (u : ↑unitInterval) => C.cdf ![u, v] - ↑u * ↑v

theorem ProbabilityTheory.Copula.continuous_cdf_sub_mul_pair (C : Copula 2) : Continuous fun (p : ↑unitInterval × ↑unitInterval) => C.cdf ![p.1, p.2] - ↑p.1 * ↑p.2

theorem ProbabilityTheory.Copula.eq_of_ae_section {C D : Copula 2} (h : ∀ᵐ (v : ↑unitInterval), ∀ (u : ↑unitInterval), C.cdf ![u, v] = D.cdf ![u, v]) : C = D

Two bivariate copulas whose v-sections agree for almost every v are equal.

Sections and the SI rearrangement

theorem ProbabilityTheory.Copula.cdf_sub_mul_eq_primDev (C : Copula 2) (u v : ↑unitInterval) : C.cdf ![u, v] - ↑u * ↑v = primDev (C.condSection v) (↑v) u

theorem ProbabilityTheory.Copula.upRearr_cdf_sub_mul_eq_rearrDev (C : Copula 2) (u v : ↑unitInterval) : C.upRearr.cdf ![u, v] - ↑u * ↑v = rearrDev (C.condSection v) (↑v) u

theorem ProbabilityTheory.Copula.mul_le_upRearr_cdf (C : Copula 2) (u v : ↑unitInterval) : ↑u * ↑v ≤ C.upRearr.cdf ![u, v]

theorem ProbabilityTheory.Copula.integral_abs_cdf_sub_mul_le_upRearr (C : Copula 2) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), |C.cdf ![u, v] - ↑u * ↑v| ≤ ∫ (u : ↑unitInterval), C.upRearr.cdf ![u, v] - ↑u * ↑v

Sectionwise L¹ comparison with the SI rearrangement.

theorem ProbabilityTheory.Copula.integral_sq_cdf_sub_mul_le_upRearr (C : Copula 2) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), (C.cdf ![u, v] - ↑u * ↑v) ^ 2 ≤ ∫ (u : ↑unitInterval), (C.upRearr.cdf ![u, v] - ↑u * ↑v) ^ 2

Sectionwise L² comparison with the SI rearrangement.

theorem ProbabilityTheory.Copula.integral_abs_cdf_sub_mul_lt_upRearr (C : Copula 2) (v : ↑unitInterval) {t₁ t₂ : ↑unitInterval} (h₁ : 0 < C.cdf ![t₁, v] - ↑t₁ * ↑v) (h₂ : C.cdf ![t₂, v] - ↑t₂ * ↑v < 0) : ∫ (u : ↑unitInterval), |C.cdf ![u, v] - ↑u * ↑v| < ∫ (u : ↑unitInterval), C.upRearr.cdf ![u, v] - ↑u * ↑v

Strict sectionwise L¹ comparison when the section changes sign.

theorem ProbabilityTheory.Copula.integral_sq_cdf_sub_mul_lt_upRearr (C : Copula 2) (v : ↑unitInterval) {t₁ t₂ : ↑unitInterval} (h₁ : 0 < C.cdf ![t₁, v] - ↑t₁ * ↑v) (h₂ : C.cdf ![t₂, v] - ↑t₂ * ↑v < 0) : ∫ (u : ↑unitInterval), (C.cdf ![u, v] - ↑u * ↑v) ^ 2 < ∫ (u : ↑unitInterval), (C.upRearr.cdf ![u, v] - ↑u * ↑v) ^ 2

Strict sectionwise L² comparison when the section changes sign.

Sectionwise comparison with the Fréchet–Hoeffding bounds

theorem ProbabilityTheory.Copula.cdf_sub_mul_le_comonotonic (C : Copula 2) (u v : ↑unitInterval) : C.cdf ![u, v] - ↑u * ↑v ≤ (comonotonic 2).cdf ![u, v] - ↑u * ↑v

theorem ProbabilityTheory.Copula.comonotonic_cdf_sub_mul_nonneg (u v : ↑unitInterval) : 0 ≤ (comonotonic 2).cdf ![u, v] - ↑u * ↑v

theorem ProbabilityTheory.Copula.mul_sub_countermonotonic_cdf (u v : ↑unitInterval) : ↑u * ↑v - countermonotonic.cdf ![u, v] = (comonotonic 2).cdf ![unitInterval.symm u, v] - ↑(unitInterval.symm u) * ↑v

The section of u v - W(u,v) is the reflected section of M(u,v) - u v.

theorem ProbabilityTheory.Copula.neg_cdf_sub_mul_le (C : Copula 2) (u v : ↑unitInterval) : -(C.cdf ![u, v] - ↑u * ↑v) ≤ (comonotonic 2).cdf ![unitInterval.symm u, v] - ↑(unitInterval.symm u) * ↑v

theorem ProbabilityTheory.Copula.integral_comp_comonotonic_symm (φ : ℝ → ℝ) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), φ ((comonotonic 2).cdf ![unitInterval.symm u, v] - ↑(unitInterval.symm u) * ↑v) = ∫ (u : ↑unitInterval), φ ((comonotonic 2).cdf ![u, v] - ↑u * ↑v)

For a function φ of the deviation, reflecting the first coordinate of the section of M - Π does not change its integral.

theorem ProbabilityTheory.Copula.section_eq_of_integral_comp_eq {φ : ℝ → ℝ} (hφ : Continuous φ) (hmono : ∀ (s t : ℝ), 0 ≤ s → s ≤ t → φ s ≤ φ t) (hinj : ∀ (s t : ℝ), 0 ≤ s → 0 ≤ t → φ s = φ t → s = t) (hneg : ∀ (t : ℝ), φ (-t) = φ t) (C : Copula 2) (v : ↑unitInterval) (hsign : (∀ (u : ↑unitInterval), 0 ≤ C.cdf ![u, v] - ↑u * ↑v) ∨ ∀ (u : ↑unitInterval), C.cdf ![u, v] - ↑u * ↑v ≤ 0) (heq : ∫ (u : ↑unitInterval), φ (C.cdf ![u, v] - ↑u * ↑v) = ∫ (u : ↑unitInterval), φ ((comonotonic 2).cdf ![u, v] - ↑u * ↑v)) : (∀ (u : ↑unitInterval), C.cdf ![u, v] = (comonotonic 2).cdf ![u, v]) ∨ ∀ (u : ↑unitInterval), C.cdf ![u, v] = countermonotonic.cdf ![u, v]

If a monotone, sign-invariant, injective-on-[0,∞) function φ of a constant-sign section of C - Π has the same integral as that of M - Π, then the section is the section of M or of W.

theorem ProbabilityTheory.Copula.not_section_comonotonic_and_countermonotonic (C : Copula 2) {v₁ v₂ : ↑unitInterval} (h₁0 : 0 < ↑v₁) (h₂0 : 0 < ↑v₂) (h₁1 : ↑v₁ < 1) (h₂1 : ↑v₂ < 1) (h₁ : ∀ (u : ↑unitInterval), C.cdf ![u, v₁] = (comonotonic 2).cdf ![u, v₁]) (h₂ : ∀ (u : ↑unitInterval), C.cdf ![u, v₂] = countermonotonic.cdf ![u, v₂]) : False

A section of M in (0,1) and a section of W in (0,1) cannot belong to the same copula.

theorem ProbabilityTheory.Copula.eq_comonotonic_or_countermonotonic_of_ae_section (C : Copula 2) (h : ∀ᵐ (v : ↑unitInterval), (∀ (u : ↑unitInterval), C.cdf ![u, v] = (comonotonic 2).cdf ![u, v]) ∨ ∀ (u : ↑unitInterval), C.cdf ![u, v] = countermonotonic.cdf ![u, v]) : C = comonotonic 2 ∨ C = countermonotonic

If almost every v-section of C is a section of M or of W, then C = M or C = W.

The Schweizer–Wolff σ

theorem ProbabilityTheory.Copula.integral_abs_cdf_sub_mul_le_comonotonic (C : Copula 2) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), |C.cdf ![u, v] - ↑u * ↑v| ≤ ∫ (u : ↑unitInterval), |(comonotonic 2).cdf ![u, v] - ↑u * ↑v|

Sectionwise, the L¹ deviation of C from Π is dominated by that of M.

theorem ProbabilityTheory.Copula.schweizerWolff_le_schweizerWolff_upRearr (C : Copula 2) : C.schweizerWolff ≤ C.upRearr.schweizerWolff

The Schweizer–Wolff measure is dominated by that of the SI rearrangement, σ(C) ≤ σ(C↑) = ρ(C↑).

theorem ProbabilityTheory.Copula.schweizerWolff_le_one (C : Copula 2) : C.schweizerWolff ≤ 1

The Schweizer–Wolff measure is at most one (Nelsen §5.3.1).

theorem ProbabilityTheory.Copula.schweizerWolff_mem_Icc (C : Copula 2) : C.schweizerWolff ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.section_sign_of_integral_abs_eq (C : Copula 2) (v : ↑unitInterval) (h : ∫ (u : ↑unitInterval), |C.cdf ![u, v] - ↑u * ↑v| = ∫ (u : ↑unitInterval), |(comonotonic 2).cdf ![u, v] - ↑u * ↑v|) : (∀ (u : ↑unitInterval), 0 ≤ C.cdf ![u, v] - ↑u * ↑v) ∨ ∀ (u : ↑unitInterval), C.cdf ![u, v] - ↑u * ↑v ≤ 0

A section with the maximal L¹ deviation has constant sign.

theorem ProbabilityTheory.Copula.schweizerWolff_eq_one_iff (C : Copula 2) : C.schweizerWolff = 1 ↔ C = comonotonic 2 ∨ C = countermonotonic

σ(C) = 1 if and only if C is one of the Fréchet–Hoeffding bounds (Nelsen §5.3.1).

Hoeffding's Φ²

theorem ProbabilityTheory.Copula.integral_sq_cdf_sub_mul_le_comonotonic (C : Copula 2) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), (C.cdf ![u, v] - ↑u * ↑v) ^ 2 ≤ ∫ (u : ↑unitInterval), ((comonotonic 2).cdf ![u, v] - ↑u * ↑v) ^ 2

Sectionwise, the L² deviation of C from Π is dominated by that of M.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_le_hoeffdingPhiSq_upRearr (C : Copula 2) : C.hoeffdingPhiSq ≤ C.upRearr.hoeffdingPhiSq

Hoeffding's Φ² is dominated by that of the SI rearrangement.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_le_one (C : Copula 2) : C.hoeffdingPhiSq ≤ 1

Hoeffding's Φ² is at most one (Nelsen §5.3.1).

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_mem_Icc (C : Copula 2) : C.hoeffdingPhiSq ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.section_sign_of_integral_sq_eq (C : Copula 2) (v : ↑unitInterval) (h : ∫ (u : ↑unitInterval), (C.cdf ![u, v] - ↑u * ↑v) ^ 2 = ∫ (u : ↑unitInterval), ((comonotonic 2).cdf ![u, v] - ↑u * ↑v) ^ 2) : (∀ (u : ↑unitInterval), 0 ≤ C.cdf ![u, v] - ↑u * ↑v) ∨ ∀ (u : ↑unitInterval), C.cdf ![u, v] - ↑u * ↑v ≤ 0

A section with the maximal L² deviation has constant sign.

theorem ProbabilityTheory.Copula.hoeffdingPhiSq_eq_one_iff (C : Copula 2) : C.hoeffdingPhiSq = 1 ↔ C = comonotonic 2 ∨ C = countermonotonic

Φ²(C) = 1 if and only if C is one of the Fréchet–Hoeffding bounds (Nelsen §5.3.1).

The uniform distance κ

theorem ProbabilityTheory.Copula.eq_half_of_four_mul_abs_cdf_sub_mul_eq_one (C : Copula 2) {u v : ↑unitInterval} (h : 4 * |C.cdf ![u, v] - ↑u * ↑v| = 1) : ↑u = 1 / 2 ∧ ↑v = 1 / 2

The only point where |C(u,v) - uv| can reach 1/4 is the centre (1/2, 1/2).

theorem ProbabilityTheory.Copula.schweizerWolffKappa_eq_one_iff (C : Copula 2) : C.schweizerWolffKappa = 1 ↔ |C.blomqvistBeta| = 1

κ(C) = 1 if and only if |β(C)| = 1, where β is Blomqvist's beta.

@[simp]

theorem ProbabilityTheory.Copula.schweizerWolffKappa_comonotonic : (comonotonic 2).schweizerWolffKappa = 1

@[simp]

theorem ProbabilityTheory.Copula.schweizerWolffKappa_countermonotonic : countermonotonic.schweizerWolffKappa = 1