ShellLawJ2 #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
structure
Algsuperdiff.Frozen.Assumptions.ShellLawJ2
(d : ℕ)
(P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d))
:
ABK26 (J2): the exact strict Gaussian tail for the three
weighted essential-L∞ cube norms. The qualitative C^2
regularity is already enforced by the shell carrier and is not repeated as a
hypothesis.
- gaussian_tail (t : ℝ) : 1 ≤ t → ↑P {F : ℤ → ShellField d | t < ShellField.j2Observable d (F 0)} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))