AnnularFinal #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
Algsuperdiff.Section4.Provider.Annular.annular_decomposition_provider
(d : ℕ)
:
∃ (C : ℝ),
0 < C ∧ ∀ (M : Section3.ABKModel d),
M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 →
∀ s ∈ Set.Icc (8 * M.gamma) (1 / 4),
∀ (hs : 0 < s) (m : ℤ),
∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), (Support.eventG0 M (Support.cgEllipLowerConstant d) m ∩ Support.eventG1 M m s (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹)).indicator
(fun (omega' : Section3.Cutoff.CutoffSample d) =>
Support.fluxCorrectedErrorObservableSqSup M m ⟨s, hs⟩ omega')
omega ≤ (ENNReal.ofReal (C * s) * ∑' (j : { j : ℤ // j ≤ m }) (n : { n : ℤ // n ≤ ↑j - 1 }), ENNReal.ofReal (Real.rpow 3 (-s * ↑(m - ↑n))) * ⨆ (v : ↑(Support.latticeAnnulusSet d (↑n) (↑j) (↑j - 1))),
ENNReal.ofReal
(Support.annularErrorObservable M ↑n ⟨s, hs⟩
(Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint ↑n ↑v)
omega) ^ 2)) + ENNReal.ofReal
(C * s⁻¹ ^ 3 * (Section3.Disorder.cstar M)⁻¹ ^ 4 * M.gamma ^ 2 * |Real.log M.gamma| ^ 4) + ENNReal.ofReal (C * s⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * (∑' (k : { k : ℤ // m ≤ k }), ENNReal.ofReal
(Real.rpow 3 ((2 - M.gamma) * ↑m) * Support.shellW1InfGradNorm m (↑omega ↑k))) ^ 2 + ENNReal.ofReal (C * s⁻¹ ^ 2 * (Section3.Disorder.cstar M)⁻¹ * M.gamma) * ∑' (n : { n : ℤ // n ≤ m }), ENNReal.ofReal (Real.rpow 3 (-(1 / 2) * s * ↑(m - ↑n))) * ∑ k ∈ Finset.Icc (↑n - 1) m,
(ENNReal.ofReal (Real.rpow 3 ((2 - M.gamma) * ↑k)) * ⨆ (v : ↑(Support.latticeCubeSet d k m)),
ENNReal.ofReal
(Support.shellW2InfNormAt (Support.triadicLatticePoint k ↑v) k (↑omega k))) ^ 2 ∧ ∀ ep ∈ Set.Ioc 0 (1 / 2),
M.gamma * |Real.log M.gamma| ^ 2 ≤ s.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * ep →
(Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) m 0 ⟨s, hs⟩ ep).indicator
(fun (omega' : Section3.Cutoff.CutoffSample d) =>
Support.fluxCorrectedErrorObservableSup M m ⟨s, hs⟩ omega')
omega ≤ ENNReal.ofReal (C * ep)
The frozen annular-decomposition statement, proved.