OAI/Probability/DilutedSpin/PoissonRateCoupling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.poisson_average_rate_add line 13

   Source documentation

   Common Poisson points give the exact first-moment rate coupling estimate. This is a consequence of convolution, not a coupling hypothesis.

   theorem poisson_average_rate_add (r s : ℝ≥0) {f : ℕ → ℝ} {C : ℝ}
       (hC : 0 ≤ C) (hstep : ∀ n, |f (n+1)-f n| ≤ C) :
       |(∫ n, f n ∂poissonMeasure (r+s))-(∫ n, f n ∂poissonMeasure r)| ≤ C*(s:ℝ) := by
   …