PerCubeSlotCommon

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

Step 5's per-cube evaluation: the shared slot bounds

What this module supplies

Four evaluations shared by the three summands of Step 3's display:

• This is the one place where the two random slots become a γ-power: bullet (B3) at the (B5) index, exactly as SigmaBarLandmark records.
• bracketMajorant_le — hence the bracket majorant is 1 + O(1) on the anchor's own range (√(rγ) ≤ 1, which p ≤ C^{-1}γ^{-1}s delivers). This is the step that makes Step 5's bracket harmless at large p, and it is where the printed q³e^{−C^{-1}γ^{-1}} of bullet (B5)'s moment conversion is spent.
• inv_sigmaBar_le_weight, lambdaSlotMajorant_le_weight — the two σ-gauges with the 3^{γ·} weight moved to the other side, which is how the per-scale factor 3^{γ(m−j)} of Step 5's geometric sum is produced.

References

• ABK26, l.bounds.mathcal.E.aL, Step 4, Step 5.

1. The product of bullets (B6a) and (B5)

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.slotProductBound (d : ℕ) (cst E : ℝ) : ℝ

The constant of the (B6a)·(B5) product: 16 C(2) · fullGradBound · c⋆^{-1/2} · lambdaSlotFactorBound.

Equations

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

theorem Algsuperdiff.Section4.Provider.BoundsEaL.slotProductBound_nonneg (d : ℕ) {cst E : ℝ} (hE : 0 < E) : 0 ≤ slotProductBound d cst E

theorem Algsuperdiff.Section4.Provider.BoundsEaL.gradSlotMajorant_mul_lambdaSlotMajorant_le (d : ℕ) (M : Section3.ABKModel d) {E : ℝ} (hE : 0 < E) (j : ℤ) {r : ℝ} (hr : 0 ≤ r) (hrg : r ≤ M.gamma⁻¹) (hgam : M.gamma ≤ 1 / 2) (hgauge : 3 ^ (M.gamma * ↑j) * (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 16 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)) : gradSlotMajorant M j r * lambdaSlotMajorant d M E j r ≤ slotProductBound d (Section3.Disorder.cstar M) E * (√r * √M.gamma)

THE (B6a)·(B5) IS O(√r √γ).

The 3^{γj} of bullet (B6a) meets the σ_{j−1}^{-1} of bullet (B5), and (B3) at that index turns the pair into 16 c⋆^{-1/2} √γ.

2. The bracket majorant is bounded

theorem Algsuperdiff.Section4.Provider.BoundsEaL.bracketMajorant_le (d : ℕ) (M : Section3.ABKModel d) {E : ℝ} (hE : 0 < E) (j : ℤ) {r : ℝ} (hr : 0 ≤ r) (hrg : 2 * r ≤ M.gamma⁻¹) (hgam : M.gamma ≤ 1 / 2) (hgauge : 3 ^ (M.gamma * ↑j) * (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 16 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)) : bracketMajorant d M E j r ≤ 1 + slotProductBound d (Section3.Disorder.cstar M) E

The bracket is O(1) at large p.

On the anchor's own range -- 2r ≤ γ^{-1}, which p ≤ C^{-1}γ^{-1}s delivers at every exponent Step 5 uses -- the bracket majorant is at most 1 + slotProductBound.

3. The two gauges, with the weight inverted

theorem Algsuperdiff.Section4.Provider.BoundsEaL.inv_sigmaBar_le_weight {d : ℕ} (M : Section3.ABKModel d) (m : ℤ) (hgauge : 3 ^ (M.gamma * ↑m) * (↑(Section3.Annealed.sigmaBar M m))⁻¹ ≤ 4 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)) : (↑(Section3.Annealed.sigmaBar M m))⁻¹ ≤ 3 ^ (-(M.gamma * ↑m)) * (4 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma))

σ_m^{-1} ≤ 3^{−γm} · 4 c⋆^{-1/2}√γ.

theorem Algsuperdiff.Section4.Provider.BoundsEaL.lambdaSlotMajorant_le_weight (d : ℕ) (M : Section3.ABKModel d) {E : ℝ} (hE : 0 < E) (j : ℤ) {r : ℝ} (hr : 0 ≤ r) (hrg : r ≤ M.gamma⁻¹) (hgauge : 3 ^ (M.gamma * ↑j) * (↑(Section3.Annealed.sigmaBar M (j - 1)))⁻¹ ≤ 16 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma)) : lambdaSlotMajorant d M E j r ≤ 3 ^ (-(M.gamma * ↑j)) * (16 * ((√(Section3.Disorder.cstar M))⁻¹ * √M.gamma) * lambdaSlotFactorBound d E)

Λ_{(B5)}(r) ≤ 3^{−γj} · 16 c⋆^{-1/2}√γ · lambdaSlotFactorBound.

4. The squared value slot

noncomputable def Algsuperdiff.Section4.Provider.BoundsEaL.valueSlotWidth (d : ℕ) : ℝ

The dimensional width of the value slot: the L∞ leg's constant plus the mean-value tail's.

Equations

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

theorem Algsuperdiff.Section4.Provider.BoundsEaL.valueSlotWidth_pos {d : ℕ} (hd : 0 < d) : 0 < valueSlotWidth d

theorem Algsuperdiff.Section4.Provider.BoundsEaL.valueSlotMajorant_sq_le {d : ℕ} (M : Section3.ABKModel d) (m j : ℤ) {r : ℝ} (hr : 0 ≤ r) (hgam : M.gamma ≤ 1 / 2) (ht : 0 ≤ ↑m - ↑j) : valueSlotMajorant M m j r ^ 2 ≤ 2 * (HCPolySupport.IndependentSums.gammaMomentConst 2 ^ 2 * valueSlotWidth d ^ 2) * (r * (1 + (↑m - ↑j))) * 3 ^ (2 * (M.gamma * ↑m))

The squared value slot.