Documentation

Papers.Rockel2026XiFootrule.RegionGeometry

← Mathematical handbook

Attainment and convexity in Theorem 3.3 #

Centered countermonotonic blocks attain every footrule value at xi=1. Mixtures then fill fixed-footrule intervals and prove convexity of the whole region. This does not assume or claim closure of the region.

source
def Papers.Rockel2026XiFootrule.attainableRegion :
Set (ℝ × ℝ)

Equation (24), with the universal coefficient ranges implicit in Copula.

Equations
Instances For
    source
    noncomputable def Papers.Rockel2026XiFootrule.rightBoundary (a : ↑unitInterval) :
    ProbabilityTheory.Copula 2

    A shuffle-of-min witness: a central W block and identity outside it.

    Equations
    Instances For
      source
      theorem Papers.Rockel2026XiFootrule.rightBoundary_coefficients (a : ↑unitInterval) :
      (rightBoundary a).chatterjeeXi = 1 ∧ (rightBoundary a).spearmanFootrule = 1 - 3 / 2 * ↑a ^ 2
      source
      theorem Papers.Rockel2026XiFootrule.xi_one_slice (y : ℝ) :
      (∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = 1 ∧ C.spearmanFootrule = y) ↔ y ∈ Set.Icc (-1 / 2) 1

      Every footrule in its entire admissible interval occurs with xi=1.

      source
      theorem Papers.Rockel2026XiFootrule.fixed_footrule_intermediate (C D : ProbabilityTheory.Copula 2) (he : C.spearmanFootrule = D.spearmanFootrule) (x : ℝ) (hC : C.chatterjeeXi ≤ x) (hD : x ≤ D.chatterjeeXi) :
      ∃ (E : ProbabilityTheory.Copula 2), E.chatterjeeXi = x ∧ E.spearmanFootrule = C.spearmanFootrule

      Equation (26): the fixed-footrule slice contains all intermediate xi values.

      source
      theorem Papers.Rockel2026XiFootrule.fixed_footrule_upward (C : ProbabilityTheory.Copula 2) (x : ℝ) (hx : C.chatterjeeXi ≤ x) (hx1 : x ≤ 1) :
      ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = x ∧ D.spearmanFootrule = C.spearmanFootrule

      Every attained point extends horizontally all the way to xi=1.

      source
      theorem Papers.Rockel2026XiFootrule.attainable_region_convex :
      Convex ℝ attainableRegion

      Theorem 3.3: the full attainable region is convex.

      source
      theorem Papers.Rockel2026XiFootrule.exact_nonnegative_footrule_region (x y : ℝ) (hy : 0 ≤ y) :
      (x, y) ∈ attainableRegion ↔ y ≤ 1 ∧ y ^ 2 ≤ x ∧ x ≤ 1

      Exact nonnegative-footrule part of the full region, with all endpoints.