HomogenizationStep #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The homogenization step — [ABK] p.homogenization.step #
Two-term Orlicz control of the cutoff homogenization error at every scale
below m upgrades, on one common event, to two-term Orlicz control of the
whole family of cutoff response observables indexed by scale and direction:
the fluctuation term improves to epsilon E^2 gamma and the rare term to
epsilon exp(-2 E^{-3} gamma^{-1}).
Proved; reduces to the standard axioms.
theorem
Algsuperdiff.Frozen.Section3.homogenization_step
(d : ℕ)
:
∃ (Chom : ℝ),
1 ≤ Chom ∧ ∀ (M : Section3.ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }),
15 * (Section3.Disorder.cstar M)⁻¹ ≤ ↑E →
M.gamma ≤ (↑E)⁻¹ ^ 10 →
(∀ k ≤ m - 1,
∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1),
Section3.Probability.IsTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2))
(Section3.Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma)
(s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) →
∀ epsilon ∈ Set.Ioc 0 (1 / 2),
M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon →
Section3.Probability.IsCommonEventTwoTermBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (1 / 4))
(fun
(i :
{ p : ℤ × { e : HCPolySupport.Vec d // HCPolySupport.Book.Ch02.vecNorm e = 1 } // ↑p.1 ≤ ↑m - Chom * |Real.log epsilon| }) =>
Section3.Observable.cutoffResponseJ M m (↑i).1 ↑(↑i).2)
(epsilon * ↑E ^ 2 * M.gamma) (epsilon * Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)))