PerCubeBracket #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Step 5's (1 + ∇k · λ^{-1}) bracket, at every moment #
What this module does #
Two of the three summands of MajorantSlots.step3DisplayAt carry the bracket
( 1 + 3^{2j}‖∇(k_L − k_{j−2})‖_{W^{1,∞}(□_j)} · λ_{2γ,2}^{-1} )^{θ} ,
at the two printed exponents θ = 2s/(1−4γ) and θ = 4γ/(1−4γ) (the
development's gapped-gauge reading of the printed 2s/(1−2γ), 2γ/(1−2γ);
Step3HSlot's deviation, inherited). This module supplies its q-th
moment, for every q ∈ [1,∞), in the development normal form ∫⁻ (·)^q ≤ (ofReal R)^q.
- both exponents are
≤ 1in the anchor's own ranges (s ≤ 1/4,γ ≤ 1/8), sox^θ ≤ xfor the basex = 1 + ∇k·λ^{-1} ≥ 1; NO Orlicz input and noq-power is spent on the exponent;
step3Bracket_majorant_le then evaluates the product majorant: the whole
q-th-moment bound is
1 + C(2)√(2q) · fullGradConst M · (3^{γ j} σ_{j−1}^{-1})
· ( λUp·C_cg + C(1/3)(2q)³ · λUp·λMax · cgTailScale ) ,
and the middle factor is O(√γ) by bullet (B3) together with the σ index
reconciliation of SigmaBarLandmark, which is exactly the statement that the
bracket is 1 + O(√q √γ) in the printed regime.
1. The abstract bracket moment #
The bracket moment, over an abstract probability space.
If two nonnegative observables satisfy the development normal form at the
doubled exponent 2q, then for every θ ≤ 1 the bracket (1 + X·Y)^θ satisfies it at
q, with the majorant 1 + R_X R_Y.
The θ ≤ 1 step is x^θ ≤ x for x ≥ 1: no moment input is spent on the
exponent. The product step is the two-factor Hölder engine and the additive 1
is ℝ≥0∞ Minkowski against a constant, which a probability measure integrates
to 1.
2. Both printed exponents are at most one #
The gradient bracket's exponent. 2s/(1−4γ) ≤ 1 in the anchor's own
ranges s ≤ 1/4, γ ≤ 1/8. This is the exact endpoint: at s = 1/4 and
γ = 0 the exponent IS 1.
3. The two slots are nonnegative #
The L-free gradient slot is nonnegative at the canonical tail gauge.
The λ-slot of Step 3's display is nonnegative.
The λ-slot of Step 3's display is measurable: the gapped gauge 2γ is
positive, which is all MajorantMeasurability's literal-measurability engine
needs.
4. The bracket at the Step-3 slots #
Step 5's bracket, at every moment.
For every q ∈ [1,∞) and every exponent θ ≤ 1 — in particular the two
printed exponents 2s/(1−4γ) and 4γ/(1−4γ), by
step3_gradient_exponent_le_one and step3_gamma_exponent_le_one — the
bracket of MajorantSlots.step3DisplayAt obeys the development normal form
with the majorant 1 + R_{B6a}(2q) · R_{B5}(2q), the product of the two proved
Step-4 majorants at the doubled exponent.
The binders are the printed regime (bullet (B5)'s own), the range R.scale ≤ m
of the gradient bullet, and 1 ≤ q. No γ-power and no s-power is moved.