GammaTenStripCellSquare #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two per-cell second moments of the strip data, regime-free #
ABK26, Step 2 of l.approximate.recurrence.formula, e.Pz.def, e.Fz.def,
e.nablaw.in.L.eight.
What this module supplies #
Closure.GammaTenStripBound.gammaTenStrip_cell_average_sq_le and
cubeFamilyAverage_integral_sq_stripCellPotentialDatum_le_of_majorant
both carry a per-cell binder hDsq (resp. hFsq): at each cell of the mesh,
the square of the cell datum is sample-integrable. This module discharges both
binders at the closure's own corrector families
Closure.SplitProducerFold.closureDirichletAlong,
Closure.SplitProducerFold.closureNeumannAlong, from one integrable pathwise
dominator per leg and nothing else.
The route, in one line #
Per cell, the datum is below twice its own background cell energy
(Closure.GammaTenStripEnergy.stripCellPotentialDatum_le_two_mul_energy, whose
only input is the cell L^2 membership of the leg field, itself the restriction
of the L^8 membership e.nablaw.in.L.eight on cu_K), the cell energy is a
gauge times a cube average
(Closure.GammaTenStripEnergy.meshCellBackgroundPotentialEnergy_eq_cubeAverage),
and the square of that cube average is below the fourth energy of the leg field
on the whole localization cube times a purely geometric volume ratio:
( fint_R |u|^2 )^2 <= fint_R |u|^4 <= |R|^{-1} |cu_K| . fint_{cu_K} |u|^4 ,
the first step Jensen at the cell (CoarseGraining
sq_cubeAverage_le_cubeAverage_sq_of_memLp), the second the window/cube
comparison
LocalizationFluctuationCellIntegrable.mesoWindowFourthEnergy_le_ratio_mul_originCubeFourthEnergy'
read at the cell's own scale. So
( datum_R )^2 <= 4 . gauge^2 . |R|^{-1} |cu_K| . fint_{cu_K} |u|^4 ,
and the caller's integrable pathwise majorant G of fint_{cu_K} |u|^4
finishes it through Integrable.mono'. The constant is explicit and depends on
R, K and d; no uniformity in the cell is claimed or needed, because the
statement is a per-cell integrability, not an estimate.
Measurability of the datum in the sample is assembled exactly as in
Closure.SplitFoldCellMoments: the energy leg through the measurable
L^2-class engine
Closure.SplitFoldCellMoments.measurable_volumeAverage_vecNormSq_of_measurable_class
at the two proved background classes of
LocalizationFluctuationBackgroundClass, the load leg through
Closure.SplitProducerLoad.measurable_meshCellLoad.
Binders, and what is NOT assumed #
Beyond the typing binders d, [NeZero d], M, n, h, K, e, e', jd,
R: the dimension gate hd : 2 <= d, the geometric membership hR of the cell
in the localization cube, and the three properties hG0, hGint, hGD (resp.
hGN) of the caller's dominator.
There is no smallness gate, no InductionState, no
M.gamma <= gamma0, no direction bound |e| <= 1 or |e'| <= 1, no
0 < h, and no recurrence-parameter hypothesis of any kind. In particular this
module does not route through
exists_gamma0_integrable_freshShellDirichlet_meshEnergyCell_rpow_four,
which carries all of those; the potential-leg mirror
Closure.SplitFoldCellMoments.integrable_meshCellBackgroundPotentialEnergy_sq_of_meshEnergyCell
is used only as a proof template and is not consumed.
Scope #
Internal Provider infrastructure for the Step-2 fluctuation estimate. There is
no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
l.approximate.recurrence.formulaStep 2,e.Pz.def,e.Fz.def,e.nablaw.in.L.eight.
Membership bookkeeping #
The pathwise cell-to-cube step #
The potential leg #
The second sample moment of the strip's potential cell datum, regime-free.
At any cell R of the localization cube cu_K and at the closure's own
corrector families, the square of Closure.GammaTenStripBound.stripCellPotentialDatum
is sample-integrable as soon as the caller exhibits one integrable pathwise
majorant G of the potential leg's fourth energy fint_{cu_K} |e' + grad w_D|^4.
There is no smallness gate, no induction state, no direction bound and no recurrence parameter.
Proved from memLp_eight_grad_closureDirichletAlong.
The flux leg #
The second sample moment of the strip's flux cell datum, regime-free.
The flux mirror of integrable_stripCellPotentialDatum_sq_closure: at any cell
R of cu_K, the square of Closure.GammaTenStripBound.stripCellFluxDatum is
sample-integrable as soon as the caller exhibits one integrable pathwise majorant
G of the flux leg's fourth energy fint_{cu_K} |e + bfF|^4.
Conditional exactly as its potential mirror, and proved from
memLp_eight_neumannFluxField_closure.