GammaTenStripLambdaGrowth

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

The growth rate in the localization scale of the strip ellipticity moment

ABK26, Step 2 of l.approximate.recurrence.formula, e.CG.bounds.2.

The gap this module fills

Closure.GammaTenStripMoment.stripLambdaMoment M m Q is finite at every cube Q, and that module states plainly that no Q-independence is claimed: the local control it integrates lives at the cover scale Cutoff.cubeOriginCoverScale Q, and the lower-tail law makes its moments grow with that scale.

The strip gate of Closure.GammaTenStripAssembly pays sqrt(d 3^{g-p}) sqrt(Cstrip) with p growing linearly in the localization scale K and g fixed, against a Cstrip that carries stripLambdaMoment M m (originCube d K). Finiteness alone is therefore not enough: the gate needs a rate. This module supplies it, and the rate is polynomial: degree eight in K, against a geometric 3^{-p}.

What is proved

• closure_openCubeSet_originCube_subset, cubeOriginCoverScale_originCube_le --- the canonical origin cover of cu_K sits at scale at most K+1. The closure of an open origin cube is inside the closed cube one scale up, and minimality of Nat.find does the rest.
• stripShellBudget and tsum_cutoffGammaMajorant_le --- the summable lower-shell Γ₂ budget of Cutoff.HighMoments.cutoffGammaMajorant, split as (1 + |ell - m|) times a factor free of the cube scale ell. The split is the elementary majorant sqrt(1 + max(ell - (m-r), 0)) <= (1+|ell-m|)(1+r) against the geometric weight 3^{gamma(m-r)}.
• integral_one_add_cutoffLocalControl_pow_le --- for 1 <= q <= 8, E[(1+u_ell)^q] <= 2^{q+1} S^8, where S = stripControlScale is the Γ₂ witness scale of Cutoff.HighMoments.hasGammaMomentGrowthWith_cutoffLocalControl capped below at one. The only probabilistic input is that witness; the rest is 1+u <= 2 max(1,u) and max(1,u)^q <= 1 + u^q.
• stripLambdaMoment_le --- the second moment of the Step-2 ellipticity weight at the envelope of Q, bounded by stripLambdaGrowthConst M times the eighth power of the witness scale at cubeOriginCoverScale Q.
• stripLambdaMoment_originCube_le --- the module's target: stripLambdaMoment M m (cu_K) <= stripLambdaGrowthConst M (stripControlBase M m (1 + K))^8, an explicit degree-eight polynomial in the localization scale K whose coefficients do not depend on K.
• eventually_poly_le_geometric --- the arithmetic the gate then uses: a fixed multiple of (1+K)^8 is eventually below any fixed positive multiple of 3^K.

Binders

Everything below is unconditional in the model: no smallness of cgamma, no inductionState, no regime, no direction normalization and no measurable selection occurs. M.shellPrefix.gamma_pos is the only model fact used, and it is a field of ABKModel.

Scope

Internal Provider infrastructure for the Step-2 boundary-strip gate. There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2, e.CG.bounds.2.

The cover scale of the localization cube

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closure_openCubeSet_originCube_subset {d : ℕ} (m : ℤ) : closure (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m + 1))

The closure of an open origin cube is inside the open origin cube one scale up. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeOriginCoverScale_originCube_le {d : ℕ} (K : ℕ) : Cutoff.cubeOriginCoverScale (HCPolySupport.originCube d ↑K) ≤ ↑K + 1

The canonical origin cover of cu_K is at scale at most K+1. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeOriginCoverScale_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) : 0 ≤ Cutoff.cubeOriginCoverScale Q

The canonical origin cover scale is nonnegative: it is a natural number. Unconditional.

Elementary real facts

The lower-shell budget, split off the cube scale

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripShellBudget (d : ℕ) (gamma : ℝ) (m : ℤ) : ℝ

The cube-scale-free lower-shell budget. The Γ₂ budget Cutoff.HighMoments.cutoffGammaMajorant with its cube-scale factor replaced by the linear majorant 1 + r.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.summable_stripShellBudgetTerm (d : ℕ) {gamma : ℝ} (hgamma : 0 < gamma) (m : ℤ) : Summable fun (r : ℕ) => Real.exp 1 * Cutoff.gaussianMaximumDimConst d * (1 + ↑r) * Real.rpow 3 (gamma * (↑m - ↑r))

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripShellBudget_nonneg (d : ℕ) (gamma : ℝ) (m : ℤ) : 0 ≤ stripShellBudget d gamma m

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.tsum_cutoffGammaMajorant_le (d : ℕ) {gamma : ℝ} (hgamma : 0 < gamma) (m ell : ℤ) : ∑' (r : ℕ), Cutoff.cutoffGammaMajorant d gamma m ell r ≤ (1 + |↑ell - ↑m|) * stripShellBudget d gamma m

