StepSevenFlushMerged

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

countable index data

Nothing here imports any of them, nothing here claims an anchor, and nothing here is a frozen statement.

The quantifier move

The boundary assembly chooses its scales A the sample (the pigeonhole selection depends on the bad set), at a lattice centre depending on the root's own x, and its flush direction after the geometry — so one null set must serve every index at once. As's merge, the index data are countable (ℤ-scales, printed lattice centres, Fin d directions, a sign bit), and Mathlib's ae_all_iff does the whole job.

References

• Mathlib, MeasureTheory.ae_all_iff.

1. The good-event bridge

theorem Algsuperdiff.Section4.Provider.Regularity.mem_goodEventAtHalf_of_stepThree {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {j : ℤ} {z : HCPolySupport.Vec d} {omega : Section3.Cutoff.CutoffSample d} (hdelta : delta ∈ Set.Ioc 0 (1 / 2)) (hmem : omega ∈ stepThreeGoodEvent M delta j z) : omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) j z ⟨stepOneS / 8, mem_goodEventAtHalf_of_stepThree._proof_1⟩ (1 / 2)

2. The flush conclusion record

def Algsuperdiff.Section4.Provider.Regularity.StepSevenFlushBound {d : ℕ} (M : Section3.ABKModel d) (K1 K2 : ℝ) (L m n : ℤ) (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : Prop

The uniform solution estimate assembled in the seventh regularity step.

Equations

• One or more equations did not get rendered due to their size.

3. The flush window energy, merged

theorem Algsuperdiff.Section4.Provider.Regularity.ae_stepSevenFlushBound_merged (d : ℕ) [NeZero d] : ∃ (C : ℝ) (A : ℝ) (K1 : ℝ) (K2 : ℝ), 0 < C ∧ 0 < A ∧ 0 < K1 ∧ 0 ≤ K2 ∧ ∀ (M : Section3.ABKModel d), stepOneS ∈ Set.Icc (64 * M.gamma) 1 → M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (stepOneS / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L m n nl : ℤ) (v : Fin d → ℤ) (i : Fin d) (sigma : ℝ), sigma = 1 ∨ sigma = -1 → m ≤ L → n + 3 ≤ m → Support.triadicLatticePoint nl v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → ExcessDecay.wellPlacedHalfGap m (n + 2) < sigma * Support.triadicLatticePoint nl v i → omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) (Support.triadicLatticePoint nl v) ⟨stepOneS / 8, mem_goodEventAtHalf_of_stepThree._proof_1⟩ (1 / 2) → A * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨stepOneS / 8, mem_goodEventAtHalf_of_stepThree._proof_1⟩ (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint nl v) omega) ≤ stepOneS ^ 4 → StepSevenFlushBound M K1 K2 L m n (Support.triadicLatticePoint nl v) omega

4. The ε-pin, merged

theorem Algsuperdiff.Section4.Provider.Regularity.ae_shellEpsPin_merged (d : ℕ) : ∃ (Cann : ℝ), 0 < Cann ∧ ∀ (A : ℝ), 0 < A → ∃ (Cfl : ℝ), 1 ≤ Cfl ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ Cann⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 256 → ∀ (Cedos Citer : ℝ) (k : ℕ), Cfl ≤ Cedos → ∀ (alpha : ℝ), 0 < alpha → alpha < 1 → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp (stepOneDelta (stepOneC1 d Cedos 1 Citer k) alpha) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (j nl : ℤ) (v : Fin d → ℤ), omega ∈ stepThreeGoodEvent M (stepOneDelta (stepOneC1 d Cedos 1 Citer k) alpha) j (Support.triadicLatticePoint nl v) → ∀ (L : ℤ), j ≤ L → A * Support.fluxCorrectedErrorRepresentative M L j ⟨stepOneS / 8, mem_goodEventAtHalf_of_stepThree._proof_1⟩ (Section3.Cutoff.translateCutoffSample (Support.triadicLatticePoint nl v) omega) ≤ stepOneS ^ 4