← Mathematical handbook

A sharp quadratic certificate for clamped conditional distributions

A clamped affine conditional CDF with slope -b uniquely maximizes b * rho - xi. The quantitative remainder controls the squared conditional CDF distance, and applies to every competing copula, including singular laws.

noncomputable def Verification.unitClamp (x : ℝ) : ℝ

Projection to the closed unit interval.

Equations

• Verification.unitClamp x = min 1 (max 0 x)

theorem Verification.unitClamp_mem (x : ℝ) : unitClamp x ∈ Set.Icc 0 1

theorem Verification.unitClamp_projection (z x : ℝ) (hx : x ∈ Set.Icc 0 1) : 0 ≤ (x - unitClamp z) * (unitClamp z - z)

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

theorem Verification.integrable_rho_section (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => (1 - ↑u) * C.conditionalCDF u v) MeasureTheory.volume

theorem Verification.integrable_rho_profile (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => ∫ (u : ↑unitInterval), (1 - ↑u) * C.conditionalCDF u v) MeasureTheory.volume

theorem Verification.rho_conditional_formula (C : ProbabilityTheory.Copula 2) : C.spearmanRho = (12 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), (1 - ↑u) * C.conditionalCDF u v) - 3

theorem Verification.clamped_rho_distance_bound (C D : ProbabilityTheory.Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => unitClamp (a - b * ↑u)) : 6 * C.conditionalCDFDistanceSq D ≤ C.chatterjeeXi - D.chatterjeeXi - b * (C.spearmanRho - D.spearmanRho)

Quantitative sharp support inequality, without a density restriction.

theorem Verification.clamped_rho_support (C D : ProbabilityTheory.Copula 2) (b : ℝ) (hD : ∀ᵐ (v : ↑unitInterval), ∃ (a : ℝ), (fun (u : ↑unitInterval) => D.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => unitClamp (a - b * ↑u)) : b * C.spearmanRho - C.chatterjeeXi ≤ b * D.spearmanRho - D.chatterjeeXi

theorem Verification.clamped_rho_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) => unitClamp (a - b * ↑u)) : b * C.spearmanRho - C.chatterjeeXi = b * D.spearmanRho - D.chatterjeeXi ↔ C = D