← Mathematical handbook

Continuous auxiliary data across all theta breakpoints

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceTriple (N : ℕ) (ell delta : ℝ) : Fin 3 → ℝ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.contactTriple (n : ℝ) : Fin 3 → ℝ

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.contactTriple n = ![1 / (2 * n), 1 / (4 * n ^ 2), -(1 / (8 * n ^ 2))]

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.inputArc (N : ℕ) (s : ℝ) : Fin 3 → ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.continuous_inputArc (N : ℕ) (hN : 0 < N) : Continuous (inputArc N)

The left and right source formulas agree at every internal arc junction.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.inputArc_at_left (N : ℕ) (hN : 0 < N) : inputArc N (1 / ↑N) = contactTriple ↑N

The integer endpoint at the start of a theta interval.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.inputArc_at_right (N : ℕ) (hN : 0 < N) : inputArc N (1 / (↑N + 1)) = contactTriple (↑N + 1)

The integer endpoint at the end of a theta interval.

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.thetaInput (theta : ℝ) : Fin 3 → ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaInput_integer (N : ℕ) (hN : 0 < N) : thetaInput ↑N = contactTriple ↑N

The source's auxiliary data at every positive integer theta.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.thetaInput_on_interval (N : ℕ) (hN : 0 < N) {theta : ℝ} (ht : theta ∈ Set.Icc (↑N) (↑N + 1)) : thetaInput theta = inputArc N (1 / theta)

On a closed theta interval, the floor-based source formulas equal one continuous arc.