EndpointSandwich

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

The endpoint sandwich for the running diffusivity

This module is deterministic arithmetic infrastructure. It transports the scalar squeeze sq_sandwich_of_relative_error to the running diffusivity Annealed.sigmaBar: a relative-error estimate against √(ν² + c⋆ γ⁻¹ 3^{2γm}) with deviation coefficient at most 1/4 yields the two-sided comparison with max (c⋆ γ⁻¹ 3^{2γm}) (ν²) in the constants 1/4 and 4.

The relative-error estimate is an explicit input binder: nothing here produces it, and no recurrence, probability space, or analytic producer is referenced. The only model facts used are the positivity of ν, γ, c⋆ and of Annealed.sigmaBar itself.

Main statement

• endpoint_sandwich_of_relative_error.

theorem Algsuperdiff.Section3.Provider.Diffusivity.endpoint_sandwich_of_relative_error {d : ℕ} {M : ABKModel d} {m : ℤ} {theta : ℝ} (htheta : 0 ≤ theta) (htheta' : theta ≤ 1 / 4) (hdev : |↑(Annealed.sigmaBar M m) - √(M.nu ^ 2 + Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ theta * ↑(Annealed.sigmaBar M m)) : 1 / 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2) ≤ ↑(Annealed.sigmaBar M m) ^ 2 ∧ ↑(Annealed.sigmaBar M m) ^ 2 ≤ 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m)) (M.nu ^ 2)

Endpoint sandwich from a relative-error flow estimate.

If the running diffusivity at scale m deviates from √(ν² + c⋆ γ⁻¹ 3^{2γm}) by at most θ · σ_m with 0 ≤ θ ≤ 1/4, then ¼ max (c⋆ γ⁻¹ 3^{2γm}) ν² ≤ σ_m² ≤ 4 max (c⋆ γ⁻¹ 3^{2γm}) ν².

The deviation hypothesis is an explicit input; no producer of it is asserted here.