← Copula mathematical handbook

The sharp lower rho–footrule boundary

The lower boundary of Kokol Bukovšek–Stopar is certified by a truncated quadratic potential. Its parameter is the width of the central diagonal block of a Bertino copula.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerPotential (r u : ℝ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerPotential r u = max 0 (|2 * u - 1| ^ 2 - r * |2 * u - 1|) / 2

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.continuous_lowerPotential (r : ℝ) : Continuous (lowerPotential r)

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerPotential_feasible {r : ℝ} (hr : 0 ≤ r) (u v : ℝ) : (u - v) ^ 2 - r * |u - v| ≤ lowerPotential r u + lowerPotential r v

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.integral_truncated_quadratic (r : ↑unitInterval) : ∫ (u : ↑unitInterval), max 0 (↑u ^ 2 - ↑r * ↑u) = 1 / 3 - ↑r / 2 + ↑r ^ 3 / 6

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerPotential_integral (r : ↑unitInterval) : ∫ (u : ↑unitInterval), lowerPotential ↑r ↑u = 1 / 6 - ↑r / 4 + ↑r ^ 3 / 12

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lower_support (C : Copula 2) (r : ↑unitInterval) : -1 + ↑r * (1 + 2 * C.spearmanFootrule) - ↑r ^ 3 ≤ C.spearmanRho

Every parameter supplies a global supporting lower bound.

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerBoundary (p : ℝ) : ℝ

The sharp lower boundary, using a square-root parameter rather than real powers.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerBoundary p = -1 + 2 * √((1 + 2 * p) / 3) ^ 3

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerParameter (p : ℝ) (hp : p ∈ Set.Icc (-1 / 2) 1) : ↑unitInterval

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerParameter p hp = ⟨√((1 + 2 * p) / 3), ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lower_bound (C : Copula 2) : lowerBoundary C.spearmanFootrule ≤ C.spearmanRho

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerCopula (r : ↑unitInterval) : Copula 2

A central comonotonic block with countermonotonic outer pieces.

Equations

• ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerCopula r = (ProbabilityTheory.Copula.RankRegion.centered ProbabilityTheory.Copula.countermonotonic r).reflect {1}

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerCopula_coefficients (r : ↑unitInterval) : (lowerCopula r).spearmanFootrule = -1 / 2 + 3 / 2 * ↑r ^ 2 ∧ (lowerCopula r).spearmanRho = -1 + 2 * ↑r ^ 3

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerBoundary_attained {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) : ∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.spearmanRho = lowerBoundary p

The sharp lower boundary is attained at every admissible footrule value.

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerCopula_minimizes_rho (r : ↑unitInterval) (C : Copula 2) (hp : C.spearmanFootrule = (lowerCopula r).spearmanFootrule) : (lowerCopula r).spearmanRho ≤ C.spearmanRho

Global minimality of each constructed lower-boundary copula.