Theorems · Theorem · probability

ProbabilityTheory.integral_poissonMeasure

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (r : NNReal)
  (f : ℕ → E),
  ∫ (n : ℕ), f n ∂ProbabilityTheory.poissonMeasure r = ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f n

The integral of a function taking values in a finite-dimensional space against poissonMeasure r is given by its sum weighted by exp (-r) * r ^ n / n!. This version does not require integrability, as the integral exists if and only if the sum exists, and otherwise they are both defined to be zero. See integral_poissonMeasure' with a general codomain which assumes integrability.

Defined in

Mathlib.Probability.Distributions.Poisson.Basic

Cited by

2 results in Mathlib

Foundations

Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional