GammaTenLoad

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

The load leg of the cgamma^{10} estimate

ABK26, Step 2 of l.approximate.recurrence.formula, the display

  ( avsum_{z in 3^n Zd cap cu_K}  E[ | bfAhom_{m-h}^{1/2} P_z |^4 ] )^{1/4}
      <=  C ,

quoted there "by e.nablaw.in.L.eight" (label).

The gap this module fills

PrincipalResponseMomentsFourth carries the whole pathwise chain of the display --- the collapse of the normalization (annealedSqrtNormSq_principalPz_eq), the fourth power (sq_annealedSqrtNormSq_principalPz_le) and its grid form --- and records explicitly that "the final numerical bound by the dimensional constant C is not proved": that bound needs e.nablaw.in.L.eight, which the module does not invoke. This module supplies exactly that missing step, at the closure's own corrector families and under the closure's own law (cutoffSampleLaw M).toMeasure.

The route

Four steps, all of them the manuscript's own.

1. Pathwise, per cell. sq_annealedSqrtNormSq_principalPz_le at the load's own gauge (gaugeRatio_self) bounds | bfAhom^{1/2} P_z |^4 by the fourth powers of the two averaged legs e' + (grad w_D)_R and e + (grad w_N + shom^{-1} h e')_R.
2. The grid re-assembly. PrincipalResponseDisplayTwoGrid.descendantsAverage_sq_vecNormSq_add_cubeAverageVec_le turns the grid average of each leg into the constant term and the volume-normalized Euclidean L^8 norm of the field on cu_K; the depth j drops out, because the grid tiles cu_K. This is descendantsAverage_sq_annealedSqrtNormSq_principalPz_le_norms.
3. e.nablaw.in.L.eight, lines (i) and (ii). Calder'on--Zygmund (Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le) releases the two corrector gradients against the forcing of e.def.w, and Corrector.cubeEuclideanLpNorm_streamForcing_le reads that forcing as shom_n^{-1} ||k_{n+h} - k_n||_{L8bar(cu_K)}. The flux leg is the Neumann gradient plus the same forcing, so Minkowski (PrincipalResponseDisplayTwoGrid.cubeEuclideanLpNorm_add_le) puts it on the same carrier. What is left is the single measurable random variable L(omega) = ||k_{n+h} - k_n||_{L8bar(cu_K)} --- this is exists_gammaTenLoadPathwiseConst.
4. e.km.kn.Lp and line (iii). The fourth moment of L under the cutoff sample law is the proved Step5InputGradMoment.exists_integral_streamIncrementLpNorm_eight_pow_four_le (the proved frozen theorem with its Gamma_1 tail replaced by a measurable positive part), and the deterministic normalization Corrector.inv_sigmaBarSq_mul_shellWidth_le --- shom_n^{-2} h 3^{2 cgamma (n+h)} <= 24 * 3^18 --- turns the resulting bound into an absolute constant. This is exists_gammaTenLoadConst.

The shape delivered, and why it is a grid average

The source display is a grid average over z in 3^n Zd cap cu_K, and so is the statement here: gridFourthMoment, respectively gridFourthMomentRoot, over descendantsAtDepth cu_K j. A uniform per-cell fourth moment is not available and is not claimed: the grid step of item 2 above is the tiling identity avsum_R fint_R = fint_{cu_K}, which loses a factor 3^{jd} when read at a single cell. The companion module Closure.GammaTenLoadFold therefore supplies the grid-load variant of Closure.GammaTenGridFold.descendantsAverage_integral_fold_le_of_moments, whose hload binder is exactly exists_gammaTenLoadConst_root's conclusion.

Binders

All binders are regime binders: the induction state Algsuperdiff.Frozen.Section3.inductionState M m0 Ec and the parameters of e.recurrence.params --- 0 < h, n <= m0, h <= 6 cstar cgamma^{-1}, n + h <= K --- together with |e|, |e'| <= 1 and the standing 2 <= d. Nothing about the corrector families is assumed: they are the closure's own closureDirichletAlong and closureNeumannAlong, whose two weak formulations are proved in Closure.SplitProducerFold. No smallness gate on cgamma occurs, and the constant is produced before the model.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2; the load display; e.Pz.def; e.nablaw.in.L.eight; e.km.kn.Lp; e.recurrence.params.

Elementary arithmetic

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gaugeRatio_self (sigma : Observable.PositiveScalar) : gaugeRatio sigma sigma = 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.pow_four_add_le (a b : ℝ) : (a + b) ^ 4 ≤ 8 * (a ^ 4 + b ^ 4)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sq_vecNormSq_le_one {d : ℕ} {v : HCPolySupport.Vec d} (hv : HCPolySupport.Book.Ch02.vecNorm v ≤ 1) : HCPolySupport.vecNormSq v ^ 2 ≤ 1

The pathwise grid bound of the load

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.descendantsAverage_sq_annealedSqrtNormSq_principalPz_le_norms {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (n m : ℤ) {e e' : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e ≤ 1) (he' : HCPolySupport.Book.Ch02.vecNorm e' ≤ 1) (Q : HCPolySupport.TriadicCube d) (j : ℕ) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (hD : MeasureTheory.MemLp wD.grad 8 (HCPolySupport.normalizedCubeMeasure Q)) (hF : MeasureTheory.MemLp (neumannFluxField sigma omega n m e' wN) 8 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => annealedSqrtNormSq sigma (principalPz sigma omega n m e e' R wD wN) ^ 2) ≤ 32 + 16 * Corrector.cubeEuclideanLpNorm Q 8 wD.grad ^ 4 + 16 * Corrector.cubeEuclideanLpNorm Q 8 (neumannFluxField sigma omega n m e' wN) ^ 4

The grid average of |bfAhom^{1/2}P_z|^4 at a fixed sample.

PrincipalResponseMomentsFourth.descendantsAverage_sq_annealedSqrtNormSq_principalPz_le read at the load's own gauge, with the two grid legs released by PrincipalResponseDisplayTwoGrid.descendantsAverage_sq_vecNormSq_add_cubeAverageVec_le into the volume-normalized L^8 norms of e.nablaw.in.L.eight.

only on the two L^8 memberships and on the two direction bounds |e|, |e'| <= 1.

The pathwise majorant, in the fresh-shell carrier alone

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gammaTenLoadPathwiseConst (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (Cpath : ℝ), 0 < Cpath ∧ ∀ (M : ABKModel d) (n : ℤ) (h K j : ℕ) (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (omega : Cutoff.ShellSeq d), (HCPolySupport.descendantsAverage (HCPolySupport.originCube d ↑K) j fun (R : HCPolySupport.TriadicCube d) => annealedSqrtNormSq (Annealed.sigmaBar M n) (principalPz (Annealed.sigmaBar M n) omega n (n + ↑h) e e' R (closureDirichletAlong M n h K e omega) (closureNeumannAlong M n h K e' omega)) ^ 2) ≤ 32 + Cpath * ((↑(Annealed.sigmaBar M n))⁻¹ * Stream.streamIncrementLpNorm 8 (↑K) n (n + ↑h) omega) ^ 4

The grid average of |bfAhom^{1/2}P_z|^4 at the closure's own families, majorized by the fresh-shell L^8 carrier.

Calderon--Zygmund releases the two corrector gradients against the forcing of e.def.w, and Corrector.cubeEuclideanLpNorm_streamForcing_le reads the forcing as shom_n^{-1} ||k_{n+h} - k_n||_{L8bar(cu_K)}. What is left on the right is the single measurable carrier of e.km.kn.Lp.

Proved from Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le and memLp_eight_grad_closure{Dirichlet,Neumann}Along, hence from the external Calderon--Zygmund input Algsuperdiff.Frozen.External.calderon_zygmund.

The annealed load leg

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.rpow_four_sqrt {v : ℝ} (hv : 0 ≤ v) : √v ^ 4 = v ^ 2

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gammaTenLoadConst (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (Cload : ℝ), 0 < Cload ∧ ∀ (M : ABKModel d) (m0 : ℤ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ec → ∀ (n : ℤ) (h K j : ℕ) (e e' : HCPolySupport.Vec d), 0 < h → n ≤ m0 → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → n + ↑h ≤ ↑K → HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → (gridFourthMoment (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) fun (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => √(annealedSqrtNormSq (Annealed.sigmaBar M n) (meshCellLoad M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega))) ≤ Cload ^ 4

The load leg of the cgamma^{10} estimate, proved.

One absolute constant Cload, produced before the model, such that on the closure's own grid the fourth moment of the localized principal load obeys the display,

  ( avsum_{R in descendantsAtDepth cu_K j}  E[ | bfAhom_n^{1/2} P_R |^4 ] )^{1/4}
      <=  Cload ,

at the recurrence's own parameters and uniformly in the localization scale K and the depth j.

All binders are regime binders of e.recurrence.params and the induction state; nothing about the corrector families is assumed beyond their being the closure's own.

This is the manuscript's own "by e.nablaw.in.L.eight" and nothing more.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_gammaTenLoadConst_root (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (Cload : ℝ), 0 < Cload ∧ ∀ (M : ABKModel d) (m0 : ℤ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ec → ∀ (n : ℤ) (h K j : ℕ) (e e' : HCPolySupport.Vec d), 0 < h → n ≤ m0 → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → n + ↑h ≤ ↑K → HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → (gridFourthMomentRoot (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) j) fun (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) => √(annealedSqrtNormSq (Annealed.sigmaBar M n) (meshCellLoad M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega))) ≤ Cload

The load leg in the root spelling the grid fold consumes.

exists_gammaTenLoadConst read through the fourth root: this is the hload binder of GammaTenLoadFold.descendantsAverage_integral_fold_le_of_grid_moments, verbatim.

Inherited from exists_gammaTenLoadConst.