GammaTenStripMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
A cell-uniform envelope for the realized upper ellipticity constant #
ABK26, Step 2 of l.approximate.recurrence.formula, e.CG.bounds.2.
The gap this module fills #
Lam_R(omega) = Cutoff.coefficientCutoffCubeEllipticityUpper M m omega R
at a fixed cube R, but its majorant carries the local control
cutoffLocalControl (cubeOriginCoverScale R) m omega, whose scale is the
canonical origin cover of R and therefore moves with R. A grid estimate
over a mesh of cells needs one envelope valid at every cell of the mesh at
once.
That envelope is supplied here. It is not a transport: Lam_R depends on the
cell only through the integer cubeOriginCoverScale R, so there is nothing to
translate --- the mesh-uniform reading is obtained by monotonicity in the
cover scale, which is the honest cost of the crude elliptic bound and is
recorded as such below.
What is proved #
localCubeControl_mono,cutoffLocalControl_mono--- the deterministic local control and its lower-tail series are monotone in the cube scale: a larger origin cube can only have a larger sup.cubeOriginCoverScale_mono--- the canonical origin cover is monotone under inclusion of open cubes. This is minimality ofNat.find, not geometry.stripEllipticityEnvelope---Kmaj (1 + u_{cover Q})^2at the cover scale of the enclosing cubeQ, andcoefficientCutoffCubeEllipticityUpper_le_stripEllipticityEnvelope, the envelope property at every cubeRwithopenCubeSet R subset openCubeSet Q.stripEllipticityWeight--- the combinationLam + 2 nu^{-1} Lam^2in which the Step-2 majorant reads the ellipticity constant, at the envelope;ellipticityUpper_weight_le_stripEllipticityWeightis its envelope property.integrable_sq_stripEllipticityWeightandstripLambdaMoment--- the second moment of the weight, i.e. the fourth moment of the envelope, as a finite explicit number. Its finiteness is the binomial expansion of(1+u)^{2k}againstCutoff.P4UpperMoments.integrable_one_add_cutoffLocalControl_pow.
The scale of the envelope, stated plainly #
stripLambdaMoment M m Q is a number attached to the enclosing cube Q.
When Q = cu_{Kc} is the localization cube, that number depends on Kc: the
local control at scale cubeOriginCoverScale (originCube d Kc) is a supremum of
the shell field over a cube of side ~3^{Kc}, and the lower-tail law makes its
moments grow with the scale. No claim of Kc-independence is made anywhere
below, and none is used.
Binders #
stripEllipticityEnvelope's envelope property is conditional on the single
geometric containment openCubeSet R subset openCubeSet Q and on nothing else:
no smallness, no measurability, no moment and no model gate occurs. The moment
statements are unconditional.
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.CG.bounds.2.
Monotonicity of the deterministic local control #
The local control is monotone in the cube scale. Unconditional.
The lower-tail local-control series is monotone in the cube scale. Unconditional; both series are summable on the public cutoff carrier.
Monotonicity of the canonical origin cover #
The canonical origin cover scale is monotone under inclusion of open cubes. This is minimality of the cover depth, not geometry: the enclosing cube's own cover already covers the closure of the smaller open cube.
only on hsub.
The cell-uniform envelope #
The cell-uniform envelope of the realized upper ellipticity constant.
Kmaj (1 + u_{cover Q})^2, with Kmaj = Cutoff.cutoffUpperEllipticityMajorant M the
dimensional constant of Cutoff.P4UpperMoments and u_{cover Q} the lower-tail local
control read at the canonical origin cover of the enclosing cube Q. It does not
mention the cell.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The envelope property. At every cube whose open cube sits inside the enclosing cube's open cube, the realized upper ellipticity constant is below the envelope of the enclosing cube.
only on the geometric containment hsub.
The weight in which the Step-2 majorant reads the constant #
The Step-2 ellipticity weight at the envelope: E + 2 nu^{-1} E^2, the
combination in which Closure.GammaTenStripCell.stripCellMajorant multiplies the
potential cell energy.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The envelope property of the weight. Monotonicity of
t |-> t + 2 nu^{-1} t^2 on the nonnegative half line.
only on the geometric containment hsub.
The envelope is a measurable function of the sample: it is a polynomial in the measurable local control. Unconditional.
The weight is a measurable function of the sample. Unconditional.
The second moment of the weight #
The weight has a finite second moment. Expanding the square, the integrand
is a fixed nonnegative combination of (1 + u)^4, (1 + u)^6 and (1 + u)^8,
each integrable by Cutoff.P4UpperMoments.integrable_one_add_cutoffLocalControl_pow.
Unconditional.
The mesh-uniform ellipticity moment, as an explicit finite number: the
second sample moment of the Step-2 ellipticity weight at the envelope of the
enclosing cube. It is the only place where the crude elliptic bound pays for
the coefficient, and it is attached to Q, not to a cell.
Equations
- One or more equations did not get rendered due to their size.