LocalizationFluctuationGridEighth #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The grid form of the eighth-moment envelope of the oscillation cell #
LocalizationFluctuationEighthMoment.meshOscillationCell_pow_eight_le_volumeAverage
is the per-cell half of the envelope that the boundary remainder consumes
(LocalizationFluctuationGammaFold.gridFourthMoment_mesoCubeGrid_le_interior_add_of_eighthMoment,
whose binder hE is a bound on the eighth-moment grid average). This
module composes that per-cell bound over the mesh and then over the sample.
What is proved #
cubeFamilyAverage_meshOscillationCell_pow_eight_le_cubeAverage-- the spatial grid composition, at the tiling constant1:
The mesh tiling identityavsum_{z in 3^n Zd cap cu_K} osc(z + cu_n)^8 <= fint_{cu_K} |u|^8 .LocalizationGrid.cubeAverage_originCube_eq_mesoGridAveragesupplies the equality on the right; the per-cell Jensen step supplies the inequality on the left. Nothing is lost: both constants are1.cubeAverage_vecNormSq_pow_four_eq_cubeEuclideanLpNorm_eight_pow_eight-- the dictionary that turnsfint_{cu_K} |u|^8into the eighth power of the manuscript's own volume-normalized EuclideanL^8norm, i.e. into the square of the left-hand side ofe.nablaw.in.L.eight, squared.cubeFamilyAverage_integral_le_of_pointwise-- the sample composition: a pointwise (in the sample) bound of a grid average by a single integrable observable passes to the grid average of the integrals.cubeFamilyAverage_integral_meshOscillationCell_pow_eight_le-- the two composed: the eighth-moment grid average of the oscillation cells is below the expectation of‖u‖^8_{L8bar(cu_K)}.integrable_rpow_four_of_isBigOWith_gammaSigma_oneandintegral_rpow_four_le_of_isBigOWith_gammaSigma_one-- the fourth moment of anO_{Gamma_1}(A)variable,E[T^4] <= (8 e A)^4, in the exact shape of the second-moment pair ofLocalizationEnvelopeMoment; this is the probabilistic input a consumer needs to turne.nablaw.in.L.eight's pathwiseChead + O_{Gamma_1}(gamma^100)into a numeric envelope.freshShellEighthEnergyConstandintegral_le_freshShellEighthEnergyConst-- that numeric envelope,8 Chead^4 + 8 (8 e A)^4, from a measurable dominating fluctuation.
Binders #
The spatial statements carry only the five integrability families on cu_K,
all consequences of the L^8 membership of |u| there, and the scale
bookkeeping n <= K, which only names the mesh. The sample statements carry
the integrability in the sample of the per-cell eighth powers and of the
dominating observable -- the standing integrability of the very moments being
formed. No smallness, normalization or moment assumption occurs, and nothing
about the corrector, the coefficient field or the model is assumed.
Not proved here. The measurability in the sample of omega |-> fint_{cu_K} |u(omega)|^8 -- the octic analogue of Corrector.CorrectorMeasurableQuartic
-- is not established, so the dominating observable of
cubeFamilyAverage_integral_meshOscillationCell_pow_eight_le is a binder
rather than a construction. Corrector.FreshShellL8 produces its fluctuation
Tfluct existentially and asserts nothing about its measurability, exactly as
LocalizationEnvelopeMoment records; LocalizationEnvelopeWire removes that
binder at the fourth power by dominating Tfluct with a measurable variable
built from the quartic layer, and the same device at the eighth power needs the
octic layer. That octic layer is available as
Corrector.CorrectorMeasurableOctic, and the envelope construction discharging
this binder is LocalizationFluctuationSplitOscEnvelope; the binder form below
is retained for generality and is not assumed away.
Scope #
There is no sorry.
References #
- ABK26,
e.nablaw.oscillations,e.lower.bound.oscillations,e.nablaw.in.L.eight.
The measure-zero boundary step, on an arbitrary triadic cube #
Unconditional. The open-cube volume average is the half-open cube average; the two cube realizations differ by their Lebesgue-null boundary.
LocalizationFluctuationDuality states the same identity, but is outside this
importing a whole duality layer for it.
The spatial grid composition #
The eighth-moment envelope at the mesh, spatially. The grid average
over 3^n Zd cap cu_K of the eighth powers of the oscillation cells of
e.nablaw.oscillations is below the single normalized eighth moment of u on
cu_K. Both the per-cell constant and the tiling constant are 1.
Conditional on the scale containment hn -- which only names the mesh -- and on the five
integrability families on cu_K, all consequences of the L^8 membership of
|u| there.
The dictionary to e.nablaw.in.L.eight #
Unconditional in the cube data, conditional on the L^8 membership.
The half-open cube average of |u|^8 is the eighth power of the manuscript's
volume-normalized Euclidean L^8 norm. This is the exact square of the
left-hand side of e.nablaw.in.L.eight.
The sample composition #
The sample half of the composition. If, at every sample point, the grid
average of a family is below one observable G, then the grid average of the
integrals is below the integral of G.
Conditional on the integrability of each member of the family and of G, and on the
pointwise bound. This is nothing but linearity of the integral on a finite
average, plus monotonicity.
The eighth-moment grid average of the oscillation cells. The spatial
composition, integrated: the quantity the boundary remainder consumes is below
the expectation of the eighth power of the normalized Euclidean L^8 norm of
u on cu_K -- the square of the quantity e.nablaw.in.L.eight controls.
Conditional on the scale bookkeeping hn, the five spatial integrability families (per
sample point), the integrability in the sample of the per-cell eighth powers,
and the integrability of the dominating observable G together with the
pathwise bound hpath. No smallness or moment assumption occurs.
The fourth moment of an O_{Gamma_1}(A) variable #
The fourth power of an O_{Gamma_1}(A) variable is integrable.
: [IsProbabilityMeasure mu], hA, hT0, hTm, hT.
The fourth moment of an O_{Gamma_1}(A) variable: E[T^4] <= (8 e A)^4.
The constant is CoarseGraining's gammaMomentConst 1 * 4^{1} = 2 e * 4 = 8 e,
raised to the fourth power; nothing below sharpens it. This is the exact
fourth-power mirror of
LocalizationEnvelopeMoment.integral_sq_le_of_isBigOWith_gammaSigma_one.
: [IsProbabilityMeasure mu], hA, hT0, hTm, hT.
The eighth-energy envelope constant #
The annealed eighth-energy envelope: 8 Chead^4 + 8 (8 e A)^4, where
Chead is the head constant of e.nablaw.in.L.eight and A its fluctuation
amplitude. The two 8s are the constants of (a+b)^4 <= 8 a^4 + 8 b^4.
Equations
Instances For
The numeric envelope, from a measurable dominating fluctuation. If
G <= (Chead + T)^4 pointwise with T a nonnegative, a.e.-measurable
O_{Gamma_1}(A) variable, then E[G] <= 8 Chead^4 + 8 (8 e A)^4.
: [IsProbabilityMeasure mu], hA, hT0, hTm, hT, the integrability of
G and the pointwise domination hGle. No sign hypothesis on Chead is
needed.