Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.SharpDiscrepancy

← Mathematical handbook

The largest rho-gamma discrepancy (Proposition 2.3) #

An explicit half-shift certificate has supporting multiplier one. Its exact value bounds every copula, and reflection gives the absolute bound.

source
noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancyS :
ℝ
Equations
Instances For
    source
    theorem Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancyS_ge_one :
    1 ≤ discrepancyS
    source
    noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancyCertificate :
    ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancyCopula :
      ProbabilityTheory.Copula 2
      Equations
      Instances For
        source
        noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.maximalDiscrepancy :
        ℝ
        Equations
        Instances For
          source
          theorem Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancy_support_slope :
          discrepancyCertificate.t = 2 / 3
          source
          theorem Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancy_coefficients :
          discrepancyCopula.giniGamma = -1 + 8 * ((14 - 2 * √10) / 39) - 10 * ((14 - 2 * √10) / 39) ^ 2 ∧ discrepancyCopula.spearmanRho = -1 + 12 * ((14 - 2 * √10) / 39) - 24 * ((14 - 2 * √10) / 39) ^ 2 + 13 * ((14 - 2 * √10) / 39) ^ 3

          The maximizing point is the source's d0=(14-2 sqrt(10))/39.

          source
          theorem Papers.AnsariRockelSteinmassl2026RhoGamma.discrepancy_value :
          discrepancyCopula.spearmanRho - discrepancyCopula.giniGamma = maximalDiscrepancy
          source
          theorem Papers.AnsariRockelSteinmassl2026RhoGamma.rho_sub_gamma_le (C : ProbabilityTheory.Copula 2) :
          C.spearmanRho - C.giniGamma ≤ maximalDiscrepancy
          source
          theorem Papers.AnsariRockelSteinmassl2026RhoGamma.abs_rho_sub_gamma_le (C : ProbabilityTheory.Copula 2) :
          |C.spearmanRho - C.giniGamma| ≤ maximalDiscrepancy

          The sharp absolute discrepancy for every bivariate copula.

          source
          theorem Papers.AnsariRockelSteinmassl2026RhoGamma.maximal_discrepancy_attained :
          ∃ (C : ProbabilityTheory.Copula 2), |C.spearmanRho - C.giniGamma| = maximalDiscrepancy ∧ ∀ (D : ProbabilityTheory.Copula 2), |D.spearmanRho - D.giniGamma| ≤ maximalDiscrepancy

          Proposition 2.3 as an attained maximum, rather than just a bound.