← Mathematical handbook

Both limiting endpoints and full coverage of the source theta parametrization

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaG_tendsto_atTop : Filter.Tendsto thetaG Filter.atTop (nhds 1)

The gamma coordinate tends to one along the full source family.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaG_tendsto_zero : Filter.Tendsto thetaG (nhdsWithin 0 (Set.Ioi 0)) (nhds (-1))

The gamma coordinate tends to minus one as theta decreases to zero.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_coordinates_tendsto_atTop : Filter.Tendsto (fun (theta : ℝ) => (thetaG theta, thetaP theta)) Filter.atTop (nhds (1, 1))

The full coordinate pair tends to the comonotone endpoint (1,1).

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_coordinates_tendsto_zero : Filter.Tendsto (fun (theta : ℝ) => (thetaG theta, thetaP theta)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-1, -1))

The full coordinate pair tends to the countermonotone endpoint (-1,-1).

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_gamma_coverage {g : ℝ} (hg : -1 < g) (hg1 : g < 1) : ∃ (theta : ℝ), 0 < theta ∧ thetaG theta = g

Every nonendpoint gamma value occurs at a positive finite source theta.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_coordinates_zero : (thetaG 0, thetaP 0) = (-1, -1)

The source endpoint convention at theta=0 is also the value of the explicit formulas.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.continuous_theta_coordinates_nonnegative : ContinuousOn (fun (theta : ℝ) => (thetaG theta, thetaP theta)) (Set.Ici 0)

Continuity on all finite nonnegative theta, including the endpoint zero.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_gamma_full_range (g : ℝ) : g ∈ Set.Icc (-1) 1 ↔ g = -1 ∨ g = 1 ∨ ∃ (theta : ℝ), 0 < theta ∧ thetaG theta = g

Theorem 1.1's surjectivity, including both endpoint conventions.