WellDefinedness #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Well-definedness of the running diffusivity #
This file proves existence and uniqueness of the positive scalar describing the
infinite-volume annealed full-block limit of the genuine coefficient cutoff.
The proof consumes the verified law carrier, normalized structural law, and
direct normalized (P4) package. None of those proof ingredients appears as a
hypothesis of the public theorem.
Main result #
existsUnique_sigmaBar: the exact no-extra-premise well-definedness theorem for the Section 3 running diffusivity.
theorem
Algsuperdiff.Section3.Annealed.existsUnique_sigmaBar
{d : ℕ}
(M : ABKModel d)
(m : ℤ)
:
∃! sigma : ℝ, 0 < sigma ∧ Filter.Tendsto
(fun (n : ℕ) =>
HCPolySupport.toFullBlockMat
(HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) ↑n))
Filter.atTop (nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (sigma • 1) (sigma⁻¹ • 1))))
There is a unique positive scalar whose isotropic block diagonal is the infinite-volume annealed full-block limit of the genuine cutoff law.