Characterization #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Characterization of the running diffusivity #
This file exposes the complete unique-choice characterization of sigmaBar:
positivity, convergence of the genuine unnormalized cutoff law's annealed
full-block matrices, and uniqueness among positive scalars with that limit.
Main result #
sigmaBar_characterization: the full limit and uniqueness theorem.
theorem
Algsuperdiff.Section3.Annealed.sigmaBar_characterization
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
:
0 < ↑(sigmaBar M m) ∧ Filter.Tendsto
(fun (n : ℕ) =>
HCPolySupport.toFullBlockMat
(HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) ↑n))
Filter.atTop
(nhds
(HCPolySupport.toFullBlockMat
(HCPolySupport.Book.Ch02.blockDiag (↑(sigmaBar M m) • 1) ((↑(sigmaBar M m))⁻¹ • 1)))) ∧ ∀ (other : ℝ),
0 < other →
Filter.Tendsto
(fun (n : ℕ) =>
HCPolySupport.toFullBlockMat
(HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) ↑n))
Filter.atTop
(nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (other • 1) (other⁻¹ • 1)))) →
other = ↑(sigmaBar M m)
The running diffusivity is positive, gives the genuine cutoff law's infinite-volume isotropic block limit, and is the unique positive scalar with that property.