← Copula mathematical handbook

The lower Fréchet–Hoeffding bound is pointwise best possible

Nelsen 2006, §2.10. For every d and every point u ∈ [0,1]^d there is a d-copula C with C(u) = W_d(u) = max(0, ∑ uᵢ - d + 1). Consequently W_d is the pointwise infimum of all d-copulas (lowerFrechetBound_eq_iInf), although for d ≥ 3 it is not itself a copula (Copula.Multivariate.LowerBound), and for d ≥ 3 there is no smallest d-copula (not_exists_least_copula).

Construction

Put ℓᵢ = 1 - uᵢ and the cumulative offsets aᵢ = ℓ₀ + ⋯ + ℓᵢ₋₁. For V uniform on (0,1] the coordinates Uᵢ = 1 - frac(V - aᵢ) are uniform (cyclicShift, map_cyclicShift), and the events {Uᵢ > uᵢ} = {frac(V - aᵢ) < ℓᵢ} are consecutive arcs of length ℓᵢ on the circle ℝ/ℤ. They are disjoint when ∑ ℓᵢ ≤ 1 and cover the circle otherwise, so P(U ≤ u) = max(0, 1 - ∑ ℓᵢ) = W_d(u). This is a cyclic version of Nelsen's proof (which uses the same disjoint-or-covering arrangement of the events {Uᵢ > uᵢ}).

Uniformity of cyclic shifts

noncomputable def ProbabilityTheory.Copula.cyclicShift (a v : ℝ) : ↑unitInterval

The cyclic shift v ↦ 1 - frac(v - a), with values in (0, 1].

Equations

• ProbabilityTheory.Copula.cyclicShift a v = ⟨1 - Int.fract (v - a), ⋯⟩

theorem ProbabilityTheory.Copula.measurable_cyclicShift (a : ℝ) : Measurable (cyclicShift a)

noncomputable def ProbabilityTheory.Copula.unitIocMeasure : MeasureTheory.ProbabilityMeasure ℝ

Uniform distribution on (0, 1], as a probability measure on ℝ.

Equations

• ProbabilityTheory.Copula.unitIocMeasure = ⟨MeasureTheory.volume.restrict (Set.Ioc 0 1), ProbabilityTheory.Copula.unitIocMeasure._proof_1⟩

theorem ProbabilityTheory.Copula.map_cyclicShift (a : ℝ) : MeasureTheory.Measure.map (cyclicShift a) ↑unitIocMeasure = MeasureTheory.volume

Cyclic shifts preserve the uniform distribution.

Consecutive arcs

noncomputable def ProbabilityTheory.Copula.cyclicOffset {d : ℕ} (ℓ : Fin d → ℝ) (n : ℕ) : ℝ

The cumulative offsets aₙ = ∑_{j < n} ℓⱼ.

Equations

• ProbabilityTheory.Copula.cyclicOffset ℓ n = ∑ j : Fin d with ↑j < n, ℓ j

theorem ProbabilityTheory.Copula.exists_fract_lt_iff {d : ℕ} {ℓ : Fin d → ℝ} (hℓ0 : ∀ (i : Fin d), 0 ≤ ℓ i) (hℓ1 : ∀ (i : Fin d), ℓ i ≤ 1) {v : ℝ} (hv0 : 0 ≤ v) (hv1 : v < 1) : (∃ (i : Fin d), Int.fract (v - cyclicOffset ℓ ↑i) < ℓ i) ↔ v < ∑ i : Fin d, ℓ i

Consecutive arcs. For v ∈ (0,1), some frac(v - aᵢ) is below ℓᵢ exactly when v < ∑ ℓᵢ.

The attaining copula

noncomputable def ProbabilityTheory.Copula.lowerBoundWitness {d : ℕ} (u : Fin d → ↑unitInterval) : Copula d

The cyclic copula attaining W_d at the point u: the law of (1 - frac(V - aᵢ))ᵢ with aᵢ = ∑_{j<i} (1 - uⱼ) and V uniform.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.cdf_lowerBoundWitness {d : ℕ} (u : Fin d → ↑unitInterval) : (lowerBoundWitness u).cdf u = lowerFrechetBound d u

Nelsen 2006, §2.10: the witness copula attains the lower bound at u.

theorem ProbabilityTheory.Copula.exists_cdf_eq_lowerFrechetBound {d : ℕ} (u : Fin d → ↑unitInterval) : ∃ (C : Copula d), C.cdf u = lowerFrechetBound d u

Nelsen 2006, §2.10: for every u some d-copula attains W_d(u).

theorem ProbabilityTheory.Copula.lowerFrechetBound_eq_iInf {d : ℕ} (u : Fin d → ↑unitInterval) : lowerFrechetBound d u = ⨅ (C : Copula d), C.cdf u

W_d is the pointwise infimum of all d-copulas.

theorem ProbabilityTheory.Copula.not_exists_least_copula {d : ℕ} (hd : 3 ≤ d) : ¬∃ (C : Copula d), ∀ (D : Copula d), C.LowerOrthantLE D

For d ≥ 3 there is no smallest d-copula in the pointwise order.