Documentation

Papers.Rockel2026XiFootrule.LowerEndpoint

← Mathematical handbook

Theorem 3.4 and the entire bottom boundary #

The checkerboard is identified by its CDF on the whole square. The universal bound and uniqueness follow from the already checked sharp xi-beta theorem and the equivalence between minimal footrule and beta=-1.

source
noncomputable def Papers.Rockel2026XiFootrule.antiCheckerboard :
ProbabilityTheory.Copula 2

The two off-diagonal median cells each have uniform density two.

Equations
Instances For
    source
    theorem Papers.Rockel2026XiFootrule.antiCheckerboard_cdf (u v : ↑unitInterval) :
    antiCheckerboard.cdf ![u, v] = 2 * (min (↑u) (1 / 2) * max 0 (↑v - 1 / 2) + max 0 (↑u - 1 / 2) * min (↑v) (1 / 2))

    Integrated density of the source's two off-diagonal squares.

    source
    theorem Papers.Rockel2026XiFootrule.antiCheckerboard_xi :
    antiCheckerboard.chatterjeeXi = 1 / 2
    source
    theorem Papers.Rockel2026XiFootrule.antiCheckerboard_footrule :
    antiCheckerboard.spearmanFootrule = -1 / 2
    source
    theorem Papers.Rockel2026XiFootrule.xi_lower_bound_at_minimal_footrule (C : ProbabilityTheory.Copula 2) (hC : C.spearmanFootrule = -1 / 2) :
    1 / 2 ≤ C.chatterjeeXi
    source
    theorem Papers.Rockel2026XiFootrule.xi_minimum_at_minimal_footrule_iff (C : ProbabilityTheory.Copula 2) (hC : C.spearmanFootrule = -1 / 2) :
    C.chatterjeeXi = 1 / 2 ↔ C = antiCheckerboard
    source
    theorem Papers.Rockel2026XiFootrule.exact_bottom_boundary (x : ℝ) :
    (∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ C.spearmanFootrule = -1 / 2) ↔ x ∈ Set.Icc (1 / 2) 1

    The bottom boundary is attained exactly for xi in [1/2,1].