Summability #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Almost-sure summability of lower local-control tails #
The Gaussian maximum estimate carries an explicit dimensional prefactor. It
is retained in expectedCubeMajorant; this is an internal proof majorant, not
a normalization of a source-facing cutoff object.
noncomputable def
Algsuperdiff.Section3.Cutoff.expectedCubeMajorant
(d : ℕ)
(gamma : ℝ)
(m ell : ℤ)
(r : ℕ)
:
The summable expectation majorant for one lower shell. The dimensional Gaussian-maximum factor is displayed explicitly rather than hidden.
Equations
- Algsuperdiff.Section3.Cutoff.expectedCubeMajorant d gamma m ell r = Algsuperdiff.Section3.Cutoff.gaussianMaximumDimConst d * Algsuperdiff.Section3.Cutoff.cubeMajorant gamma m ell r
Instances For
theorem
Algsuperdiff.Section3.Cutoff.summable_expectedCubeMajorant
{d : ℕ}
{gamma : ℝ}
(hgamma : 0 < gamma)
(m ell : ℤ)
:
Summable (expectedCubeMajorant d gamma m ell)
The exact deterministic lower-tail-good condition holds almost surely under the canonical shell law.