← Mathematical handbook

theorem Papers.Rockel2026XiBlest.blest_quadratic_certificate (a b t x : ℝ) (hx : x ∈ Set.Icc 0 1) : (x - Verification.unitClamp (a + b * (1 - t) ^ 2)) ^ 2 ≤ x ^ 2 - 2 * b * (1 - t) ^ 2 * x - (Verification.unitClamp (a + b * (1 - t) ^ 2) ^ 2 - 2 * b * (1 - t) ^ 2 * Verification.unitClamp (a + b * (1 - t) ^ 2)) + -2 * a * (x - Verification.unitClamp (a + b * (1 - t) ^ 2))

theorem Papers.Rockel2026XiBlest.clamped_blest_distance_bound (C D : ProbabilityTheory.Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.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 Papers.Rockel2026XiBlest.clamped_blest_support (C D : ProbabilityTheory.Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.unitClamp (a + b * (1 - ↑u) ^ 2)) : b * blestNu C - C.chatterjeeXi ≤ b * blestNu D - D.chatterjeeXi

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