← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_quadratic_certificate (a b t x : ℝ) (hx : x ∈ Set.Icc 0 1) : (x - Common.unitClamp (a + b * (1 - t) ^ 2)) ^ 2 ≤ x ^ 2 - 2 * b * (1 - t) ^ 2 * x - (Common.unitClamp (a + b * (1 - t) ^ 2) ^ 2 - 2 * b * (1 - t) ^ 2 * Common.unitClamp (a + b * (1 - t) ^ 2)) + -2 * a * (x - Common.unitClamp (a + b * (1 - t) ^ 2))

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.clamped_blest_distance_bound (C D : Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (a + b * (1 - ↑u) ^ 2)) : 6 * C.conditionalCDFDistanceSq D ≤ C.chatterjeeXi - D.chatterjeeXi - b * (blestNu C - blestNu D)

Quantitative sharp support inequality, without a density restriction.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.clamped_blest_support (C D : Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (a + b * (1 - ↑u) ^ 2)) : b * blestNu C - C.chatterjeeXi ≤ b * blestNu D - D.chatterjeeXi

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.clamped_blest_support_eq_iff (C D : Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Common.unitClamp (a + b * (1 - ↑u) ^ 2)) : b * blestNu C - C.chatterjeeXi = b * blestNu D - D.chatterjeeXi ↔ C = D