Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.ExactRegion

← Mathematical handbook

The full sharp rho-gamma region #

Boundary coordinates are explicit arithmetic expressions from the package. Both reflected boundaries are attained, as is every point between them.

source
@[reducible, inline]
abbrev Papers.AnsariRockelSteinmassl2026RhoGamma.BoundaryParameter :
Type
Equations
Instances For
    source
    noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho (g : ℝ) :
    ℝ
    Equations
    Instances For
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.boundary_coefficients (a : BoundaryParameter) :
      (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.copula a).giniGamma = ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.gamma a ∧ (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.copula a).spearmanRho = ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.rho a
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_parameter (a : BoundaryParameter) :
      upperRho (ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.gamma a) = ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.rho a
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sharp_upper_bound (C : ProbabilityTheory.Copula 2) :
      C.spearmanRho ≤ upperRho C.giniGamma
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sharp_lower_bound (C : ProbabilityTheory.Copula 2) :
      -upperRho (-C.giniGamma) ≤ C.spearmanRho
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upper_boundary_attained {g : ℝ} (hg : g ∈ Set.Icc (-1) 1) :
      ∃ (C : ProbabilityTheory.Copula 2), C.giniGamma = g ∧ C.spearmanRho = upperRho g
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.lower_boundary_attained {g : ℝ} (hg : g ∈ Set.Icc (-1) 1) :
      ∃ (C : ProbabilityTheory.Copula 2), C.giniGamma = g ∧ C.spearmanRho = -upperRho (-g)
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.exact_region (r g : ℝ) :
      (r, g) ∈ region ↔ g ∈ Set.Icc (-1) 1 ∧ -upperRho (-g) ≤ r ∧ r ≤ upperRho g

      Theorem 1.1, equation (6), with no supplied optimizer hypothesis.

      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.boundary_value_unique (a b : BoundaryParameter) (h : ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.gamma a = ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.gamma b) :
      ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.rho a = ProbabilityTheory.Copula.RankRegion.RhoGamma.UpperParameter.rho b
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.glued_dual_feasible (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) (u v : ↑unitInterval) :
      min ↑u ↑v * |max ↑u ↑v - A.t| ≤ A.dual ↑u + A.dual ↑v

      Explicit constructed certificates cover every auxiliary branch.

      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sharp_supporting_bound (A : ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate) (C : ProbabilityTheory.Copula 2) :
      C.spearmanRho - 3 / 2 * A.t * C.giniGamma ≤ A.copula.spearmanRho - 3 / 2 * A.t * A.copula.giniGamma

      Theorem 4.2: global support bound for each concrete glued optimizer.