Step5InputGradMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
hgradM: the grid fourth moment of the Dirichlet corrector's cube averages #
ABK26, e.nablaw.in.L.eight, read inside Step 5 of
l.approximate.recurrence.formula.
Closure.Step5Basket.step5GaugeEndpoint_closureFamilies_of_momentLegs leaves
hgradM as the binder
( avsum_{R in grid} E[ |(grad w_D)_R|^4 ] )^{1/2}
<= C2 * shom_n^{-2} * h * 3^{2 cgamma (n+h)} .
The route #
The manuscript's own three steps, in order.
- The grid step. The grid tiles
cu_K, so per-cube Jensen followed by the tiling identity gives, at fixed sample and with no dependence onK,
which isavsum_R |(grad w_D)_R|^4 <= 8 ||grad w_D||_{L8bar(cu_K)}^4 ,PrincipalResponseDisplayTwoGrid.descendantsAverage_sq_vecNormSq_add_cubeAverageVec_leatc = 0. The grid fourth moment is a finite average of integrals, so the sample integral may be taken outside. - Calderon--Zygmund.
Corrector.exists_cubeEuclideanL8_gradient_sq_sum_lebounds||grad w_D||^2_{L8bar(cu_K)}by theL^8norm of the forcing ofe.def.w, whichCorrector.cubeEuclideanLpNorm_streamForcing_lereads asshom_n^{-1} ||k_{n+h} - k_n||_{L8bar(cu_K)}. e.km.kn.Lp.Corrector.exists_streamIncrementLpNormSq_head_tail--- the proved frozen theorem --- splits that square into the headC h 3^{2 cgamma (n+h)}and aGamma_1tail whose amplitude carries the extra decay3^{-(K-m)d/8} <= 1. Its second moment isLocalizationEnvelopeMoment.integral_sq_le_of_isBigOWith_gammaSigma_one', so the fourth moment of theL^8norm is at most an absolute multiple of the head squared, and the square root of the grid moment is the display.
References #
- ABK26,
e.nablaw.in.L.eight;e.km.kn.Lp; Step 5.
The grid step, at fixed sample #
Per-cube Jensen and the tiling identity, at c = 0. The grid average of
the fourth power of the cube averages of a field is at most 8 times the fourth
power of its normalized Euclidean L^8 norm on the ambient cube. No dependence
on the depth j.
The per-cube form of the same estimate, with the grid cardinality: enough for integrability, not for the display.
Taking the sample integral outside the grid average #
The grid fourth moment under a pathwise grid bound. The grid is finite, so the sample integral commutes with its average.
The L^8 carrier of e.km.kn.Lp, made measurable #
The volume-normalized L^8 norm of the fresh shell on cu_K is a random
variable.
The fourth moment of the fresh-shell L^8 norm on cu_K.
e.km.kn.Lp (the proved frozen theorem) splits ||k_m - k_n||^2_{L8bar(cu_K)} into a head and a Gamma_1 tail whose amplitude carries
the factor 3^{-(K-m)d/8} <= 1. Replacing the anchor's tail variable by the
measurable positive part max(L^2 - head, 0) --- which the anchor's own
bound dominates --- makes the second moment available, and the fourth moment of
L follows.
Both the bound and the integrability are produced; no measurability of the anchor's own tail variable is assumed.
hvmem and hgradM at the closure's Dirichlet family #
hvmem and hgradM, proved.
One constant, produced before the model, such that at every admissible pair
(n, n+h) and every localization scale K >= n+h the closure's own Dirichlet
family satisfies both Step-5 gradient legs: the cube averages are L^4 in the
sample, and the square root of their grid fourth moment obeys
e.nablaw.in.L.eight in the shape the manuscript reads it.
The depth j is arbitrary: the grid step is the tiling identity, which holds at
every depth.
Proved from Corrector.exists_cubeEuclideanL8_gradient_sq_sum_le and
ApproximateRecurrence.memLp_eight_grad_freshShellDirichlet, hence from the
external Calderon--Zygmund input
Algsuperdiff.Frozen.External.calderon_zygmund.