PerCubeFirstThird #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 5's per-cube moments: the first and third summands #
What this module does #
Step 5 of l.bounds.mathcal.E.aL says that "the p-th root of the sum over j ≤ n of the p/2-th moment of the first and third terms appearing on the right side of
e.apply.sensitivity.J.aL is indeed bounded by the right side of
e.bounds.mathcal.E.aL", and treats the second and fourth terms separately,
"with additional inputs".
first : R = 4C · ( 1 + R_{B6a}(4q) R_{B5}(4q) ) · R_{B4}(4q)²
third : R = C · ( σ_m^{-1} + R_{B5}(4q) )² · R_{B6a}(4q)²
Both are exactly the anchor's scalar shape once the proved bullets are read:
R_{B4}(4q)² is O(q s^{-2} γ) (the printed C s^{-1}q^{1/2}γ^{1/2} squared,
which is the s^{-1}√p√γ of the anchor), and in the third term (σ_m^{-1} + R_{B5}) · R_{B6a} is O(√q √γ) by (B3) at both indices
(SigmaBarLandmark.exists_rpow_gamma_mul_inv_sigmaBar_sub_one_le), so its
square is O(q γ). N summand carries a 3^{γ(m−j)} factor: they are uniform
in the descendant scale, which is why Step 5 calls them straightforward.
The engines are the proved ones:
MomentHolder.lintegral_rpow_mul_le_of_moments for the two-factor Hölder,
PerCubeBracket for the (1+∇k·λ^{-1})^θ bracket, and ℝ≥0∞ Minkowski
against a constant for the σ_m^{-1} + λ^{-1} slot.
What is NOT here #
The S summand. It is the one the manuscript handles with the additional
j-geometric sum, and it is NOT uniform in the descendant scale.
1. The three summands of Step 3's display, named #
The summand of MajorantSlots.step3DisplayAt: the (2,2) homogenization error
leg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The S summand of MajorantSlots.step3DisplayAt: the λ^{-1}-weighted
value/ratio leg. Named here for the decomposition only; NO moment bound for it
is asserted on this tree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third summand of MajorantSlots.step3DisplayAt: the pure gradient leg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2. Two abstract moment steps #
The square of an observable, in the normal form. If X obeys the
development normal form at 2r, then X² obeys it at r with the majorant
R_X². This is the step that converts the printed (2,2)-error and gradient
bullets (stated for the object itself) into the display's squared slots.
Minkowski against a deterministic shift, in the normal form. If Y obeys
the development normal form at r ≥ 1, so does b + Y for every constant b ≥ 0, with the majorant b + R_Y. This is the σ_m^{-1} + λ^{-1} slot of the
display's third summand.
A deterministically scaled two-factor product, in the normal form.
The shape both of Step 3's first summand (4C · bracket · 𝓔²) and of its third
(C · (σ_m^{-1}+λ^{-1})² · ∇k²): a nonnegative observable dominated pointwise
by b · (A · B) with A, B in the normal form at the doubled exponent.
3. The three Step-4 majorants, named #
The (B5) majorant at exponent p, at the λ-slot Step 3 reads
(LambdaSlotConsumer).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The (B6a) majorant at exponent p (StepFourMoments).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The (B4) majorant at exponent p (StepFourMoments), the two-lane
(Γ₂, Γ_{1/2}) bound of the (2,2) homogenization error.
Equations
- One or more equations did not get rendered due to their size.
Instances For
4. The third summand #
The third summand's q-th moment.
∫⁻ ( C ((σ_m^{-1} + λ^{-1}) · 3^{2j}‖∇(k_L−k_{j−2})‖)² )^q
≤ ( ofReal ( C (σ_m^{-1} + R_{B5}(4q))² R_{B6a}(4q)² ) )^q .
Both factors enter at the exponent 4q — the two-factor Hölder doubling
applied to two squares — and the majorant is uniform in the descendant scale j = R.scale once (B3) is applied at both σ indices: σ_m^{-1}·R_{B6a} and
R_{B5}·R_{B6a} are both O(√q √γ), so the whole term is O(q γ), which the
anchor's (√p (s^{-1}+√(m−n)) √γ)² dominates. This is one of the two summands
Step 5 calls straightforward.
5. The first summand #
The first summand's q-th moment.
∫⁻ ( C σ_m^{-1}σ_{j−2} (1 + ∇k·λ^{-1})^{2s/(1−4γ)} 𝓔_{s,2,2}² )^q
≤ ( ofReal ( 4C · R_bracket · R_{B4}² ) )^q .
The three inputs are the three proved Step-4 items, and they enter at the
exponents the two-factor Hölder doubling produces: the deterministic ratio
bullet (B1) at 4 (StepFourSigmaBar), the bracket at 2q
(PerCubeBracket.exists_lintegral_rpow_step3Bracket_le, which itself reads
(B6a) and (B5) at 4q), and the (2,2) error at 4q
(StepFourMoments.exists_lintegral_rpow_unitCubeHomogenizationError22_le).
The three moment inputs are conditional API obligations, carried as hypotheses rather than instantiated, so that each proved bullet keeps its own constant: no constant is enlarged and no regime is merged here.
Because R_{B4}(4q) is the printed C s^{-1}q^{1/2}γ^{1/2} + Cq² e^{-C^{-1}γ^{-1}} and R_bracket = 1 + O(√q√γ)
(PerCubeBracket.step3Bracket_majorant_le), this majorant is O(q s^{-2} γ)
uniformly in the descendant scale — the anchor's own (√p s^{-1} √γ)².