GradBottomLayer

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

B6, first half completed: the bottom layer of the L-free gradient slot

What this module does

GradSlotMoment.lean resolved the L-free gradient slot into a deep block (every shell index at least the cube scale, carrying the 𝒪_{Γ₂}(^{γj}) display) plus ONE bottom layer i = j − 1, read on a cube strictly larger than its own shell scale. It is settled here.

The route is the proved covering-plus-maximum machinery of Stream/LargeCubeW1Inf.lean and its translated companion Stream/TranslatedLargeCubeW1Inf.lean: their largeCubeDerivGauge l k j = 3^k ‖∇j‖_{L^∞(□_l)} + 3^{2k} ‖∇²j‖_{L^∞(□_l)} is exactly the manuscript's e.W1inf.jL.bound.smaller summand, and isBigOWith_gammaSigma_largeCubeDerivGauge_lt_translate prices it, for k < l real base point, at C(d) (l − k)^{1/2} 3^{γk}. Taking the cube scale l = j and the shell scale k = j − 1 gives l − k = 1, so the maximum lemma's (log N)^{1/2} factor is a pure d-constant here.

The deterministic bridge is the exact weight arithmetic

3^{2j} ‖∇ j_{j−1}‖_{W^{1,∞}(z+□_j)}
    ≤ 3^{2j} ‖∇² j_{j−1}‖_{L^∞(z+□_j)} + 3^{j} ‖∇ j_{j−1}‖_{L^∞(z+□_j)}
    ≤ 9 · largeCubeDerivGauge j (j−1) (translate z j_{j−1}) ,

since 9 · 3^{j−1} = 3^{j+1} ≥ 3^{j} and 9 · 3^{2(j−1)} = 3^{2j}. Only constants move; the amplitude 3^{γ(j−1)} ≤ 3^{γj} keeps the exponent.

The assembled slot

Section 3 below glues the bottom layer to GradSlotMoment's deep block through the single ℕ-indexed series

fullGradSeries j v ω = Σ_{n ≥ 0} ‖∇ j_{j−1+n}‖_{W^{1,∞}(3^j v + □_j)} ,

whose weighted form carries one 𝒪_{Γ₂}(^{γj}) display for the WHOLE L-free gradient slot (isBigOWith_gammaSigma_weightedFullGradSeries); the identification with the slot itself is almost sure, exactly as in GradSlotMoment.ae_lFreeGradSlot_eq_bottomLayer_add_deep.

References

• ABK26, (e.nabla.jk.O), (e.W.1.inf.bound), (e.W1inf.jL.bound.smaller), (bullet (B6), first half).

1. The deterministic bridge to the proved large-cube derivative gauge

theorem Algsuperdiff.Section4.Provider.BoundsEaL.rpow_weighted_shellW1InfGradNorm_le_largeCubeDerivGauge {d : ℕ} (k : ℤ) (f : Frozen.Assumptions.ShellField d) : Real.rpow 3 (2 * ↑k) * Support.shellW1InfGradNorm k f ≤ 9 * Section3.Provider.Stream.largeCubeDerivGauge k (k - 1) f

The bottom-layer weight arithmetic. The cube-weighted W^{1,∞} gradient gauge at cube scale k is dominated by 9 times the proved large-cube derivative gauge at cube scale k and shell scale k − 1.

2. The Γ₂ display of the bottom layer

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.bottomGradConst (d : ℕ) : ℝ

The explicit constant of the bottom-layer display: 9 times the proved e.W1inf.jL.bound.smaller constant.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.bottomGradConst d = 9 * Algsuperdiff.Section3.Provider.Stream.shellW1InfSmallerConst d

theorem Algsuperdiff.Section4.Provider.BoundsEaL.bottomGradConst_nonneg (d : ℕ) : 0 ≤ bottomGradConst d

theorem Algsuperdiff.Section4.Provider.BoundsEaL.isBigOWith_gammaSigma_weightedBottomGradLayer {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) * gradLayerGauge k v omega (k - 1)) (bottomGradConst d * Real.rpow 3 (M.gamma * ↑k))

3^{2j} ‖∇ j_{j−1}‖_{W^{1,∞}(3^j v + □_j)} = 𝒪_{Γ₂}(C(d) 3^{γ j}), with the explicit constant C(d) = 9 · shellW1InfSmallerConst d. No exponent is moved: the proved translated display is read at cube scale j, shell scale j − 1, so its (l − k)^{1/2} factor is 1 and its amplitude 3^{γ(j−1)} is at most the target 3^{γ j}.

3. The whole L-free gradient slot as one series

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

The full layer series of the gradient slot at the cube 3^k v + □_k: the bottom layer i = k − 1 together with the whole deep block.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.fullGradSeries k v omega = ∑' (n : ℕ), Algsuperdiff.Section4.Provider.BoundsEaL.gradLayerGauge k v omega (k - 1 + ↑n)

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

The geometric part of the full-slot constant.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.fullGradBase M = (Algsuperdiff.Section4.Provider.BoundsEaL.bottomGradConst d + 3) * (1 - Real.rpow 3 (M.gamma - 1))⁻¹

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

The explicit constant of the full-slot display.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.fullGradConst M = HCPolySupport.IndependentSums.gammaTriangleConst 2 * Algsuperdiff.Section4.Provider.BoundsEaL.fullGradBase M

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

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

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.fullGradAmp {d : ℕ} (M : Section3.ABKModel d) (k : ℤ) (n : ℕ) : ℝ

The amplitude family of the full series: geometric with ratio 3^{γ−1}.

Equations

• Algsuperdiff.Section4.Provider.BoundsEaL.fullGradAmp M k n = (Algsuperdiff.Section4.Provider.BoundsEaL.bottomGradConst d + 3) * Real.rpow 3 (M.gamma * ↑k) * Real.rpow 3 (M.gamma - 1) ^ n

theorem Algsuperdiff.Section4.Provider.BoundsEaL.isBigOWith_gammaSigma_weightedFullGradSeries {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) * fullGradSeries k v omega) (fullGradConst M * Real.rpow 3 (M.gamma * ↑k))

B6, first half, complete: the whole L-free gradient slot has the Step-4 target shape.

3^{2j} Σ_{i ≥ j−1} ‖∇ j_i‖_{W^{1,∞}(3^j v + □_j)} = 𝒪_{Γ₂}(^{γ j}), with the explicit constant C = (9 · shellW1InfSmallerConst d + 3)(1 − 3^{γ−1})^{-1}. No exponent is moved.

4. Identification of the series with the slot

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

Local re-derivation of the private tsum_deepGradTerm_eq of GradSlotMoment.lean: the ℕ-indexed reading of the deep block.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.fullGradSeries_eq_of_summable {d : ℕ} (k : ℤ) (v : Fin d → ℤ) (omega : Section3.Cutoff.CutoffSample d) (hsum : Summable (deepGradTerm k v omega)) : fullGradSeries k v omega = gradLayerGauge k v omega (k - 1) + deepGradSeries k v omega

Where the deep block is summable, the full series really is the bottom layer plus the deep block.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.ae_lFreeGradSlot_eq_weighted_fullGradSeries {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) * fullGradSeries R.scale R.index omega

The L-free gradient slot equals the weighted full series, almost surely.

Combined with isBigOWith_gammaSigma_weightedFullGradSeries this is the Step-4 target shape 𝒪_{Γ₂}(^{γ j}) for the whole slot.