GradSlotMoment

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

B6, first half: the Γ₂ display of the L-free gradient slot

What this module does

ShellSlotBounds.lFreeGradSlot m T R ω is

3^{2j} ( Σ_{i ∈ (j−2, m]} ‖∇ j_i‖_{W^{1,∞}(3^j v + □_j)}  +  T j v ω ) ,

This module produces the Step-4 target shape 𝒪_{Γ₂}(^{γj}) for that object, and isolates exactly one layer that the shape does not yet cover.

• The deep block Σ_{i ≥ j} -- every layer whose shell index is at least the cube scale -- carries the display

  3^{2j} Σ_{i ≥ j} ‖∇ j_i‖_{W^{1,∞}(3^j v + □_j)}
      = 𝒪_{Γ₂}( gammaTriangleConst 2 · (1 − 3^{γ−1})^{-1} · 3^{γ j} ) .
  

  The per-layer amplitude is 3^{j} 3^{(γ−1)i} (TailSummability's cross-scale reading of e.nabla.jk.O), the geometric sum over i ≥ j is 3^{γj}(1 − 3^{γ−1})^{-1}, and the Γ₂ triangle inequality for countable sums is the proved Orlicz.isBigOWith_gammaSigma_tsum_of_tsum_le. The constant is explicit and absolute: γ ≤ 1/4 gives (1 − 3^{γ−1})^{-1} ≤ (1 − 3^{-3/4})^{-1}.

• The bottom layer i = j − 1 is separated out (ae_lFreeGradSlot_eq_bottomLayer_add_deep). It is the ONE layer of the slot whose gauge is read on a cube strictly larger than the shell's own scale, and the proved per-shell display does not reach it.

References

• ABK26, (e.nabla.jk.O), (e.ugly.estimate.for.J.pre), (Step 3).

1. The layer gauge, and the deep block

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.gradLayerGauge {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (i : ℤ) : ℝ

One layer of the gradient slot: ‖∇ j_i‖_{W^{1,∞}(3^k v + □_k)}.

Equations

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

theorem Algsuperdiff.Section4.Provider.BoundsEaL.gradLayerGauge_nonneg {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (i : ℤ) : 0 ≤ gradLayerGauge k v omega i

theorem Algsuperdiff.Section4.Provider.BoundsEaL.measurable_gradLayerGauge {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (i : ℤ) : Measurable fun (omega : Section3.Cutoff.CutoffSample d) => gradLayerGauge k v omega i

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.deepGradTerm {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (i : ℤ) : ℝ

The layer term of the D block: the layers whose shell index is at least the cube scale, where the proved per-shell display applies.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.deepGradTerm k v omega i = if k ≤ i then Algsuperdiff.Section4.Provider.BoundsEaL.gradLayerGauge k v omega i else 0

theorem Algsuperdiff.Section4.Provider.BoundsEaL.deepGradTerm_nonneg {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (i : ℤ) : 0 ≤ deepGradTerm k v omega i

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.deepGradSeries {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The deep block of the gradient slot, before the cube weight.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.deepGradSeries k v omega = ∑' (i : ℤ), Algsuperdiff.Section4.Provider.BoundsEaL.deepGradTerm k v omega i

2. The per-layer Γ₂ display at the cube weight

theorem Algsuperdiff.Section4.Provider.BoundsEaL.isBigOWith_gammaSigma_weightedGradLayer {d : ℕ} (M : Section3.ABKModel d) {k i : ℤ} (hki : k ≤ i) (v : Fin d → ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Section3.Cutoff.CutoffSample d) => Real.rpow 3 (2 * ↑k) * gradLayerGauge k v omega i) (Real.rpow 3 (↑k + (M.gamma - 1) * ↑i))

The weighted layer display. For a shell index i at least the cube scale k, the weighted layer 3^{2k} ‖∇ j_i‖_{W^{1,∞}(3^k v + □_k)} has a Γ₂ upper tail at amplitude 3^{k + (γ−1)i}.

3. The geometric amplitude sum

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.deepGradConst {d : ℕ} (M : Section3.ABKModel d) : ℝ

The absolute constant of the deep block. Only γ ≤ 1/4 enters.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.deepGradConst M = HCPolySupport.IndependentSums.gammaTriangleConst 2 * (1 - Real.rpow 3 (M.gamma - 1))⁻¹

theorem Algsuperdiff.Section4.Provider.BoundsEaL.deepGradConst_pos {d : ℕ} (M : Section3.ABKModel d) : 0 < deepGradConst M

4. The deep block's Γ₂ display

theorem Algsuperdiff.Section4.Provider.BoundsEaL.tsum_deepGradTerm_eq {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) : ∑' (n : ℕ), gradLayerGauge k v omega (k + ↑n) = deepGradSeries k v omega

The ℕ-indexed reading of the deep block.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.isBigOWith_gammaSigma_deepGradSeries {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (v : Fin d → ℤ) : HCPolySupport.IndependentSums.IsBigOWith (↑(Section3.Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : Section3.Cutoff.CutoffSample d) => Real.rpow 3 (2 * ↑k) * deepGradSeries k v omega) (deepGradConst M * Real.rpow 3 (M.gamma * ↑k))

B6, first half: the deep block of the gradient slot has the Step-4 target shape.

3^{2j} Σ_{i ≥ j} ‖∇ j_i‖_{W^{1,∞}(3^j v + □_j)} = 𝒪_{Γ₂}(^{γ j}) with the explicit absolute constant C = gammaTriangleConst 2 · (1 − 3^{γ−1})^{-1}. No exponent is moved: the per-layer amplitude is the manuscript's own 3^{(γ−1)i}, the cube weight contributes 3^{k}, and the geometric sum over i ≥ k contributes 3^{γk}(1 − 3^{γ−1})^{-1}.

5. The slot decomposition: the deep block plus ONE bottom layer

theorem Algsuperdiff.Section4.Provider.BoundsEaL.deepGradTerm_eq_add {d : ℕ} (m k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (hkm : k ≤ m) (i : ℤ) : deepGradTerm k v omega i = tailLayerTerm m k v omega i + if k ≤ i ∧ i ≤ m then gradLayerGauge k v omega i else 0

The layer bookkeeping: below the truncation the deep term splits into the (m, ∞) tail term and a finitely supported middle block.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.headLayerSum_add_tailSeriesGauge_eq {d : ℕ} (m k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (hkm : k ≤ m) (hsum : Summable (tailLayerTerm m k v omega)) : headLayerSum m k v omega + tailSeriesGauge m k v omega = gradLayerGauge k v omega (k - 1) + deepGradSeries k v omega

The slot bracket, resolved. Wherever the upper shell series converges, the L-free bracket of the gradient slot is the bottom layer i = k − 1 plus the deep block.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.ae_lFreeGradSlot_eq_bottomLayer_add_deep {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (hkm : R.scale ≤ m) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), lFreeGradSlot m (tailSeriesGauge m) R omega = Real.rpow 3 (2 * ↑R.scale) * gradLayerGauge R.scale R.index omega (R.scale - 1) + Real.rpow 3 (2 * ↑R.scale) * deepGradSeries R.scale R.index omega

B6, first half: the gradient slot resolved almost surely.

At the canonical tail gauge the L-free gradient slot is, almost surely, the weighted bottom layer i = R.scale − 1 plus the weighted deep block.