HighMoments

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

Higher moments of the genuine cutoff local envelope

The lower-infinite cutoff itself is defined only on CutoffSample. This module follows the same rule for its local control: the displayed series is used only on that carrier, where LowerTailGood supplies its summability. In particular, this is not a totalized control on arbitrary shell sequences.

The upper ellipticity lane must control the full nonsymmetric coefficient matrix. Thus its random envelope is built from the skew cutoff, not confused with the deterministic lower energy constant nu.

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffLocalControl {d : ℕ} (ell m : ℤ) (omega : CutoffSample d) : ℝ

The actual lower-tail local control on the public convergence carrier. Its value is the nonnegative series of the literal local controls of all shells j_(m-r).

Equations

• Algsuperdiff.Section3.Cutoff.cutoffLocalControl ell m omega = ∑' (r : ℕ), Algsuperdiff.Section3.Cutoff.localCubeControl ell (↑omega (m - ↑r))

theorem Algsuperdiff.Section3.Cutoff.cutoffLocalControl_nonneg {d : ℕ} (ell m : ℤ) (omega : CutoffSample d) : 0 ≤ cutoffLocalControl ell m omega

The cutoff local-control series is nonnegative.

theorem Algsuperdiff.Section3.Cutoff.summable_cutoffLocalControl {d : ℕ} (ell m : ℤ) (omega : CutoffSample d) : Summable fun (r : ℕ) => localCubeControl ell (↑omega (m - ↑r))

The defining local-control series is summable at every point of the public cutoff carrier.

noncomputable def Algsuperdiff.Section3.Cutoff.localCubeControlGammaScale (d : ℕ) (q : ℤ) : ℝ

Internal quantitative scale for the literal zero-shell local control. It records the finite lattice entropy at a cube scale and is not a new normalization of any source-facing object.

Equations

• Algsuperdiff.Section3.Cutoff.localCubeControlGammaScale d q = √(3 * (1 + ↑d * Real.log 3)) * √(1 + max (↑q) 0)

theorem Algsuperdiff.Section3.Cutoff.hasGammaMomentGrowthWith_localCubeControl_zero {d : ℕ} (M : ABKModel d) (q : ℤ) : HCPolySupport.IndependentSums.HasGammaMomentGrowthWith (↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)) 2 (localCubeControl q) (HCPolySupport.IndependentSums.gammaMomentConst 2 * localCubeControlGammaScale d q)

The zero-shell local control has an explicit Γ₂ moment witness. The only scale dependence is the square root of the number of unit descendants; no independence between translated controls is assumed.

noncomputable def Algsuperdiff.Section3.Cutoff.cutoffGammaMajorant (d : ℕ) (gamma : ℝ) (m ell : ℤ) (r : ℕ) : ℝ

The deterministic Γ₂ budget for one lower shell. It is the earlier expectation majorant with the harmless tail-to-moment factor displayed, so its summability follows from the already-verified geometric majorant.

Equations

• Algsuperdiff.Section3.Cutoff.cutoffGammaMajorant d gamma m ell r = Real.exp 1 * Algsuperdiff.Section3.Cutoff.expectedCubeMajorant d gamma m ell r

theorem Algsuperdiff.Section3.Cutoff.cutoffGammaMajorant_pos (d : ℕ) (gamma : ℝ) (m ell : ℤ) (r : ℕ) : 0 < cutoffGammaMajorant d gamma m ell r

theorem Algsuperdiff.Section3.Cutoff.summable_cutoffGammaMajorant {d : ℕ} {gamma : ℝ} (hgamma : 0 < gamma) (m ell : ℤ) : Summable (cutoffGammaMajorant d gamma m ell)

theorem Algsuperdiff.Section3.Cutoff.isBigOWith_gammaSigma_localCubeControl_lowerShell {d : ℕ} (M : ABKModel d) (m ell : ℤ) (r : ℕ) : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 2) (fun (omega : ℤ → Frozen.Assumptions.ShellField d) => localCubeControl ell (omega (m - ↑r))) (cutoffGammaMajorant d M.gamma m ell r)

A single lower shell has the explicit Γ₂ tail budget matching the summable deterministic majorant. This transports only the literal marginal scaling law, and uses no cross-shell independence.

theorem Algsuperdiff.Section3.Cutoff.isBigO_gammaSigma_cutoffLocalControl {d : ℕ} (M : ABKModel d) (ell m : ℤ) : HCPolySupport.IndependentSums.IsBigO (↑(cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (cutoffLocalControl ell m) (HCPolySupport.IndependentSums.gammaTriangleConst 2 * ∑' (r : ℕ), cutoffGammaMajorant d M.gamma m ell r)

The actual lower-infinite cutoff local control has a scale-summable Γ₂ bound on its public convergence carrier. This is a countable triangle over its literal lower shells; it assumes neither shell independence nor a totalized cutoff outside CutoffSample.

theorem Algsuperdiff.Section3.Cutoff.measurable_cutoffLocalControl {d : ℕ} (ell m : ℤ) : Measurable (cutoffLocalControl ell m)

Measurability of the genuine cutoff local envelope follows from its everywhere-convergent partial sums on CutoffSample.

theorem Algsuperdiff.Section3.Cutoff.hasGammaMomentGrowthWith_cutoffLocalControl {d : ℕ} (M : ABKModel d) (ell m : ℤ) : HCPolySupport.IndependentSums.HasGammaMomentGrowthWith (↑(cutoffSampleLaw M)) 2 (cutoffLocalControl ell m) (HCPolySupport.IndependentSums.gammaMomentConst 2 * (HCPolySupport.IndependentSums.gammaTriangleConst 2 * ∑' (r : ℕ), cutoffGammaMajorant d M.gamma m ell r))

Witness-level Γ₂ moment aggregation for the actual lower cutoff. The explicit scale is the summable lower-shell budget multiplied only by CoarseGraining's documented finite-triangle and tail-to-moment constants.