GammaTenStripCell #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Step-2 cell integrand, bounded on both sides at every cell #
ABK26, Step 2 of l.approximate.recurrence.formula,
e.lower.bound.basic.split, e.CG.bounds.2.
What this module is #
Every proved bound on LocalizationFluctuationSelectEndpoint. meshFluctuationCellIntegrand --- Closure.GammaTenAssemblyCell. meshFluctuationCellIntegrand_le_of_besovEnvelope and its two fold shapes ---
is one-sided (an upper bound) and needs a pathwise Besov envelope Bg of
the gauged bfF_z on the cell. The envelope's moment carrier is the
interior mesh, which is why
Closure.GammaTenStripAssembly.fluctuationEnergyAverage_le_of_interior_cell_fold_grid_load
has to pay for the boundary strip, and its hstrip binder asks for a full-mesh
average of the squares of the cell expectations --- a quantity that needs a
bound of the integrand from below as well.
This module supplies the missing side. The bound below is not a refinement of
the Besov route; it is the crude elliptic one, and it needs no envelope, no
minimizer, no Besov exponent, no gauge and no cell-membership beyond the
geometric one that types the L^2 legs:
|fluct_R(omega)|
<= (Lam_R + 2 nu^{-1} Lam_R^2) ( Epot_R + |P_R^{pot}|^2 )
+ 2 nu^{-1} ( Eflux_R + |P_R^{flux}|^2 ) ,
Lam_R = Cutoff.coefficientCutoffCubeEllipticityUpper M (n+h) omega R being the
realized upper ellipticity constant of the cell's own cutoff coefficient, nu
the model's uniform lower one, and Epot_R, Eflux_R the two named cell
energies of Closure.SplitObligationsBackground.
Where each side comes from #
LocalizationFluctuationMuMeasCell.meshFluctuationCellIntegrand_eq is the
definitional identity
fluct_R = 2 mu_field( a_omega; P_z + bfF_z ) - switch_R(P_z) ,
and both summands are bracketed unconditionally:
0 <= mu_field <= mu(background)(LocalizationFluctuationMuMeasCore.doubledMuField_nonneg,doubledMuField_le_self) --- the field slope is its own competitor and every doubled energy density is a.e. nonnegative;0 <= switch_R(P_z) <= (Lam + 2 nu^{-1} Lam^2)|P^{pot}|^2 + 2 nu^{-1}|P^{flux}|^2(LocalizationFluctuationMuMeasCell.switchCubeEnergy_nonneg,Closure.SplitObligationsQuadratic.switchCubeEnergy_le_ellipticityUpper);mu(background)itself is below the plain elliptic upper bound of its carrier (Closure.SplitObligationsBackground.doubledMuValue_le_plainUpperBound), whose two averages are definitionally the two named cell energies.
The lower half of the integrand uses only the first item's left inequality and
the second item's right one; the upper half only the converse pair. Nothing is
assumed about the corrector data beyond the vector-L^2 typing of the two
background legs, which
LocalizationFluctuationBackgroundClass.memVectorL2_meshCellBackground_{potential,flux}
supplies from the cell's geometric membership alone.
What is proved #
stripCellMajorant--- the right-hand side above, as a named nonnegative sample function of the cell.stripCellMajorant_nonneg.abs_meshFluctuationCellIntegrand_le_stripCellMajorant--- the display, at every cell of the full meshdescendantsAtDepth (cu_{Kc}) jdand at every sample point.sq_integral_le_sq_integral_of_abs_le--- the measure-theoretic step that turns a two-sided pointwise bound into a bound on the square of the sample integral, with no integrability of the dominated function assumed: where it is integrable the twoabs_lehalves apply, and where it is not the Bochner integral is0while the majorant's is nonnegative.cubeFamilyAverage_sq_integral_meshFluctuationCellIntegrand_le_of_majorant--- the reduction ofhstrip: the full-mesh average of the squared cell expectations is below the same average read at the crude elliptic majorant. What is left ofClosure.GammaTenStripAssembly'shstripafter it is a statement about a nonnegative grid family --- no minimizer, no Besov datum, no interior restriction --- namely the sample integrability of the majorant at each cell together with
That residual is not proved here.cubeFamilyAverage (mesoCubeGrid d Kc (Kc - j)) (fun R => (int_omega stripCellMajorant ... R omega)^2) <= Cstrip .
Binders #
For the pointwise bound, the cell's geometric membership hR and nothing else:
no smallness gate, no Besov exponent, no gauge parameter, no measurability, no
integrability, no moment and no weak-solution property occurs, and the two
correctors enter only as the arguments of the carriers. The integral step adds
the integrability and nonnegativity of the majorant alone.
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.
The crude elliptic majorant of the cell #
The crude elliptic majorant of the Step-2 cell integrand.
(Lam_R + 2 nu^{-1} Lam_R^2) ( Epot_R + |P_R^{pot}|^2 )
+ 2 nu^{-1} ( Eflux_R + |P_R^{flux}|^2 ) ,
with Lam_R the realized upper ellipticity constant of the cell's cutoff
coefficient, nu the model's uniform lower one, Epot_R, Eflux_R the two
named cell energies of the Step-2 background and P_R the cell's principal
load. It mentions no Besov datum and no minimizer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The crude elliptic majorant is nonnegative. Unconditional.
The two-sided cell bound #
The Step-2 cell integrand is bounded in absolute value by the crude elliptic majorant, at every cell of the full mesh and at every sample point.
|fluct_R(omega)| <= stripCellMajorant M n h Kc e e' wD wN R omega .
The upper half drops the switch energy by its nonnegativity and bounds the field-slope minimum by the energy of its own slope field; the lower half drops the field-slope minimum by its nonnegativity and bounds the switch energy by the plain elliptic upper bound of the cell's coefficient. Neither half mentions a Besov envelope, so neither is restricted to the interior mesh.
only on the cell's geometric membership hR, which is used solely to type the
two background legs as vector-L^2 on the cell.
From the pointwise bound to the square of the sample integral #
The square of the integral of a two-sidedly dominated function.
If |f| <= g almost surely with g nonnegative and integrable, then
(int f)^2 <= (int g)^2. No integrability of f is assumed: where f is
integrable the bound is abs_integral_le_integral_abs followed by
integral_mono_ae, and where it is not the Bochner integral of f is 0,
whose absolute value is below the nonnegative integral of g.
only on hg, hg0 and hfg.
hstrip, reduced to a nonnegative-majorant grid average #
The hstrip binder of Closure.GammaTenStripAssembly, reduced.
The left-hand side of
cubeFamilyAverage (mesoCubeGrid d Kc (Kc - j))
(fun R => (int_omega fluct_R)^2) <= Cstrip
is below the same average taken at the crude elliptic majorant instead of the
cell integrand. The passage from the one to the other is the only place where
the sign of the integrand matters, and it is exactly what
abs_meshFluctuationCellIntegrand_le_stripCellMajorant removes: after it, the
residual is a statement about a nonnegative grid family, with no minimizer,
no Besov datum and no interior restriction left in it.
on the sample integrability of the majorant at each cell of the mesh and on the
majorant's own grid average hmaj. Neither the integrability nor the
measurability of the cell integrand itself is assumed.