StepFiveBudgetSums

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

t.regularity Step 5: the two budget sums

The target

ABK26 t.regularity Step 5, the displays

  e.sum.eps.j.bound
      ∑_{j=n}^{m-1} ε_j  ≤  C δ (m-n)  =  C C₁^{-1}(1-α)(m-n)
  e.sum.delta.j.bound
      ∑_{j=n}^{m-1} δ_j  ≤  C 3^{m/2} σ_m^{-1} [g]_{W^{1/2,∞}(□_m)}
        + C ( 3^{m/2} [∇h]_{W^{1/2,∞}(□_m)}
              + C₁^{-1}(1-α)(m-n) ‖∇h‖_{L^∞(□_m)} ) 1_{z ∉ □_{m-1}} .

The first display is unconditional here: it is the Cesàro clause of GoodScaleWindows — the very same clause that supplies the bad-scale budget — read on the ε leg instead of the indicator leg. The manuscript attributes it to "e.scale.sep.for.mathcal.E and the definition of X_m(α)"; in the proved formalization the X_m(α) gate is what delivers GoodScaleWindows, so the implication is exactly the one transcribed here.

The second display is proved in abstract-real form: its three legs are the two geometric tails of StepFiveGeometricTail plus one ε-sum leg, which is the first display again.

Deviations from print

• D1 (window). The anchor l.iteration.lemma sums ε and δ over Finset.Icc n m; the manuscript's displays sum over [n, m-1]. The ε bound below is proved on the larger window Icc n m (which is what GoodScaleWindows gives and what the anchor consumes), hence dominates the printed sum.
• D2 (constant). GoodScaleWindows yields δ((m-n)+1), not δ(m-n). With the Step-3 window gate 14 ≤ m-n this is ≤ 2δ(m-n), i.e. the printed C δ (m-n) at the explicit C = 2. Recorded, not hidden.
• ** (binding).** The boundary leg ε_j ‖∇h‖_{L^∞} 1_{z∉□_{m-1}} is carried explicitly through the three-leg budget; it is NOT discarded.

References

• ABK26, t.regularity Step 5.

1. The real-valued ε_j(z) family

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepFiveEps {d : ℕ} (M : Section3.ABKModel d) (j : ℤ) (z : HCPolySupport.Vec d) (delta : ℝ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

ε_j(z) as a real number.'s stepOneEpsJ is ℝ≥0∞-valued, while l.iteration.lemma demands ε : ℤ → ℝ; this is the toReal layer.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepFiveEps M j z delta omega = (Algsuperdiff.Section4.Provider.Regularity.stepOneEpsJ M j z delta omega).toReal

theorem Algsuperdiff.Section4.Provider.Regularity.stepFiveEps_nonneg {d : ℕ} (M : Section3.ABKModel d) (j : ℤ) (z : HCPolySupport.Vec d) (delta : ℝ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ stepFiveEps M j z delta omega

ε_j(z) ≥ 0 — the sign hypothesis of l.iteration.lemma.

2. e.sum.eps.j.bound

theorem Algsuperdiff.Section4.Provider.Regularity.sum_stepOneEpsJ_le_of_goodScaleWindows_fine {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {w : Fin d → ℤ} (hw : w ∈ Support.latticeCubeSet d (n - 1) m) : ∑ k ∈ Finset.Icc n m, stepOneEpsJ M k (Support.triadicLatticePoint (n - 1) w) delta omega ≤ ENNReal.ofReal delta * (↑(m - n).toNat + 1)

The ε-Cesàro clause read as a sum, at the producer's own (finer) lattice: ∑_{k=n}^{m} ε_k(z) ≤ δ ((m-n)+1) in ℝ≥0∞.

theorem Algsuperdiff.Section4.Provider.Regularity.sum_stepFiveEps_le_of_goodScaleWindows_fine {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta : 0 ≤ delta) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {w : Fin d → ℤ} (hw : w ∈ Support.latticeCubeSet d (n - 1) m) : ∑ k ∈ Finset.Icc n m, stepFiveEps M k (Support.triadicLatticePoint (n - 1) w) delta omega ≤ delta * (↑(m - n).toNat + 1)

The same at the printed lattice 3^n ℤ^d ∩ □_m, and in ℝ.

theorem Algsuperdiff.Section4.Provider.Regularity.sum_stepFiveEps_le_of_goodScaleWindows {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta : 0 ≤ delta) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : ∑ k ∈ Finset.Icc n m, stepFiveEps M k (Support.triadicLatticePoint n v) delta omega ≤ delta * (↑(m - n).toNat + 1)

e.sum.eps.j.bound, at the printed centres z ∈ 3^n ℤ^d ∩ □_m:

   ∑_{k=n}^{m} ε_k(z)  ≤  δ ((m-n) + 1) .

Note the window is the anchor's Icc n m (deviation D1) and the length is (m-n)+1 (deviation D2).

theorem Algsuperdiff.Section4.Provider.Regularity.toNat_window_add_one_le_two_mul {n m : ℤ} (hwin : 14 ≤ m - n) : ↑(m - n).toNat + 1 ≤ 2 * (↑m - ↑n)

(m-n).toNat + 1 ≤ 2 (m-n) at the Step-3 window gate 14 ≤ m-n — the arithmetic that turns deviation D2's δ((m-n)+1) into the printed C δ (m-n) at C = 2.

theorem Algsuperdiff.Section4.Provider.Regularity.sum_stepFiveEps_le_two_mul_delta_mul_window {d : ℕ} {M : Section3.ABKModel d} {delta : ℝ} {n m : ℤ} {omega : Section3.Cutoff.CutoffSample d} (hdelta : 0 ≤ delta) (hwin : 14 ≤ m - n) (hgood : GoodScaleWindows M stepOneSEighth delta stepOneSEighth_pos n m omega) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d n m) : ∑ k ∈ Finset.Icc n m, stepFiveEps M k (Support.triadicLatticePoint n v) delta omega ≤ 2 * delta * (↑m - ↑n)

e.sum.eps.j.bound in the printed shape:

   ∑_{k=n}^{m} ε_k(z)  ≤  2 δ (m-n) .

The explicit C = 2 is deviation D2; the window is the anchor's (D1), which dominates the printed [n, m-1].