MinimalScaleSeparation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Minimal scale separation — [ABK] p.minimal.scale.separation.sec4 #
There is an almost surely finite random minimal scale Z, with an exponential
tail in the number of scales, above which the scale averages of two quantities
are simultaneously at most delta, uniformly over the triadic lattice points
of the ambient cube: the flux-corrected error observable restricted to the
good event, and the indicator of the complement of that good event.
Proved; reduces to the standard axioms.
theorem
Algsuperdiff.Frozen.Section4.minimal_scale_separation
(d : ℕ)
:
∃ (C : ℝ),
0 < C ∧ ∀ (M : Section3.ABKModel d) (s delta : ℝ),
s ∈ Set.Ioc 0 (1 / 4) →
delta ∈ Set.Ioc 0 (1 / 2) →
M.gamma ≤ C⁻¹ ^ 10 * min (Section3.Disorder.cstar M ^ 10) (delta ^ 2 * Section3.Disorder.cstar M ^ 2 * s ^ 9) →
8 * M.gamma ≤ s →
∀ (m : ℤ) (hs : 0 < s),
∃ (Z : Section3.Cutoff.CutoffSample d → ℕ∞),
Measurable Z ∧ (∀ (N : ℕ),
↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ Z omega} ≤ ENNReal.ofReal
(C * Real.exp
(-((↑N - 1) * s ^ 9 * Section3.Disorder.cstar M ^ 2 * delta ^ 2) / (C * M.gamma)))) ∧ ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ n ≤ m,
Z omega ≤ ↑(m - n).toNat →
⨆ (z : ↑(Section4.Support.latticeCubeSet d (n - 1) m)),
(↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m,
(goodEventAt M (Section4.Support.cgEllipLowerConstant d) k
(Section4.Support.triadicLatticePoint (n - 1) ↑z) ⟨s, hs⟩
(s * √delta)).indicator
(fun (omega' : Section3.Cutoff.CutoffSample d) =>
Section4.Support.fluxCorrectedErrorObservableSup M k ⟨s, hs⟩
(Section3.Cutoff.translateCutoffSample
(Section4.Support.triadicLatticePoint (n - 1) ↑z) omega'))
omega ≤ ENNReal.ofReal delta ∧ ⨆ (z : ↑(Section4.Support.latticeCubeSet d (n - 1) m)),
(↑(m - n).toNat + 1)⁻¹ * ∑ k ∈ Finset.Icc n m,
(goodEventAt M (Section4.Support.cgEllipLowerConstant d) k
(Section4.Support.triadicLatticePoint (n - 1) ↑z) ⟨s, hs⟩
(s * √delta))ᶜ.indicator
(fun (x : Section3.Cutoff.CutoffSample d) => 1) omega ≤ ENNReal.ofReal delta