Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.ThetaBoundary

← Mathematical handbook

Theorem 1.1 and Proposition 3.9 in the paper's original theta coordinates #

source
noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaAlpha (theta : ℝ) :
ℝ
Equations
Instances For
    source
    noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaT (theta : ℝ) :
    ℝ
    Equations
    Instances For
      source
      noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaA (theta : ℝ) :
      ℝ
      Equations
      Instances For
        source
        noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaZ (theta : ℝ) :
        ℝ
        Equations
        Instances For
          source
          noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaG (theta : ℝ) :
          ℝ

          Equation (19), the source gamma coordinate.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaP (theta : ℝ) :
            ℝ

            Equation (19), the source rho coordinate.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_splitting (theta : ℝ) (ht : 0 < theta) :
              have A := thetaCertificate theta ht; sourceAlpha A = thetaAlpha theta ∧ A.t = thetaT theta ∧ ↑A.a = thetaA theta ∧ A.z = thetaZ theta

              The source formulas (18) agree with the actual copula's gluing lengths.

              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_boundary_coefficients (theta : ℝ) (ht : 0 < theta) :
              (thetaCertificate theta ht).copula.giniGamma = thetaG theta ∧ (thetaCertificate theta ht).copula.spearmanRho = thetaP theta

              Proposition 3.9: the actual constructed copula has exactly G(theta), P(theta).

              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_boundary_maximizes (theta : ℝ) (ht : 0 < theta) (C : ProbabilityTheory.Copula 2) (hC : C.giniGamma = thetaG theta) :
              C.spearmanRho ≤ thetaP theta

              Theorem 1.1's maximizing statement, for every original theta>0.

              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_boundary_value (theta : ℝ) (ht : 0 < theta) :
              upperRho (thetaG theta) = thetaP theta

              Equation (5), including attainment, in the paper's explicit theta parametrization.

              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_parameter_inequalities (theta : ℝ) (ht : 0 < theta) :
              thetaOffset theta < 0 ∧ thetaAlpha theta < 1 ∧ thetaT theta / 2 ≤ thetaA theta ∧ thetaA theta < thetaT theta

              Lemma 3.7 stated entirely with the source's explicit functions.