Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.ThetaFamily

← Mathematical handbook

The original theta-indexed auxiliary and boundary family #

source
noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate (theta : ℝ) (ht : 0 < theta) :
ProbabilityTheory.Copula.RankRegion.RhoGamma.AuxiliaryCertificate

Lemma 3.5's actual primal-dual certificate, with precisely the source branch selection.

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

    Equation (16)'s choice of the contact distance.

    Equations
    Instances For
      source
      noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaDelta (theta : ℝ) :
      ℝ
      Equations
      Instances For
        source
        noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaMean (theta : ℝ) :
        ℝ
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaSquare (theta : ℝ) :
          ℝ
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaOffset (theta : ℝ) :
            ℝ
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate_s (theta : ℝ) (ht : 0 < theta) :
              (thetaCertificate theta ht).s = 1 / theta

              The auxiliary multiplier really is 1/theta, on all branches.

              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate_data (theta : ℝ) (ht : 0 < theta) :
              have A := thetaCertificate theta ht; ∫ (x : Fin 2 → ↑unitInterval), |↑(x 0) - ↑(x 1)| ∂A.D.toMeasure = thetaMean theta ∧ ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) - ↑(x 1)) ^ 2 ∂A.D.toMeasure = thetaSquare theta ∧ A.c = thetaOffset theta

              Equation (15) or (17), including the potential normalization, for every theta>0.

              source
              theorem Papers.AnsariRockelSteinmassl2026RhoGamma.sourceTheta_thetaCertificate (theta : ℝ) (ht : 0 < theta) :
              sourceTheta (thetaCertificate theta ht) = theta

              The paper's theta and the certificate normalization coincide exactly.