PrincipalResponseMomentsFourth #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: sub-step (iv) of the principal response, the fourth-moment display #
Source display in ABK26, inside Step 3 of the proof of
l.approximate.recurrence.formula (label):
( avsum_{z in 3^n Zd cap cu_K} E[ | bfAhom_{m-1}^{1/2} P_z |^4 ] )^{1/4} <= C .
The manuscript proves the same display at the gauge m - h earlier in the same
proof ("and we get, by e.nablaw.in.L.eight"), and quotes it at the gauge `m
- 1` here. Two things separate the two readings, and this module supplies both of them:
- the gauge transport from
shom_{m-h}toshom_{m-1}, which costs exactly the ratiomax( shom_{m-1}/shom_{m-h} , shom_{m-h}/shom_{m-1} )on the squared length and its square on the fourth power; and - the collapse of the normalization, which is sub-step (ii): because
P_zis by definitionbfAhom_{m-h}^{-1/2}applied to the raw averaged slope pair,| bfAhom_{m-h}^{1/2} P_z |^2is the unnormalized|e' + (grad w_D)_R|^2 + |e + (grad w_N + shom^{-1} h e')_R|^2.
What is proved here, and what is not #
Everything below is pathwise: an inequality between explicit functions of
the sample and of the two correctors, with no expectation taken. The
manuscript's own display is an inequality between expectations, so the
statements here are strictly stronger in that respect, and strictly weaker in
another: the final numerical bound by the dimensional constant C is not
proved. That bound needs e.nablaw.in.L.eight (label) together with the
comparison of the volume-normalized L^4 and L^8 norms on cu_K and the
second moment of the Gamma_1 fluctuation it carries; none of those is invoked
below, and no declaration here asserts the display's right-hand side.
The two grid averages that remain on the right-hand side of
descendantsAverage_sq_annealedSqrtNormSq_principalPz_le are exactly the two
quantities that e.nablaw.in.L.eight is quoted for. They are named, not
bounded.
The eLpNorm bridges #
The companion module PrincipalResponseLegsBudget takes the two moments in
seminorm form, as the binders hBn : ‖B‖_8 <= Cb and hVn : ‖V‖_4 <= Cv.
eLpNorm_le_ofReal_of_integral_rpow_le and its two specializations turn a real
moment bound E[X^p] <= C^p -- the form in which both displays are printed --
into exactly those binders, so that neither has to be stated twice.
Main results #
annealedSqrtNormSq,annealedSqrtNormSq_nonneg-- the integrand| bfAhom^{1/2} P |^2of the display, and its nonnegativity.gaugeRatio,annealedSqrtNormSq_le_gaugeRatio_mul,sq_annealedSqrtNormSq_le_gaugeRatio_sq_mul-- the gauge transport.annealedSqrtNormSq_principalPz_eq-- the collapse, from sub-step (ii).sq_annealedSqrtNormSq_principalPz_le-- the pathwise fourth power.descendantsAverage_sq_annealedSqrtNormSq_principalPz_le-- the grid form.eLpNorm_le_ofReal_of_integral_rpow_le,eLpNorm_eight_le_ofReal_of_moment,eLpNorm_four_le_ofReal_of_moment-- the seminorm bridges.
The integrand #
| bfAhom^{1/2} P |^2. The shom-weighted squared length of a doubled
load, shom |P_1|^2 + shom^{-1} |P_2|^2.
Equations
- Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedSqrtNormSq sigma Y = ↑sigma * HCPolySupport.vecNormSq Y.1 + (↑sigma)⁻¹ * HCPolySupport.vecNormSq Y.2
Instances For
The gauge transport #
The cost of reading the display at a different gauge: the larger of the two
diffusivity ratios. At the manuscript's two scales, e.shom.h.bounds bounds
it by a dimensional constant, which is why the printed constant C does not
change between.
Equations
- Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugeRatio sigmaLow sigmaTop = max (↑sigmaTop / ↑sigmaLow) (↑sigmaLow / ↑sigmaTop)
Instances For
The gauge transport. Changing the gauge of the squared length costs at most the larger of the two diffusivity ratios.
The gauge transport on the fourth power, which is what raises to.
The collapse of the normalization: sub-step (ii) #
The collapse at the load's own gauge. ellipticityBudget_eq read
through annealedSqrtNormSq: at the gauge that defines P_z the two
normalizations cancel exactly, leaving the raw averaged slope pair.
The pathwise fourth power #
The pathwise fourth power, at the display's gauge. For the localized load
P_z of e.Pz.def built at sigmaLow and read through the gauge sigmaTop,
| bfAhom_{sigmaTop}^{1/2} P_z |^4
<= 2 rho^2 ( |e' + (grad w_D)_R|^4
+ |e + (grad w_N + sigmaLow^{-1} h e')_R|^4 ) ,
with rho = gaugeRatio sigmaLow sigmaTop.
The grid form #
The grid form. Averaging the pathwise fourth power over the triadic
subcubes of Q = cu_K at the localization depth j = K - n:
avsum_R | bfAhom_{sigmaTop}^{1/2} P_R |^4
<= 2 rho^2 ( avsum_R |e' + (grad w_D)_R|^4
+ avsum_R |e + (grad w_N + sigmaLow^{-1} h e')_R|^4 ) .
The seminorm bridges #
From a printed moment to the seminorm binder. Both displays are printed as
real moment roots (E[X^p])^{1/p} <= C; the Hoelder leg consumes them as
eLpNorm bounds. For a nonnegative X in L^p the two are the same
statement.
The binder hBn. The eighth moment of the operator norm, in the seminorm
form the Hoelder leg consumes.
The binder hVn. The fourth moment of the normalized load length, in the
seminorm form the Hoelder leg consumes.