Documentation

Papers.OrendayLaresRockel2026XiBeta.SharpBound

← Mathematical handbook

The universal cubic inequality #

The proof uses the two median strips and a one-dimensional tent estimate. All conditional integrals are with respect to the copula's regular kernel; no density or differentiability hypothesis is imposed.

source
noncomputable def Papers.OrendayLaresRockel2026XiBeta.medianDisplacement (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) :
ℝ

Displacement of the conditional distribution on the lower median strip.

Equations
Instances For
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.medianDisplacement_lipschitz (C : ProbabilityTheory.Copula 2) (v w : ↑unitInterval) :
    |medianDisplacement C v - medianDisplacement C w| ≤ |↑v - ↑w|
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.median_strip_energy (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) :
    medianDisplacement C v ^ 2 ≤ (∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2) - ↑v ^ 2

    Jensen's inequality on each half, proved by integrating a square.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.median_energy_le_xi (C : ProbabilityTheory.Copula 2) :
    6 * ∫ (v : ↑unitInterval), medianDisplacement C v ^ 2 ≤ C.chatterjeeXi
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.medianTent_le_abs_displacement (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) :
    Verification.medianTent |C.blomqvistBeta| ↑v ≤ |medianDisplacement C v|

    The beta constraint forces a tent-shaped lower bound on absolute displacement.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.beta_cubic_le_two_xi (C : ProbabilityTheory.Copula 2) :
    |C.blomqvistBeta| ^ 3 ≤ 2 * C.chatterjeeXi

    Proposition 5, inequality part, for every copula including singular laws.