← Mathematical handbook

The source auxiliary distance law: an atom and a uniform interval component

noncomputable def Papers.AnsariRockelSteinmassl2026RhoGamma.sourceAtomMass (N : ℕ) (delta : ℝ) : ℝ

Equations

• Papers.AnsariRockelSteinmassl2026RhoGamma.sourceAtomMass N delta = 1 - 2 * ↑N * (↑N + 1) * |delta|

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_distance_distribution (theta : ℝ) (ht : 1 < theta) (f : ℝ → ℝ) (hf : Continuous f) : have A := thetaCertificate theta ⋯; have p := sourceAtomMass ⌊theta⌋₊ (thetaDelta theta); ∫ (x : Fin 2 → ↑unitInterval), f |↑(x 0) - ↑(x 1)| ∂A.D.toMeasure = p * f (thetaEll theta) + (1 - p) * ∫ (u : ↑unitInterval), f (thetaEll theta + thetaDelta theta * ↑u)

Section 2.1's complete distance-distribution formula, tested against every continuous function.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_atom_mass_bounds (theta : ℝ) (ht : 1 < theta) : sourceAtomMass ⌊theta⌋₊ (thetaDelta theta) ∈ Set.Icc 0 1

The atom and interval-component weights are genuine probabilities.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_delta_bound (theta : ℝ) (ht : 1 < theta) : |thetaDelta theta| ≤ 1 / (2 * ↑⌊theta⌋₊) - 1 / (2 * (↑⌊theta⌋₊ + 1))

The source bound |delta|<=L-R holds uniformly on every finite branch.

theorem Papers.AnsariRockelSteinmassl2026RhoGamma.theta_midpoint_atom_zero (theta : ℝ) (ht : 1 < theta) (hmid : 1 / theta = 1 / (2 * ↑⌊theta⌋₊) + 1 / (2 * (↑⌊theta⌋₊ + 1))) : sourceAtomMass ⌊theta⌋₊ (thetaDelta theta) = 0

At each internal source junction, the atomic part vanishes.