Documentation

Papers.AnsariRockelSteinmassl2026RhoGamma.ThetaPotential

← Mathematical handbook

Lemma 3.5: the source potential, including its almost-everywhere derivative bound #

source
noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaWidth (theta : ℝ) :
ℝ

Equation (34).

Equations
Instances For
    source
    theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaCertificate_width (theta : ℝ) (ht : 0 < theta) :
    (thetaCertificate theta ht).w = thetaWidth theta

    The library certificate has exactly the Lipschitz constant specified by the source.

    source
    theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_auxiliary_potential (theta : ℝ) (ht : 0 < theta) :
    have A := thetaCertificate theta ht; A.h 0 = thetaOffset theta ∧ (∀ (u v : ↑unitInterval), A.h ↑u + A.h ↑v ≤ (↑u - ↑v) ^ 2 - 1 / theta * |↑u - ↑v|) ∧ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂A.D.toMeasure, A.h ↑(x 0) + A.h ↑(x 1) = (↑(x 0) - ↑(x 1)) ^ 2 - 1 / theta * |↑(x 0) - ↑(x 1)|

    Lemma 3.5: a genuine feasible potential, contact on the optimizer, and the source endpoint value.

    source
    theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_potential_derivative (theta : ℝ) (ht : 0 < theta) :
    ∀ᵐ (u : ℝ), DifferentiableAt ℝ (thetaCertificate theta ht).h u ∧ |deriv (thetaCertificate theta ht).h u| ≤ thetaWidth theta

    Equation (37), with differentiability itself established almost everywhere.

    source
    theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_discriminant_inequalities (theta : ℝ) (ht : 0 < theta) :
    theta ^ 2 * thetaWidth theta ^ 2 ≤ 1 + 2 * theta ^ 2 * thetaOffset theta ∧ (1 + theta * thetaWidth theta) / 2 ≤ thetaAlpha theta

    Lemma 3.7's discriminant and lower-root inequalities in the original theta variables.