LocalizationFluctuationCellIntegrable #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Sample integrability of the per-cell coarse energies of e.def.w #
LocalizationOscillationDisplay and LocalizationOscillationEndpoint carry one
surviving hypothesis about the sample space, hcellInt:
forall R in the interior meso grid,
Integrable (fun omega => meshEnergyCell (m - h) (grad w_omega) R ^ 4) P .
This module discharges it. Nothing here is a step of the manuscript's argument; it is the measure-theoretic bookkeeping the manuscript leaves implicit.
The obstruction and the route #
CorrectorMeasurableQuartic proves that the quartic window observable
omega |-> fint_W |grad w_omega|^4 is Borel, by a countable supremum of
truncations, because F |-> int_S ‖F‖^4 is not continuous on L^2. The
observable meshEnergyCell needs instead the quadratic window observable
omega |-> fint_W |grad w_omega|^2, and for that no truncation is needed: the
functional
F |-> ( eLpNorm F 2 ((volumeMeasureOn U).restrict S) ).toReal
is 1-Lipschitz on L^2(U), because restriction only decreases the
seminorm and the seminorm obeys the triangle inequality. Its square is the
window integral of ‖F‖^2, so the quadratic window observable is continuous --
not merely Borel -- in the L^2 class, and composing with
CorrectorMeasurableGradient's measurable gradient map gives measurability in
the sample.
Integrability then follows by domination:
meshEnergyCell^4 <= mesoWindowFourthEnergy (per-window Jensen)
<= |cu_K| |W|^{-1} originCubeFourthEnergy
<= |cu_K| |W|^{-1} (2 Chead^2 + 2 T'^2) ,
with T' = max(sqrt(originCubeFourthEnergy) - Chead, 0) the measurable
dominating fluctuation of LocalizationEnvelopeWire -- rebuilt here because it
is private there -- whose square is integrable from the Gamma_1 tail of
e.nablaw.in.L.eight.
Main results #
measurable_volumeAverage_vecNormSq_freshShellDirichletGradand its Neumann mirror -- the quadratic window observable is measurable in the sample.exists_gamma0_integrable_freshShellDirichlet_meshEnergyCell_rpow_fourand its Neumann mirror -- the binderhcellIntof the oscillation endpoint, as a theorem.
Scope #
There is no sorry.
References #
- ABK26,
e.def.w,e.nablaw.oscillations,e.nablaw.in.L.eight.
The Lipschitz window functional on L^2 #
The L^2 size of an L^2 class over a window, read through the seminorm
of the restricted measure.
Equations
Instances For
The restricted norm is controlled by a comparison field and their difference.
The window L^2 functional is 1-Lipschitz on L^2. Restriction only
decreases the seminorm, so the ambient L^2 distance controls the window one.
The square of the window functional is the window integral of ‖F‖^2.
The quadratic window observable at a gradient class #
Unconditional: the normalized second energy of the Dirichlet corrector gradient over any measurable window of the cube is a measurable function of the sample.
wD is an arbitrary family of zero-trace weak solutions of the fresh-shell
Dirichlet problem e.def.w; no measurability, continuity or selection property
of the family is assumed.
Unconditional: the Neumann mirror of the previous statement.
The per-cell coarse energy as a square #
The fourth power of the per-cell coarse energy is the square of the window
average of |u|^2.
: the caller supplies integrability on the window of the coordinate squares of
u.
The window is dominated by the cube #
The window fourth energy is at most the volume ratio times the global
fourth energy, for any window contained in cu_K.
: the caller supplies hsub (the containment) and hfour (integrability of
|u|^4 on cu_K).
The integrability core #
The generic integrability step. Given the pathwise L^8 bound with a
Gamma_1 fluctuation, the measurability of the two window observables, and the
three spatial integrability families on cu_K, the fourth power of the per-cell
coarse energy is integrable in the sample.
: complete binder census beyond the typing binders d, Omega, its MeasurableSpace instance, mu, K, ell, 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, hsq, hfour on cu_K; hsub (the window
containment); and hglobMeas, hcellMeas (measurability in the sample of the
global fourth energy and of the window second energy). No integrability in the
sample is assumed.
The two wired consumers #
hcellInt 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 four spatial families on cu_K, the fourth power of
the per-cell coarse energy over any window contained in cu_K is integrable in
the sample.
Reaches exactly the external anchor
Algsuperdiff.Frozen.External.calderon_zygmund, a proved external,
inherited from exists_freshShell_cubeEuclideanL8_leg_bound.
hcellInt for the Neumann corrector of e.def.w, as a theorem. The
mean-zero Neumann mirror of the previous statement.