SecondTermMoment

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Step 5's second summand: its q-th moment, by the four-factor Hölder

What this module does

The second summand of PerCubeFirstThird.step3SecondTerm is

C σ_m^{-1} σ_{j−2}²  ·  λ_{2γ,2}^{-1}  ·  (1 + ∇k λ^{-1})^{4γ/(1−4γ)}
      ·  ( σ_{j−2}^{-2} ‖h‖² + (σ_m σ_{j−2}^{-1} − 1)² ) ,

the one Step 5 handles "with additional inputs". This module supplies its q-th moment in the development normal form.

The route is a S followed by two Hölder products. Because σ_{j−2}² σ_{j−2}^{-2} = 1, the summand is

  C σ_m^{-1} · ( λ^{-1} · ( bracket · ‖h‖² ) )                       (the value leg)
+ C σ_m^{-1} σ_{j−2}² (σ_m σ_{j−2}^{-1} − 1)² · ( λ^{-1} · bracket ) (the (B2) leg)

-- no inequality is spent on the split. The (B2) leg is a TWO-factor product with a deterministic scalar in front, so it reads (B5) and the bracket at 2q only; its scalar is bullet (B2), which is deterministic and therefore costs no moment at all.

Every Step-4 bullet is available at every moment q ∈ [1,∞) -- that is exactly what Step 4's "hence, for every q" sentences deliver -- so the exponent boost is free, and NO constant beyond the product of the caller's own majorants appears.

References

• ABK26, l.bounds.mathcal.E.aL, e.apply.sensitivity.J.aL, Step 4 bullets (B2)/(B5)/(B6a)/(B6b), Step 5.

1. The two named majorants

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.bracketMajorant (d : ℕ) (M : Section3.ABKModel d) (EB : ℝ) (j : ℤ) (r : ℝ) : ℝ

The bracket majorant of PerCubeBracket.exists_lintegral_rpow_step3Bracket_le at moment r, named: 1 + R_{B6a}(2r) R_{B5}(2r).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.bracketMajorant_nonneg (d : ℕ) (M : Section3.ABKModel d) (EB : ℝ) (j : ℤ) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ bracketMajorant d M EB j r

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.secondTermMajorant (d : ℕ) (M : Section3.ABKModel d) (E EB Cd : ℝ) (m j : ℤ) (q : ℝ) : ℝ

The second summand's majorant at moment q, at the two proved budgets E (the λ-slot bullet) and E_B (the bracket).

Equations

• One or more equations did not get rendered due to their size.

2. The abstract four-factor Hölder core

3. The second summand's moment at the Step-3 slots

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_lintegral_rpow_step3SecondTerm_le (d : ℕ) : ∃ (CL : ℝ) (CB : ℝ), 6 ≤ CL ∧ 6 ≤ CB ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ (max CL CB)⁻¹ ^ 10 * Section3.Disorder.cstar M ^ 10 → M.gamma ≤ 1 / 8 → ∀ (Cd : ℝ), 0 ≤ Cd → ∀ (m : ℤ) (R : HCPolySupport.TriadicCube d), R.scale ≤ m → ∀ (q : ℝ), 1 ≤ q → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (step3SecondTerm Cd M m R omega (lFreeGradSlot m (tailSeriesGauge m) R omega) (lFreeValueSlot m (tailSeriesGauge m) R omega)) ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (secondTermMajorant d M (CL * (Section3.Disorder.cstar M)⁻¹) (CB * (Section3.Disorder.cstar M)⁻¹) Cd m R.scale q) ^ q

The second summand's q-th moment.

∫⁻ ( step3SecondTerm )^q ≤ ( ofReal ( secondTermMajorant ) )^q ,

the four-factor Hölder of the module docstring at the proved Step-4 bullets. Both budgets are of the printed shape C c⋆^{-1}; the standing regime is taken at the maximum of the two proved constants.