Moments and generating functions of the Poisson distribution

This file develops the probability-generating function of the native Poisson law and the elementary analytic API of the real-valued Poisson law. For a rate r : ℝ≥0, the cast law Po(ℝ, r) has all exponential moments, moment-generating function exp (r * (exp t - 1)), cumulant-generating function r * (exp t - 1), and both mean and variance equal to r.

The zero-rate law is recorded explicitly as the point mass at zero.

The series calculation for the probability-generating function follows the calculation of ProbabilityTheory.charFun_map_cast_poissonMeasure in Mathlib; the moment-generating function is its value at exp t. The same series, together with the factorial-moment series ∑ k, exp (-r) r ^ k / k! * k.descFactorial n = r ^ n, is also stated as a HasSum, the form in which Poisson mixtures consume it. The moment formulas are then obtained by differentiating the moment-generating function.

@[simp]

theorem TauCeti.Probability.poissonMeasure_zero : ProbabilityTheory.poissonMeasure 0 = MeasureTheory.Measure.dirac 0

A Poisson law of rate zero is concentrated at zero.

theorem TauCeti.Probability.poissonMeasure_real_singleton_zero (r : NNReal) : (ProbabilityTheory.poissonMeasure r).real {0} = Real.exp (-↑r)

A Poisson law of rate r has mass exp (-r) at zero.

theorem TauCeti.Probability.poissonMeasure_singleton_zero_eq_one_iff {r : NNReal} : (ProbabilityTheory.poissonMeasure r) {0} = 1 ↔ r = 0

A Poisson law puts all its mass at zero exactly at rate zero.

theorem TauCeti.Probability.poissonMeasure_singleton_ne_zero_iff (r : NNReal) (n : ℕ) : (ProbabilityTheory.poissonMeasure r) {n} ≠ 0 ↔ r ≠ 0 ∨ n = 0

A Poisson singleton has nonzero mass exactly when the rate is positive or the count is zero.

theorem TauCeti.Probability.hasSum_pow_poissonMeasure (r : NNReal) (z : ℝ) : HasSum (fun (k : ℕ) => Real.exp (-↑r) * ↑r ^ k / ↑k.factorial * z ^ k) (Real.exp ((z - 1) * ↑r))

The probability-generating series of a Poisson law: weighted by the Poisson masses, the powers z ^ k sum to exp ((z - 1) * r).

theorem TauCeti.Probability.hasSum_descFactorial_poissonMeasure (r : NNReal) (n : ℕ) : HasSum (fun (k : ℕ) => Real.exp (-↑r) * ↑r ^ k / ↑k.factorial * ↑(k.descFactorial n)) (↑r ^ n)

The factorial moments of a Poisson law as a weighted series: weighted by the Poisson masses, the falling factorials k.descFactorial n sum to r ^ n.

theorem TauCeti.Probability.lintegral_ofReal_poissonMeasure {f : ℕ → ℝ} (hf : 0 ≤ f) (r : NNReal) {a : ℝ} (ha : HasSum (fun (k : ℕ) => Real.exp (-↑r) * ↑r ^ k / ↑k.factorial * f k) a) : ∫⁻ (k : ℕ), ENNReal.ofReal (f k) ∂ProbabilityTheory.poissonMeasure r = ENNReal.ofReal a

The lower integral of a nonnegative observable against a Poisson law is the weighted sum of its values, whenever that sum converges.

@[simp]

theorem TauCeti.Probability.pgf_poissonMeasure (r : NNReal) (t : ℝ) : pgf id (ProbabilityTheory.poissonMeasure r) t = Real.exp (↑r * (t - 1))

The probability-generating function of a Poisson distribution.

@[simp]

theorem TauCeti.Probability.mgf_id_map_cast_poissonMeasure (r : NNReal) : ProbabilityTheory.mgf (fun (x : ℝ) => x) (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) = fun (t : ℝ) => Real.exp (↑r * (Real.exp t - 1))

The moment-generating function of a real-valued Poisson law of rate r is t ↦ exp (r * (exp t - 1)).

theorem TauCeti.Probability.integrable_exp_mul_id_map_cast_poissonMeasure (r : NNReal) (t : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (t * x)) (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r))

Every exponential moment of a real-valued Poisson law is integrable.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_map_cast_poissonMeasure (r : NNReal) : ProbabilityTheory.integrableExpSet (fun (x : ℝ) => x) (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) = Set.univ

The exponential-integrability domain of a real-valued Poisson law is all of ℝ.

theorem TauCeti.Probability.memLp_id_map_cast_poissonMeasure (r p : NNReal) : MeasureTheory.MemLp id (↑p) (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r))

A real-valued Poisson law has finite moments of every order.

@[simp]

theorem TauCeti.Probability.cgf_id_map_cast_poissonMeasure (r : NNReal) : ProbabilityTheory.cgf (fun (x : ℝ) => x) (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) = fun (t : ℝ) => ↑r * (Real.exp t - 1)

The cumulant-generating function of a real-valued Poisson law of rate r is t ↦ r * (exp t - 1).

@[simp]

theorem TauCeti.Probability.integral_id_map_cast_poissonMeasure (r : NNReal) : ∫ (x : ℝ), x ∂MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r) = ↑r

The mean of a real-valued Poisson law is its rate.

@[simp]

theorem TauCeti.Probability.integral_sq_map_cast_poissonMeasure (r : NNReal) : ∫ (x : ℝ), x ^ 2 ∂MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r) = ↑r ^ 2 + ↑r

The second raw moment of a real-valued Poisson law is r ^ 2 + r.

@[simp]

theorem TauCeti.Probability.variance_id_map_cast_poissonMeasure (r : NNReal) : ProbabilityTheory.variance id (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) = ↑r

The variance of a real-valued Poisson law is its rate.

theorem TauCeti.Probability.integrable_natCast_rpow_poissonMeasure (r : NNReal) {p : ℝ} (hp : 0 ≤ p) : MeasureTheory.Integrable (fun (n : ℕ) => ↑n ^ p) (ProbabilityTheory.poissonMeasure r)

Every nonnegative real power of the native Poisson count is integrable.

@[simp]

theorem TauCeti.Probability.integral_natCast_poissonMeasure (r : NNReal) : ∫ (n : ℕ), ↑n ∂ProbabilityTheory.poissonMeasure r = ↑r

The mean of the native Poisson count is its rate.

@[simp]

theorem TauCeti.Probability.variance_natCast_poissonMeasure (r : NNReal) : ProbabilityTheory.variance (fun (n : ℕ) => ↑n) (ProbabilityTheory.poissonMeasure r) = ↑r

The variance of the native Poisson count is its rate.

theorem TauCeti.Probability.integral_of_hasLaw_map_cast_poissonMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {r : NNReal} (hX : ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) P) : ∫ (ω : Ω), X ω ∂P = ↑r

A real random variable with Poisson law has expectation equal to the rate.

theorem TauCeti.Probability.variance_of_hasLaw_map_cast_poissonMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {r : NNReal} (hX : ProbabilityTheory.HasLaw X (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r)) P) : ProbabilityTheory.variance X P = ↑r

A real random variable with Poisson law has variance equal to the rate.