G2Moments #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 3 of the 𝒢₂ lane: the X_j moment bound and E[X_j^p] ≤ 1 #
ABK26, §4.1, e.Xj.moment.bound:
E[X_j^p]^{1/p} ≤ C K₂ c⋆^{−2} s^{−4} ε^{−2} γ p + C K₂ s^{−5} ε^{−2} exp(−C^{−1}c⋆³γ^{−1}) p⁴ ,
the two summands being the images of the two Orlicz lanes of
e.Xj.Orlicz.bound under e.moments.OGamma2 (E[|X|^p]^{1/p} ≤ Cp^{1/σ}K) at
σ = 1 (giving the linear p) and σ = 1/4 (giving p⁴); and then, at the
parameter choices e.K.and.p.choices, E[X_j^p] ≤ 1.
Why the two lanes may not be merged #
A Γ_σ tail implies a Γ_{σ'} tail at the same scale for σ' ≤ σ, so the
two-term display could be collapsed to a single Γ_{1/4} display. That
collapse is fatal here: it replaces the linear p of the first term by p⁴,
and the manuscript's own verification of the first term — C K₂ c⋆^{−2}s^{−4} ε^{−2}γ·p =₂ K₁^{−1} ≤ 1/2 — depends on the exponent being exactly 1. This
is why the pair is never merged in the manuscript: no single
σ dominates both lanes. The engine below therefore takes a genuine
two-term display and applies the ambient moment engine separately to each
witness, joining them with ℝ≥0∞ Minkowski.
The E[X_j^p] ≤ 1 verification, faithfully #
closes Step 3 with two numerical claims — "the first term equals CK₂K₁^{−1} ≤ 1/2
for K₂K₁^{−1} small" and "the second is ≤ 1/2 for K₀ large enough". Both
are conditions on the proof-internal constants K₀,K₁,K₂ of
e.K.and.p.choices, which the lemma's proof is free to choose. They are
carried here as the single explicit hypothesis hnorm
gammaMomentConst 1 · p · (Γ_1-scale) + gammaMomentConst (1/4) · p⁴ · (Γ_{1/4}-scale) ≤ D ,
which is exactly the manuscript's sentence with the two halves added instead of
being bounded by 1/2 each. No hypothesis is added that the manuscript does not
make, and no proof step migrates into a hypothesis: hnorm IS the manuscript's
constant-selection step.
Scope #
Provider material: proved local helpers. hcube (the per-cube two-term
display, see G2AtomTail) and hnorm are conditional A obligations.
References #
- ABK26,
l.ratio.of.good.scales.for.mathcal.E.
1. Generic: scaling and the two-term moment engine #
Scaling of a two-term weak-Orlicz display.
e.moments.OGamma2 at a two-term display (the Step-3 engine).
For a nonnegative X with X ≤ 𝒪_{Γ_{σ₁}}(A₁) + 𝒪_{Γ_{σ₂}}(A₂) and p ≥ 1,
E[X^p]^{1/p} ≤ C(σ₁) p^{1/σ₁} A₁ + C(σ₂) p^{1/σ₂} A₂ .
The proof applies the ambient one-term moment engine to each clamped witness and
joins the two with ℝ≥0∞ Minkowski; the statement is in the raised
∫⁻ ≤ (…)^p form the ambient engine and the Appendix-D interface both use.
The Appendix-D unit moment from a two-term display. The normalized atom
D^{-1}X has ∫⁻ (D^{-1}X)^p ≤ 1 as soon as the two moment terms add up to at
most D. This is the hmomL slot of the concentration interface, at the 𝒢₂
lane's genuinely two-term display.
2. The 𝒢₂ lane #
The Γ_1-lane Orlicz scale of X_j produced by Step 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Γ_{1/4}-lane Orlicz scale of X_j produced by Step 2; the
manuscript's CK₂s^{−5}ε^{−2}exp(−C^{−1}c⋆³γ^{−1}).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Step 2 in the packaged scale notation.
The 𝒢₂ Appendix-D array, X_{k,j} = D^{-1}X_j. The normalizer D
carries the manuscript's K₂ε^{−2}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Step 3's conclusion E[X_j^p] ≤ 1, in the ∫⁻ reading, for the whole
Appendix-D array.
hnorm is the manuscript's own constant-selection sentence — "for K₂K₁^{−1}
small" and "for K₀ large enough" — with the two halves added rather than
bounded by 1/2 each. hcube is the per-cube conditional A obligation of
G2AtomTail.