PerCubeSlotSecond

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

Step 5's second summand, evaluated at the anchor's scalar

What this module does

SecondTermMoment.exists_lintegral_rpow_step3SecondTerm_le supplies the second summand's q-th moment at a symbolic majorant with two legs. This module evaluates both against the anchor's own linear and flat per-scale slots K p γ(m−j) 3^{2γ(m−j)} and K p γ 3^{2γ(m−j)}:

• the value leg is σ_m^{-1} · R_{B5}(2q) · R_bracket(4q) · R_{B6b}(8q)². The two σ-gauges contribute 3^{−γm} and 3^{−γj}, each with a √γ, and the squared value slot contributes 3^{2γm} and q(1+(m−j)); the three weights combine to the per-scale 3^{γ(m−j)} of Step 5's geometric sum (SecondTermArithmetic.rpow_three_gauge_triple), and the two √γ to the anchor's γ.
• the (B2) leg is deterministic apart from R_{B5}(2q) R_bracket(2q), and its scalar σ_m^{-1}σ_{j−2}²(σ_mσ_{j−2}^{-1}−1)² is bullet (B1) twice against bullet (B2). (B2)'s squared minimum splits into the same two slots by SecondTermArithmetic.min_one_add_sq_le, and its γ^{3/5}|log γ|² portion is O(√γ) only A squaring -- which is what SecondTermArithmetic.gammaLogPortion_sq_le supplies.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4 bullets (B1)/(B2)/(B5)/(B6b), Step 5 (in particular the j-sum).

1. A four-factor product step

2. Bullet (B2)'s squared minimum, split into the two slots

theorem Algsuperdiff.Section4.Provider.BoundsEaL.sigmaBarContinuity_min_sq_le {g t : ℝ} (hg0 : 0 < g) (hg1 : g ≤ 1) (ht : 0 ≤ t) : min 1 (g * (t + 2) + g ^ (3 / 5) * |Real.log g| ^ 2) ^ 2 ≤ 320004 * (g * t + g)

Bullet (B2)'s squared minimum, split.

(min{1, γ(t+2) + γ^{3/5}|log γ|²})² ≤ 320004 (γt + γ): the linear and flat per-scale shapes, at both branches of the minimum at once. The 320000 is 2·400², the square of the scale-free log bound γ^{1/10}(log γ)² ≤ 400.

3. The two leg constants

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.secondValueLegBound (d : ℕ) (cst EL EB : ℝ) : ℝ

The constant of the second summand's VALUE leg.

Equations

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

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.secondRatioLegBound (d : ℕ) (cst EL EB C2b : ℝ) : ℝ

The constant of the second summand's (B2) leg.

Equations

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

theorem Algsuperdiff.Section4.Provider.BoundsEaL.secondValueLegBound_pos (d : ℕ) (hd : 0 < d) {cst EL EB : ℝ} (hcst : 0 < cst) (hEL : 0 < EL) (hEB : 0 < EB) : 0 < secondValueLegBound d cst EL EB

theorem Algsuperdiff.Section4.Provider.BoundsEaL.secondRatioLegBound_pos (d : ℕ) {cst EL EB C2b : ℝ} (hEL : 0 < EL) (hEB : 0 < EB) (hC2b : 0 < C2b) : 0 < secondRatioLegBound d cst EL EB C2b

4. The second summand at the anchor's linear and flat slots

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_lintegral_rpow_step3SecondTerm_slot (d : ℕ) [NeZero d] (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (Creg : ℝ) (A : ℝ), 0 < Creg ∧ 0 < A ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ Creg⁻¹ ^ 10 → M.gamma ≤ 1 / 8 → ∀ (Cd : ℝ), 0 ≤ Cd → ∀ (m : ℤ) (R : HCPolySupport.TriadicCube d), R.scale ≤ m → ∀ (q : ℝ), 1 ≤ q → 8 * q ≤ M.gamma⁻¹ → ∫⁻ (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 (Cd * A * (q * ((M.gamma * (↑m - ↑R.scale) + M.gamma) * 3 ^ (2 * (M.gamma * (↑m - ↑R.scale)))))) ^ q

The second summand, evaluated.

∫⁻ (step3SecondTerm)^q ≤ (ofReal (C_d A q (γ(m−j)+γ) 3^{2γ(m−j)}))^q: the anchor's own linear and flat per-scale slots.