PoissonSmoothing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.poisson_bounded_shift line 13
Source documentation
Poisson's add-one identity gives a smoothing estimate for every bounded test, without any regularity in the count. This is the needed large-rate transfer for the cavity reservoir, not the O(1) unmatched-points estimate.
```
lemma poisson_bounded_shift (r : ℝ≥0) (hr : 0<r) {f : ℕ → ℝ} {B : ℝ}
    (hf : ∀ n, |f n|≤B) :
    |(∫ n, f (n+1) ∂poissonMeasure r)-(∫ n, f n ∂poissonMeasure r)| ≤
      B / Real.sqrt r := by
…
```
lemma OAI.DilutedSpinGlass.poisson_bounded_rate_add line 62