Definition

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

The running diffusivity

The Section 3 running diffusivity is the unique positive scalar supplied by existsUnique_sigmaBar. There is no fallback value or provisional branch.

Main definition

• sigmaBar: the genuine running diffusivity of the coefficient cutoff.

noncomputable def Algsuperdiff.Section3.Annealed.sigmaBar {d : ℕ} (M : ABKModel d) (m : ℤ) : Observable.PositiveScalar

The genuine positive running diffusivity of the coefficient cutoff at scale m, selected from its proved unique infinite-volume characterization.

Equations

• Algsuperdiff.Section3.Annealed.sigmaBar M m = ⟨Classical.choose ⋯, ⋯⟩