The Γ₂ budget at cube scale ell, split. The cube scale enters only through the linear factor 1 + |ell - m|.

on 0 < gamma alone.

The moments of the local control, quantitatively

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripControlScale {d : ℕ} (M : ABKModel d) (ell m : ℤ) : ℝ

The Γ₂ witness scale of the cutoff local control, capped below at one. Three times the witness of Cutoff.HighMoments.hasGammaMomentGrowthWith_cutoffLocalControl; the factor three absorbs sqrt q for q <= 9, and the cap keeps the eighth power monotone.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.one_le_stripControlScale {d : ℕ} (M : ABKModel d) (ell m : ℤ) : 1 ≤ stripControlScale M ell m

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripControlScale_nonneg {d : ℕ} (M : ABKModel d) (ell m : ℤ) : 0 ≤ stripControlScale M ell m

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_cutoffLocalControl_pow_le {d : ℕ} (M : ABKModel d) (ell m : ℤ) {q : ℕ} (hq1 : 1 ≤ q) (hq9 : q ≤ 9) : ∫ (omega : Cutoff.CutoffSample d), Cutoff.cutoffLocalControl ell m omega ^ q ∂↑(Cutoff.cutoffSampleLaw M) ≤ stripControlScale M ell m ^ q

The q-th moment of the local control is below the q-th power of the capped witness scale, for q <= 9. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.integral_one_add_cutoffLocalControl_pow_le {d : ℕ} (M : ABKModel d) (ell m : ℤ) {q : ℕ} (hq1 : 1 ≤ q) (hq8 : q ≤ 8) : ∫ (omega : Cutoff.CutoffSample d), (1 + Cutoff.cutoffLocalControl ell m omega) ^ q ∂↑(Cutoff.cutoffSampleLaw M) ≤ 2 ^ (q + 1) * stripControlScale M ell m ^ 8

The shifted moment. For 1 <= q <= 8, E[(1+u)^q] <= 2^{q+1} S^8. Unconditional.

The growth of the strip ellipticity moment

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripLambdaGrowthConst {d : ℕ} (M : ABKModel d) : ℝ

The K-free coefficient of the strip moment's growth. A fixed polynomial in the model's crude upper-ellipticity majorant and in nu^{-1}.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripLambdaGrowthConst_nonneg {d : ℕ} (M : ABKModel d) : 0 ≤ stripLambdaGrowthConst M

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripLambdaMoment_le {d : ℕ} (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : stripLambdaMoment M m Q ≤ stripLambdaGrowthConst M * stripControlScale M (Cutoff.cubeOriginCoverScale Q) m ^ 8

The strip ellipticity moment, quantitatively. Unconditional.

The polynomial rate at the localization cube

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripControlBase {d : ℕ} (M : ABKModel d) (m : ℤ) : ℝ

The K-free base of the witness scale at the localization cube.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripControlBase_nonneg {d : ℕ} (M : ABKModel d) (m : ℤ) : 0 ≤ stripControlBase M m

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripControlScale_originCube_le {d : ℕ} (M : ABKModel d) (m : ℤ) (K : ℕ) : stripControlScale M (Cutoff.cubeOriginCoverScale (HCPolySupport.originCube d ↑K)) m ≤ stripControlBase M m * (1 + ↑K)

The witness scale at the localization cube grows at most linearly. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.stripLambdaMoment_originCube_le {d : ℕ} (M : ABKModel d) (m : ℤ) (K : ℕ) : stripLambdaMoment M m (HCPolySupport.originCube d ↑K) ≤ stripLambdaGrowthConst M * (stripControlBase M m * (1 + ↑K)) ^ 8

The target: the strip ellipticity moment grows at most polynomially in the localization scale. Degree eight, with K-free coefficients. Unconditional.

Polynomial against geometric

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.eventually_poly_le_geometric (A : ℝ) {c : ℝ} (hc : 0 < c) : ∀ᶠ (K : ℕ) in Filter.atTop, A * (1 + ↑K) ^ 8 ≤ c * 3 ^ K

The arithmetic the strip gate uses. A fixed multiple of (1+K)^8 is eventually below any fixed positive multiple of 3^K.

on 0 < c alone.