Theorems · Theorem · probability

ProbabilityTheory.charFun_map_cast_poissonMeasure

∀ (r : NNReal) (t : ℝ),
  MeasureTheory.charFun (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) t =
    Complex.exp (↑↑r * (Complex.exp (↑t * Complex.I) - 1))

The characteristic function of the Poisson distribution with rate r is t ↦ exp(r(exp(it) - 1)).

Defined in

Mathlib.Probability.Distributions.Poisson.Basic

Cited by

0 results in Mathlib

Foundations

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