GammaTenStripBound #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The hstrip binder, at the crude elliptic majorant #
ABK26, Step 2 of l.approximate.recurrence.formula,
e.lower.bound.basic.split, e.CG.bounds.2.
What this module is #
cubeFamilyAverage_sq_integral_meshFluctuationCellIntegrand_le_of_majorant
reduced the hstrip binder of
Closure.GammaTenStripAssembly.fluctuationEnergyAverage_le_of_interior_cell_fold_grid_load
to two statements about the nonnegative crude elliptic majorant
maj_R = (Lam_R + 2 nu^{-1} Lam_R^2) . D_R + 2 nu^{-1} . F_R ,
namely its sample integrability at each cell and the bound
avsum_{R in 3^{n} Zd cap cu_{Kc}} ( E[ maj_R ] )^2 <= Cstrip .
Here D_R and F_R are the two named cell data of the majorant, defined
below: the Step-2 background's potential (resp. flux) cell energy plus the
squared length of the matching leg of the cell's principal load P_z. This
module discharges both statements from the second grid moments of D and
F alone, with the coefficient leg paid by the cell-uniform ellipticity moment
of Closure.GammaTenStripMoment.
The estimate, in one line #
Cauchy--Schwarz in the sample separates the coefficient from the cell datum:
E[ maj_R ] <= E[ W . D_R ] + 2 nu^{-1} E[ F_R ]
<= sqrt(E[W^2]) sqrt(E[D_R^2]) + 2 nu^{-1} sqrt(E[F_R^2]) ,
W being the cell-uniform ellipticity weight of Closure.GammaTenStripMoment
(which dominates Lam_R + 2 nu^{-1} Lam_R^2 at every cell of the mesh at
once), and then (x+y)^2 <= 2x^2 + 2y^2 and the grid average give
Cstrip = 2 . stripLambdaMoment M (n+h) (cu_{Kc}) . Cpot + 8 nu^{-2} . Cflux .
Nothing else enters: no Besov envelope, no minimizer, no interior restriction, no oscillation cell, no gauge and no smallness gate.
What is proved #
stripCellPotentialDatum,stripCellFluxDatum, their nonnegativity, andstripCellMajorant_eq_data--- the majorant read at the two data (definitional).stripCellMajorant_le_weight_mul_data--- the cell-uniform pointwise majorization, conditional only on the geometric containment of the cell in the localization cube.integrable_stripCellMajorant_of_data_sq--- the sample integrability of the majorant at one cell, from the two cell data's second moments. No measurability of the corrector data is assumed: both data inherit their a.e.-strong measurability from their own square's integrability.cubeFamilyAverage_sq_integral_stripCellMajorant_le--- the grid bound at the majorant.gammaTenStripConstandgammaTenStrip_cell_average_sq_le--- thehstripbinder itself, in the exact shapeClosure.GammaTenStripAssembly.fluctuationEnergyAverage_le_of_interior_cell_fold_grid_loadconsumes, at the explicit constant above.
Binders, and what is left #
gammaTenStrip_cell_average_sq_le is on exactly four hypotheses, all of them
moment statements about the two cell data of the majorant on the full mesh:
hDsq,hFsq--- per cell, the sample integrability ofD_R^2,F_R^2;hpot,hflux--- the grid averages of those second moments, belowCpotandCflux.
Nothing else is assumed: no smallness gate, no induction state, no Besov datum, no measurable selection and no interior-mesh restriction occurs, and neither the integrability nor the measurability of the Step-2 cell integrand itself is used.
The two grid binders are not discharged here. Their intended route is the
exact tiling identity
LocalizationGrid.cubeAverage_originCube_eq_mesoGridAverage composed with the
per-cell Jensen step and the annealed fourth energy of e.nablaw.in.L.eight
(LocalizationEnvelopeSpatial.originCubeFourthEnergy_le_sq_of_cubeEuclideanLpNorm_sq_le
together with LocalizationEnvelopeMoment's Gamma_1 second moment); none of
that is invoked below and no declaration here asserts it.
The size of Cstrip #
stripLambdaMoment M (n+h) (cu_{Kc}) is the second sample moment of the
ellipticity weight at the canonical origin cover of the localization cube,
and therefore depends on Kc: see the scale discussion in
Closure.GammaTenStripMoment. No Kc-independence is claimed here, and the
consumer's absorption gate hgate is stated at whatever Cstrip it is given.
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.lower.bound.localization.terms,e.Pz.def,e.Fz.def,e.CG.bounds.2.
Two Cauchy--Schwarz steps in the sample #
Two integrability transfers #
The two cell data of the crude elliptic majorant #
The potential datum of the cell: the Step-2 background's normalized
potential cell energy plus the squared length of the potential leg of the cell's
principal load P_z. It is the factor the ellipticity constant multiplies in
Closure.GammaTenStripCell.stripCellMajorant.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The flux datum of the cell, the flux mirror of stripCellPotentialDatum.
It carries only the deterministic factor 2 nu^{-1}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The crude elliptic majorant, read at the two cell data. Definitional.
The cell-uniform majorization #
The majorant is below the cell-uniform ellipticity weight times the potential datum, plus the flux datum.
The only cell-dependent factor of the coefficient leg is replaced by the
envelope of Closure.GammaTenStripMoment, which is uniform over every cube
inside the localization cube.
only on the geometric containment hsub.
The sample integrability of the majorant at one cell #
The hint binder of
cubeFamilyAverage_sq_integral_meshFluctuationCellIntegrand_le_of_majorant,
at one cell.
on the geometric containment hsub and on the second sample moments hDsq,
hFsq of the two cell data. No measurability of the corrector data is
assumed: each datum is the square root of its own square, hence a.e.-strongly
measurable as soon as that square is integrable.
The grid bound at the majorant #
The grid average of the squared cell expectations of the majorant.
on the two per-cell second moments hDsq, hFsq and on their two grid
averages hpot, hflux. The coefficient leg is paid once, by the
cell-uniform Closure.GammaTenStripMoment.stripLambdaMoment.
hstrip #
The strip constant. 2. (second moment of the cell-uniform ellipticity weight). Cpot + 8 nu^{-2}. Cflux. Its only inputs are the model's uniform
lower ellipticity nu, the ellipticity moment of the localization cube and the
two grid second moments of the cell data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
hstrip. The full-mesh average of the squared cell expectations of the
Step-2 cell integrand is below gammaTenStripConst.
This is the exact shape of the hstrip binder of
Closure.GammaTenStripAssembly.fluctuationEnergyAverage_le_of_interior_cell_fold_grid_load.
on exactly the four moment binders hDsq, hFsq, hpot, hflux of
cubeFamilyAverage_sq_integral_stripCellMajorant_le: the sign of the cell
integrand is removed by Closure.GammaTenStripCell, and no Besov envelope, no
minimizer, no measurable selection and no interior restriction enters.