LocalizationFluctuationNumericOctic #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
hmem8: the L^2-in-the-sample membership of the oscillation cells #
LocalizationOscillationFullMesh carries two e.nablaw.in.L.eight side
conditions into the Step-5 shape. The first of them is
forall R in the mesh,
MemLp (fun omega => osc(z_R + cu_n; grad w_omega) ^ 4) 2 P ,
i.e. the finiteness of the eighth moment of the oscillation cell together with its measurability in the sample. This module discharges it.
The two halves #
Measurability. CorrectorMeasurableQuartic and
LocalizationFluctuationCellIntegrable supply the quartic and the quadratic
window observables; what the oscillation cell needs on top of the quadratic
one is the centring, and the centring is a difference of two window
observables:
osc^2(V; u) = fint_V |u|^2 - |fint_V u|^2 ,
meanSquareOscillationVecOn_eq_sub_vecNormSq_volumeAverageVec below. The first
term is measurable by
measurable_volumeAverage_vecNormSq_freshShellDirichletGrad; the second is a
finite sum of squares of the linear window observables of
Corrector.measurable_setIntegral_gradCoordL2, which are continuous. So the
oscillation cell -- more precisely its fourth power, which is osc^2 squared
and therefore free of the square root -- is measurable in the sample.
Finiteness. Domination, exactly as in
LocalizationFluctuationCellIntegrable, one power up:
osc^8 <= fint_{z+cu_n} |u|^8 (per-cell Jensen)
<= |cu_K| |z+cu_n|^{-1} fint_{cu_K} |u|^8 (window <= cube)
= |cu_K| |z+cu_n|^{-1} (‖u‖^2_{L8bar(cu_K)})^4
<= |cu_K| |z+cu_n|^{-1} (Chead + T')^4 ,
with T' = max((fint_{cu_K} |u|^8)^{1/4} - Chead, 0) the measurable dominating
fluctuation -- the octic analogue of the device of
LocalizationFluctuationCellIntegrable, measurable because
CorrectorMeasurableOctic makes fint_{cu_K} |u|^8 measurable -- whose fourth
power is integrable from the Gamma_1 tail of e.nablaw.in.L.eight
(LocalizationFluctuationGridEighth.integrable_rpow_four_of_isBigOWith_gammaSigma_one).
Main results #
meanSquareOscillationVecOn_eq_sub_vecNormSq_volumeAverageVec-- the centring identity.measurable_meshOscillationCell_rpow_four_freshShellDirichletGradand its Neumann mirror -- the fourth power of the oscillation cell is measurable in the sample.exists_gamma0_memLp_two_freshShellDirichlet_meshOscillationCell_rpow_fourand its Neumann mirror -- the binderhmem8ofLocalizationOscillationFullMesh, as a theorem.
Scope #
There is no sorry.
References #
- ABK26,
e.def.w,e.nablaw.oscillations,e.nablaw.in.L.eight,e.lower.bound.oscillations.
The oscillation cell as a square #
The fourth power of the oscillation cell is the square of the mean-square oscillation over the cell's own realization.
only on the scale identification hsc, which names the cell.
The square of the fourth power of the oscillation cell is its eighth power. Unconditional apart from the nonnegativity, which is automatic.
Measurability of the oscillation cell #
A representative identified almost everywhere gives the same coordinate window integral.
Oscillation is measurable for arbitrary representatives of measurable L² classes.
Quadratic-observable measurability and the window integrabilities remain explicit premises.
Unconditional in the sample: the fourth power of the oscillation cell of
e.nablaw.oscillations is a measurable function of the sample, for an
arbitrary family of zero-trace weak solutions of e.def.w.
on the cell data hsc, hsub and on the two coordinate integrability families
on the cell.
The Neumann mirror of the previous statement.
The cell is dominated by the cube #
The cell average of |u|^8 is at most the volume ratio times the cube
average of |u|^8, for any cell contained in cu_K.
: the containment hsub and the integrability height on cu_K.
The integrability core #
A measurable nonnegative fourth-power envelope inherits integrability and the explicit eighth-energy bound, even when the dominating fluctuation is not measurable.
The generic MemLp step. Given the pathwise L^8 bound with a
Gamma_1 fluctuation, the measurability of the two octic observables, and the
six spatial families on cu_K, the fourth power of the oscillation cell is
L^2 in the sample.
: complete binder census beyond the typing binders d, Omega, its MeasurableSpace instance, mu, K, n, R, u, Chead, A, T: [IsProbabilityMeasure mu]; hChead : 0 <= Chead; hA : 0 < A; hT0, hT (the Gamma_1 tail);
hmem, hpath (the spatial L^8 membership and the pathwise L^8 bound);
hcoord, hcoordsq, hsq, hfour, height on cu_K; hsc, hsub (the
cell data); and hglobMeas, hcellMeas (measurability in the sample of the
cube's eighth energy and of the fourth power of the cell). No integrability in
the sample is assumed.
The two wired consumers #
hmem8 for the Dirichlet corrector of e.def.w, as a theorem.
For every gamma below one explicit threshold, in the whole parameter range of
e.recurrence.params, and for every sample family of zero-trace weak solutions
of e.def.w obeying the six spatial families on cu_K, the fourth power of the
oscillation cell of any cell contained in cu_K is L^2 in the sample.
Reaches exactly the external anchor
Algsuperdiff.Frozen.External.calderon_zygmund, a proved external,
inherited from exists_freshShell_cubeEuclideanL8_leg_bound.
hmem8 for the Neumann corrector of e.def.w, as a theorem. The
mean-zero Neumann mirror of the previous statement.