SigmaBarBridge

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Comparing the generator and canonical running diffusivities

The generator-renormalization theorem introduces a positive scalar through an existential quantifier, while the localized quantities use Annealed.sigmaBar. Both scalars satisfy the same relative approximation to the explicit square-root scale. The triangle inequality therefore compares the existential scalar directly with the canonical one.

theorem Algsuperdiff.Section5.Support.generatorSigmaBar_close_to_sigmaBar_of_approx (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (Cind : ℝ), 0 < gamma0 ∧ 0 < Cind ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (m : ℤ) (Cgen sigmaBarM : ℝ), 0 < Cgen → 0 < sigmaBarM → |sigmaBarM - √(M.nu ^ 2 + cstar * M.gamma⁻¹ * Real.rpow 3 (2 * M.gamma * ↑m))| ≤ Cgen * √M.gamma * |Real.log M.gamma| * sigmaBarM → |sigmaBarM - ↑(Section3.Annealed.sigmaBar M m)| ≤ max Cgen (Cind * cstar⁻¹ ^ 2) * √M.gamma * |Real.log M.gamma| * (sigmaBarM + ↑(Section3.Annealed.sigmaBar M m))

Any positive scalar satisfying the generator approximation is close to the canonical running diffusivity. This form keeps the comparison attached to the same scalar used by a caller's other conclusions.