GaussianTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit exponential tail and ball estimates for standard Gaussian. Constants depend only on the ambient dimension (and polynomial degree).

theorem OAI.GeneralMahler.normal_tail line 12
theorem OAI.GeneralMahler.normal_ball_lower line 51
Source documentation
Uniform lower estimate for the Gaussian mass of a ball measured in standard coordinates.
```
theorem normal_ball_lower (m : ℕ) {r:ℝ} (hr : 0 < r) :
    ∃ c > (0:ℝ), ∀ (x:Rn m),
      c * exp (-((‖x‖+r)^2)/2) ≤ (normal m).real (closedBall x r) := by
…
```
Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.normal
lemma OAI.GeneralMahler.tail_exp_le_a line 99
Source documentation
Useful for absorbing large cutoff estimates into the smaller Gaussian lower bound in Lemma Gaussian layer tails.
```
lemma tail_exp_le_a (s : ℝ) (hs : 0 ≤ s) :
    Real.exp (-( (4*(1+s))^2) / 4) ≤ (√(2*π)) * Real.exp 4 * Layers.a (-s) := by
…
```
Mentions: OAI.GeneralMahler.Layers.a