LocalControlMoment

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

Gaussian moments for local cutoff controls

This module transports J2's literal one-sided tail to finite translated unit-cube maxima without introducing an independence assumption.

noncomputable def Algsuperdiff.Section3.Cutoff.gaussianMaximumDimConst (d : ℕ) : ℝ

The dimension-only constant in the finite Gaussian maximum estimate for triadic unit descendants. It is deliberately named so later shell-scale summability statements cannot silently change the normalization.

Equations

• Algsuperdiff.Section3.Cutoff.gaussianMaximumDimConst d = HCPolySupport.IndependentSums.gammaMomentConst 2 * √(3 * (1 + ↑d * Real.log 3))

theorem Algsuperdiff.Section3.Cutoff.gaussianMaximumDimConst_pos (d : ℕ) : 0 < gaussianMaximumDimConst d

theorem Algsuperdiff.Section3.Cutoff.zeroShell_unitCubeValueNorm_gaussian_tail {d : ℕ} (M : ABKModel d) (t : ℝ) (ht : 1 ≤ t) : ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) {j : Frozen.Assumptions.ShellField d | t < j.unitCubeValueNorm} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))

J2's sequence-level tail induces the same literal tail for the exact zero-shell marginal law.

theorem Algsuperdiff.Section3.Cutoff.zeroShell_translatedUnitCubeControl_gaussian_tail {d : ℕ} (M : ABKModel d) (z : HCPolySupport.Vec d) (t : ℝ) (ht : 1 ≤ t) : ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) {j : Frozen.Assumptions.ShellField d | t < translatedUnitCubeControl z j} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))

Stationarity transports J2's unit-cube tail to every translated unit control under the zero-shell law.

theorem Algsuperdiff.Section3.Cutoff.integrable_originCubeUnitControlMax_zero {d : ℕ} (M : ABKModel d) (q : ℤ) (hq : 0 ≤ q) : MeasureTheory.Integrable (originCubeUnitControlMax q hq) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

Under the zero-shell marginal, the exact finite maximum over the unit descendants of a nonnegative-scale origin cube is integrable. No independence of the translated controls is used: the finite-maximum lemma consumes only their individual J2 tails.

theorem Algsuperdiff.Section3.Cutoff.integral_originCubeUnitControlMax_zero_le {d : ℕ} (M : ABKModel d) (q : ℤ) (hq : 0 ≤ q) : ∫ (j : Frozen.Assumptions.ShellField d), originCubeUnitControlMax q hq j ∂↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) ≤ gaussianMaximumDimConst d * √(1 + ↑q.toNat)

The finite translated-unit maximum has the explicit dimension--depth Gaussian expectation bound. The expectation is used only together with the integrability theorem above (and is therefore never a totalized-integral surrogate).

theorem Algsuperdiff.Section3.Cutoff.integrable_localCubeControl_under_zeroShellLaw_of_nonneg {d : ℕ} (M : ABKModel d) (q : ℤ) (hq : 0 ≤ q) : MeasureTheory.Integrable (localCubeControl q) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

On nonnegative cube scales, the exact local control is integrable under the zero-shell marginal because it is pointwise bounded by the integrable finite descendant maximum.

theorem Algsuperdiff.Section3.Cutoff.integrable_localCubeControl_under_zeroShellLaw_of_nonpos {d : ℕ} (M : ABKModel d) (q : ℤ) (hq : q ≤ 0) : MeasureTheory.Integrable (localCubeControl q) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

On nonpositive cube scales, the local control is integrable under the zero-shell marginal by direct comparison with the unit-cube control.

theorem Algsuperdiff.Section3.Cutoff.integrable_localCubeControl_under_zeroShellLaw {d : ℕ} (M : ABKModel d) (q : ℤ) : MeasureTheory.Integrable (localCubeControl q) ↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P)

A convenient complete zero-shell integrability A for every integer cube scale.

theorem Algsuperdiff.Section3.Cutoff.integral_localCubeControl_under_zeroShellLaw_le_of_nonneg {d : ℕ} (M : ABKModel d) (q : ℤ) (hq : 0 ≤ q) : ∫ (j : Frozen.Assumptions.ShellField d), localCubeControl q j ∂↑(Frozen.Assumptions.ShellField.zeroShellLaw M.P) ≤ gaussianMaximumDimConst d * √(1 + ↑q.toNat)

The nonnegative-scale local control inherits the finite-maximum expectation bound. Both integrability facts are supplied explicitly before monotonicity of the Bochner integral is invoked.