Documentation

Papers.AnsariRockel2026RhoFootrule.ExactRegion

← Mathematical handbook

The full sharp rho-footrule region #

The package supplies arithmetic boundary parameters, actual attaining copulas, and global inequalities. The coefficient order here matches the article. Uniqueness of the optimizing copula is proved in OptimizerUniqueness.lean.

source
@[reducible, inline]
abbrev Papers.AnsariRockel2026RhoFootrule.BoundaryParameter :
Type
Equations
Instances For
    source
    noncomputable def Papers.AnsariRockel2026RhoFootrule.upperRho (p : ℝ) :
    ℝ

    The upper boundary as a scalar function on its valid interval.

    Equations
    Instances For
      source
      theorem Papers.AnsariRockel2026RhoFootrule.upperRho_parameter (a : BoundaryParameter) :
      upperRho (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule a) = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.rho a

      The scalar boundary agrees with every explicit arithmetic arc.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.boundary_coefficients (a : BoundaryParameter) :
      (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.copula a).spearmanFootrule = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule a ∧ (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.copula a).spearmanRho = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.rho a

      Both coefficient identities of the constructed boundary copula.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.sharp_upper_bound (C : ProbabilityTheory.Copula 2) :
      C.spearmanRho ≤ upperRho C.spearmanFootrule

      Global sharp upper bound, valid for singular copulas too.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.upper_boundary_attained {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) :
      ∃ (C : ProbabilityTheory.Copula 2), C.spearmanFootrule = p ∧ C.spearmanRho = upperRho p

      Every upper-boundary point is attained.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.sharp_lower_bound (C : ProbabilityTheory.Copula 2) :
      -1 + 2 * √((1 + 2 * C.spearmanFootrule) / 3) ^ 3 ≤ C.spearmanRho

      The known lower boundary, with its exact square-root normalization.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.lower_boundary_attained {p : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) :
      ∃ (C : ProbabilityTheory.Copula 2), C.spearmanFootrule = p ∧ C.spearmanRho = -1 + 2 * √((1 + 2 * p) / 3) ^ 3
      source
      theorem Papers.AnsariRockel2026RhoFootrule.exact_region (r p : ℝ) :
      (∃ (C : ProbabilityTheory.Copula 2), C.spearmanRho = r ∧ C.spearmanFootrule = p) ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ ProbabilityTheory.Copula.RankRegion.RhoFootrule.lowerBoundary p ≤ r ∧ r ≤ upperRho p

      Corollary 1.2: both directions, in the source's (rho, footrule) order.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.boundary_value_unique (a b : BoundaryParameter) (h : ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule a = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.footrule b) :
      ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.rho a = ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.rho b

      Arc junctions yield the same boundary value.