LocalizationFluctuationEighthMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-cell eighth-moment envelope of the oscillation cell #
LocalizationFluctuationGammaFold.gridFourthMoment_mesoCubeGrid_le_interior_add_of_eighthMoment
closes the boundary remainder against an eighth-moment grid average of the
same per-cell quantity, and
LocalizationFluctuationGammaFold.exists_gamma_threshold_mesh_boundary then
puts that remainder below gamma^100. What the consumer still owes is the
spatial half of that envelope: a pointwise (in the sample) bound of the
eighth power of the oscillation cell of e.nablaw.oscillations by the cell
average of |u|^8, whose grid average the mesh tiling identity of
LocalizationGrid turns into the single quantity fint_{cu_K} |u|^8 that
e.nablaw.in.L.eight controls.
This module proves that spatial half. Two elementary steps do the work, at the
constant 1 in both.
- Variance is below the second moment.
meanSquareOscillationVecOncentres the field at its own window average; dropping the centring costs nothing:volumeAverage_sub_volumeAverage_sq_le. This replaces the manuscript's implicit triangle inequality and avoids its2^7. - Jensen twice.
(fint g)^4 <= fint g^4forg = |u|^2 >= 0, by two applications of Cauchy--Schwarz against the constant1(sq_volumeAverage_le_volumeAverage_sq). This is the same normalized Cauchy--SchwarzLocalizationEnvelopeMeshuses at one level, restated on a general set of finite positive volume so it can be iterated.
meshOscillationCell_pow_eight_le_volumeAverage is the composed statement, and
volumeAverage_vecNormSq_pow_four_eq_cubeEuclideanLpNorm_eight_pow_eight is the
dictionary that turns its right-hand side into the eighth power of the
volume-normalized Euclidean L^8 norm -- verbatim the left-hand side of
Corrector.FreshShellL8.exists_cubeEuclideanL8_gradient_sq_sum_le_const_add_gammaPow.
Binders #
hsc -- the cell is read at its own scale, which only names n; and the
integrability families, which are the standing spatial integrability of the
moments being formed (all four follow from the L^8 membership of |u| on the
cube, which is what e.nablaw.in.L.eight supplies). They are conditional A
obligations discharged by the caller. No smallness, no moment, no
measurability in the sample, and nothing about the corrector, the coefficient
field or the sample space occurs.
Scope #
There is no sorry.
References #
- ABK26,
e.nablaw.oscillations,e.lower.bound.oscillations,e.nablaw.in.L.eight.
Cauchy--Schwarz against the constant, on a general window #
Cauchy--Schwarz against 1 on a set of finite positive volume:
(int_V g)^2 <= |V| int_V g^2.
on the volume data and the two integrabilities.
Normalized Cauchy--Schwarz on a general window. The square of the window
average is below the window average of the square; the constant is 1. Stated
on a general set so that it can be iterated, which is what the eighth moment
needs.
The exact form of the centring step. The window average of the squared deviation from the window average is the window average of the square minus the square of the window average.
on the volume data and the two integrabilities; this is the equality whose
inequality half is
LocalizationFluctuationEighthMoment.volumeAverage_sub_volumeAverage_sq_le.
Variance is below the second moment. Dropping the centring in
meanSquareOscillationVecOn costs nothing.
The oscillation cell against the window energy #
The coordinate squares average to the squared Euclidean gauge.
on the coordinate integrabilities.
The oscillation is a difference of two window observables. The mean-square oscillation of a vector field over a window is the window average of its squared gauge minus the squared gauge of its window average.
on the volume data and the coordinate integrabilities. This is the identity
that makes the oscillation cell measurable in the sample: both terms on the
right are window observables of the L^2 class.
The mean-square oscillation is below the mean-square size. Componentwise
volumeAverage_sub_volumeAverage_sq_le, summed over the coordinates.
on the volume data and the coordinate integrabilities.
The volume data of an open triadic cube #
Unconditional: an open triadic cube has finite volume.
Unconditional: an open triadic cube has positive volume.
The eighth-moment envelope of the oscillation cell #
The pointwise Jensen step of the eighth-moment envelope. At the cell's
own scale the eighth power of the oscillation cell of e.nablaw.oscillations is
below the cell average of |u|^8; the constant is 1.
on the identification hsc of the cell's scale and on the five integrability
families -- all consequences of the L^8 membership of |u| on the cube,
which is what e.nablaw.in.L.eight supplies. The volume data of the open cube
is discharged internally.