HomStepOneMoment #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Theorem B, §4.5, Step 1: the Hölder assembly of the EthmB(m) moment #
The target #
Step 1 ends with the sentence
"Combining this estimate with the
bounds_mathcal_E_aLlemma, using Hölder's inequality ands = |log γ|⁻¹, we obtain the moment bound announced in the𝓔estimate."
It is recorded that the Hölder bookkeeping is asserted, not displayed. This
module reconstructs it in full. EthmB(m) is the sum of two products
T₁ = s⁻¹ · Y · ( 𝓔_{s₁} · (1 + 𝓔_{1/4}) ), T₂ = C γ⁵ · ( 1 + 𝓔²_{s₁/2} ),
so the exponent boosts are 2 on the outer product, 4 on the inner one and
2 on the square — NOT the uniform 3 a naive three-factor Hölder would ask
for. The assembly is therefore:
| object | exponent at which it is consumed |
|---|---|
Y = 3^{(1-α)X_m(α)} | 2p |
𝓔_{s₁,∞,2}(□_m, n; ·) | 4p |
𝓔_{1/4,∞,2}(□_m; ·) | 4p |
𝓔_{s₁/2,∞,2}(□_m, n; ·) | 2p |
The conditional edge (the ONE in this lane) #
Y and its moment are the only inputs this module does not produce. Y is
the minimal-scale factor 3^{(1-α) X_m(α)} and its moment bound
𝔼[ (3^{(1-α)X_m(α)})^{2p} ] ≤ 2^{2p}
is the Markov/Γ₁ step of Step 1, whose input is clause (a) of Theorem C
(X_m(α) = 𝒪_{Γ₁}(C γ (1-α)^{-2})). Per the conditional-edge device it enters
here as a NAMED TRANSCRIBED HYPOTHESIS (hY), at the single exponent 2p at
which it is consumed — never by importing Theorem C itself. Theorem C is a
declared dependency of this step, so this is a node-internal edge, not a side
assumption. NOTE for the consumer: the printed range of the Markov step is p ≤ C⁻¹(1-α)γ⁻¹ with 1 - α = s/2; the caller must respect it when discharging
hY.
The output shape #
The assembled majorant is left FACTORED,
s⁻¹ · ( R_Y · ( R₁ · (1 + R₂) ) ) + C γ⁵ · ( 1 + R₃² ),
with R_Y, R₁, R₂, R₃ the caller's own factor majorants (R_Y = 2 at the
plain Theorem-C edge; the enlarged-Y re-pin passes the
𝓔-boosted majorant instead — the interface generalization). This is the honest
output of Hölder: not one power of γ, of s, or of |log γ| has been moved
or absorbed ( forbids silent absorption of s-powers, since
s = s(γ) is not a constant). The numeric collapse to the printed display
C(√p + √|log γ|)√γ |log γ|² is a separate, separately auditable step.
1. Two generic ℝ≥0∞ moment tools #
Exponent monotonicity (Lyapunov) in the normal form.
On a probability space the normal form at a LARGER exponent implies it at a
smaller one, with the SAME majorant. This is what lets the Step-1 assembly
consume the anchor at the boosted exponent q = max(4p, 2d s'⁻¹) and still
read the result at 4p:'s threshold q ≥ 2 d s'⁻¹ is respected without
weakening the conclusion.
The two-term Minkowski step, in the normal form.
The constant observable 1 sits in the normal form with majorant 1.
2. The assembly #
STEP 1's HÖLDER ASSEMBLY.
Given the four factor moments — the minimal-scale factor Y at exponent
2p with majorant R_Y and the three 𝓔-factors at 4p, 4p, 2p — the
defect EthmB(m) obeys this development normal form at p with the factored
majorant
s⁻¹ · ( R_Y · ( R₁ · (1 + R₂) ) ) + C γ⁵ · ( 1 + R₃² ).
Nothing is absorbed: this is the source's "using Hölder's inequality" written out.