Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.SignThresholds

← Mathematical handbook

The sharp zero slices and sign thresholds (Corollary 2.4) #

source
noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.rhoThreshold :
ℝ
Equations
Instances For
    source
    noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.gammaThreshold :
    ℝ
    Equations
    Instances For
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_zero :
      upperRho 0 = rhoThreshold
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.upperRho_neg_gammaThreshold :
      upperRho (-gammaThreshold) = 0
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.gammaThreshold_mem :
      gammaThreshold ∈ Set.Icc 0 1
      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.zero_gamma_slice (r : ℝ) :
      (r, 0) ∈ region ↔ |r| ≤ rhoThreshold

      Exactly the attainable rho values at gamma zero, including both endpoints.

      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.zero_rho_slice (g : ℝ) :
      (0, g) ∈ region ↔ |g| ≤ gammaThreshold

      Exactly the attainable gamma values at rho zero, including both endpoints.

      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.same_sign_of_abs_rho_gt (C : ProbabilityTheory.Copula 2) (h : rhoThreshold < |C.spearmanRho|) :
      0 < C.spearmanRho * C.giniGamma

      Above the sharp absolute rho threshold the coefficients have the same strict sign.

      source
      theorem Papers.AnsariRockelSteinmassl2026RhoGamma.same_sign_of_abs_gamma_gt (C : ProbabilityTheory.Copula 2) (h : gammaThreshold < |C.giniGamma|) :
      0 < C.spearmanRho * C.giniGamma

      Above the sharp absolute gamma threshold the coefficients have the same strict sign.