MomentEngine #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The one-term Γ_σ-tail → q-th-moment conversion, in the anchor's normal form #
Nothing here imports that file, and nothing here claims the anchor.
The target #
Step 4 of the proof of l.bounds.mathcal.E.aL lists seven bullets and converts
four of them into moment bounds with the sentence "and hence, for every q ∈ [1,∞)", citing l.moments.gamma.psi (E[|X|^q]^{1/q} ≤ C q^{1/σ} K). Three
of the four are ONE-term displays:
𝓔_{s,2,2} (two-term; handled by `MomentSplitter`)
3^{2j}‖∇(k_L−k_{j−2})‖_{W^{1,∞}(□_j)} ≤ 𝒪_{Γ₂}(C 3^{γ j})
‖k_L − k_{j−2} − (k_L−k_m)_{□_m}‖_{L²(□_j)} ≤ 𝒪_{Γ₂}(C min{γ^{−1/2},(m−j)^{1/2}} 3^{γ m})
λ_{γ,2}^{-1}(□_j;𝐚_{j−2}) ≤ C σ_{j−1}^{-1} + 𝒪_{Γ_{1/3}}(…)
and the remaining three bullets are D scalar inequalities, whose q-th moment
is the scalar itself (a probability measure has total mass one).
Main results #
lintegral_rpow_le_of_ae_le_const— the deterministic bullets: anℝ≥0∞-valued observable a.e. bounded by a constant has all itsq-th moments bounded by that constant.lintegral_rpow_le_of_isBigOWith_of_ae_le— the one-term engine at generalσ: an observable a.e. dominated byENNReal.ofReal ∘ XwithX ≤ 𝒪_{Γ_σ}(A)obeys∫⁻ F^q ≤ (.ofReal R)^qfor every real majorantRofC(σ) q^{1/σ} A.lintegral_rpow_le_of_isBigOWith_gammaTwo,lintegral_ofReal_rpow_le_of_isBigOWith_gammaTwo— theσ = 2instance, withq^{1/σ}evaluated toReal.sqrt q(the√qof the printed bullets, and the anchor's own√p).lintegral_rpow_le_of_isBigOWith_add_const_of_ae_le— the shape of bullet (B5), whose display carries a D summand alongside theΓ_{1/3}one:∫⁻ F^q ≤ (.ofReal R)^qfor every real majorantRofb + C(σ) q^{1/σ} A, byℝ≥0∞Minkowski against the constant.gammaMomentBound,gammaTwoMomentBound— the majorants as named quantities, so a consumer can carry them symbolically.
Route, and what is reused rather than re-proved #
Nothing about it is re-derived here. What is added is exactly what the
anchor's normal form needs and that engine does not have: the ℝ≥0∞-observable
left-hand side (so the literal, only-a.e.-measurable Step-4 objects can be the
subject via an a.e. domination), the (.ofReal R) ^ q right-hand side with a
caller-supplied majorant, and the evaluation of q^{1/σ} at σ = 2. This is
the one-term twin of MomentSplitter, whose two-term statements have the same
shape and the same binders.
Binders #
Only the source binders: 1 ≤ q (the range q ∈ [1,∞) of
l.moments.gamma.psi), 0 < σ, positivity of the Orlicz scale (which the
two-term relation bundles and the one-term relation does not), nonnegativity
and a.e. measurability of the field, the display itself, the a.e. domination of
the observable, and the majorant inequality. IsProbabilityMeasure is the
ambient hypothesis of l.moments.gamma.psi.
References #
- ABK26,
l.moments.gamma.psi;l.bounds.mathcal.E.aL.
1. The one-term moment majorant #
The one-term moment majorant produced by l.moments.gamma.psi: C(σ) q^{1/σ} A. The constant is CoarseGraining's own gammaMomentConst, left in the
engine's normal form so that none is silently reshaped.
Equations
- Algsuperdiff.Section4.Provider.BoundsEaL.gammaMomentBound sigma p A = HCPolySupport.IndependentSums.gammaMomentConst sigma * p ^ sigma⁻¹ * A
Instances For
The σ = 2 moment majorant, with q^{1/2} spelled as Real.sqrt q — the
√q of the printed Step-4 bullets and the √p of the anchor's conclusion.
Equations
Instances For
2. The deterministic bullets #
3. The one-term Orlicz → moment splitter #
The one-term Γ_σ → lintegral moment conversion, in the normal form of
bounds_mathcal_E_aL.
If an ℝ≥0∞-valued observable F is almost surely dominated by ENNReal.ofReal (X ·)
for a nonnegative, a.e. measurable X carrying a display X ≤ 𝒪_{Γ_σ}(A), then for every
q ≥ 1 and every real R majorizing the engine's moment constant C(σ) q^{1/σ} A, ∫⁻ F^q ≤ (.ofReal R)^q.
4. The Γ₂ instance: the √q of the printed bullets #
The Γ₂ moment conversion. The q^{1/σ} of l.moments.gamma.psi at
σ = 2 is √q, which is the q^{1/2} printed in the two e.nabla.km.kn.infty
bullets of Step 4 and the √p of the anchor's conclusion.
The Γ₂ moment conversion with the observable taken to be ENNReal.ofReal ∘ X
itself.
5. The deterministic-shift shape: b + 𝒪_{Γ_σ}(A) #
The moment conversion of a deterministically shifted one-term display.
Bullet (B5) of Step 4 is the only bullet whose display has a D summand,
λ_{γ,2}^{-1}(□_j;𝐚_{j−2}) ≤ C σ_{j−1}^{-1} + 𝒪_{Γ_{1/3}}(C σ_{j−1}^{-1}exp(−C^{-1}γ^{-1})), and its printed moment conversion keeps the
two summands apart: E[λ^{-q}]^{1/q} ≤ C σ_{j−1}^{-1}(1 + C q³ exp(−C^{-1}γ^{-1})). The q³ is q^{1/σ} at σ = 1/3.
The proof is ℝ≥0∞ Minkowski against the constant, exactly as the manuscript's
l.moments.gamma.psi is applied to a sum.