poissonPMFRealSum — Mathlib

English

The sum over all n of Poisson pmfReal equals 1.

Русский

Сумма по всем n плотности Пуассона равна единице.

LaTeX

$$$\\sum_{n=0}^{\\infty} \\mathrm{poissonPMFReal}(r,n) = 1$$$

Lean4

theorem poissonPMFRealSum (r : ℝ≥0) : HasSum (fun n ↦ poissonPMFReal r n) 1 :=
  by
  let r := r.toReal
  unfold poissonPMFReal
  apply (hasSum_mul_left_iff (exp_ne_zero r)).mp
  simp only [mul_one]
  have : (fun i ↦ rexp r * (rexp (-r) * r ^ i / ↑(Nat.factorial i))) = fun i ↦ r ^ i / ↑(Nat.factorial i) :=
    by
    ext n
    rw [mul_div_assoc, exp_neg, ← mul_assoc, ← div_eq_mul_inv, div_self (exp_ne_zero r), one_mul]
  rw [this, exp_eq_exp_ℝ]
  exact NormedSpace.expSeries_div_hasSum_exp ℝ r

Похожие утверждения