PerCubeSlotFirst

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

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

What this module does

PerCubeFirstThird.lintegral_rpow_step3FirstTerm_le supplies the first summand's q-th moment at the symbolic majorant 4C · R_bracket · R_{B4}². This module evaluates it against the anchor's own slot K p γ s^{-2}:

• the bracket is O(1) (PerCubeSlotCommon.bracketMajorant_le);
• R_{B4}(4q)² is O(q γ s^{-2}). Its Γ₂ lane gives the printed C s^{-1}q^{1/2}γ^{1/2} squared, i.e. exactly the slot; its Γ_{1/2} lane gives the printed C q² e^{−C^{-1}c⋆³γ^{-1}} squared, and the exponential beats the q-power on the anchor's own range q ≤ γ^{-1} WITH one factor γ to spare (SecondTermArithmetic.pow_mul_exp_neg_inv_le_mul).

That second point is the only place where the printed Γ_{1/2} lane has to be priced; it costs no p-restriction whatsoever.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4 bullet (B4), Step 5.

1. The squared (2,2)-error majorant

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.errSlotSquareBound (d : ℕ) (cst C : ℝ) : ℝ

The constant of the squared (B4) majorant: the Γ₂ lane's 24 C(2)² pen₂² C² c⋆^{-2} plus the Γ_{1/2} lane's, the latter priced by x^5 e^{-x} ≤ 5!.

Equations

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

theorem Algsuperdiff.Section4.Provider.BoundsEaL.annulusPenalty_nonneg (d : ℕ) {sigma : ℝ} (hsigma : 0 < sigma) (p : ℕ) : 0 ≤ Proportion.annulusPenalty d sigma p

theorem Algsuperdiff.Section4.Provider.BoundsEaL.errSlotSquareBound_pos (d : ℕ) {cst C : ℝ} (hcst : 0 < cst) (hC : 0 < C) : 0 < errSlotSquareBound d cst C

theorem Algsuperdiff.Section4.Provider.BoundsEaL.errSlotMajorant_sq_le (d : ℕ) (M : Section3.ABKModel d) {C s q : ℝ} (hC : 0 < C) (hs : 0 < s) (hs1 : s ≤ 1) (hq : 1 ≤ q) (hqg : q ≤ M.gamma⁻¹) : errSlotMajorant d M C s (4 * q) ^ 2 ≤ errSlotSquareBound d (Section3.Disorder.cstar M) C * (q * (M.gamma * (s⁻¹ * s⁻¹)))

The squared (2,2)-error majorant is O(q γ s^{-2}).

Both printed lanes are evaluated: the Γ₂ lane is the anchor's own (s^{-1}√q√γ)², and the Γ_{1/2} lane's q⁴e^{−2C^{-1}c⋆³γ^{-1}} is at most 5!(2C^{-1}c⋆³)^{-5} γ on the anchor's own range q ≤ γ^{-1}.

2. The first summand at the anchor's first slot

theorem Algsuperdiff.Section4.Provider.BoundsEaL.exists_lintegral_rpow_step3FirstTerm_slot (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 → ∀ (s : ℝ), 0 < s → s ≤ 1 / 4 → 8 * M.gamma ≤ s → ∀ (m : ℤ) (R : HCPolySupport.TriadicCube d), R.scale ≤ m → ∀ (q : ℝ), 1 ≤ q → 8 * q ≤ M.gamma⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (step3FirstTerm Cd M m R omega s (lFreeGradSlot m (tailSeriesGauge m) R omega)) ^ q ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (Cd * A * (q * (M.gamma * (s⁻¹ * s⁻¹)))) ^ q

The first summand, evaluated.

∫⁻ (step3FirstTerm)^q ≤ (ofReal (C_d A q γ s^{-2}))^q, uniformly in the descendant scale: this is the anchor's own first slot.