Probability-generating functions

This file defines the probability-generating function of a natural-number-valued random variable and establishes its basic measure-theoretic API. The central results relate it to Mathlib's moment-generating function and show that it turns sums of independent random variables into products. The file then identifies the generating function of a finite measure on ℕ with the sum of the power series carrying its singleton masses, so that the generating function is analytic on (-1, 1) and its Taylor coefficients at the origin recover those masses; consequently a law on ℕ is determined by its generating function near 0.

Main declarations

• TauCeti.Probability.pgf — the probability-generating function.
• TauCeti.Probability.pgf_exp — evaluation at exp t is a moment-generating function, and TauCeti.Probability.mgf_id_map_natCast restates this for the real cast of a law on ℕ.
• TauCeti.Probability.integrable_pow_of_abs_le_one — on [-1, 1] the integrand is integrable under a finite measure.
• TauCeti.Probability.IndepFun.pgf_add and TauCeti.Probability.iIndepFun.pgf_sum — multiplicativity over binary and finite sums of independent random variables when the factor integrands are integrable.
• TauCeti.Probability.IndepFun.pgf_add_of_abs_le_one and TauCeti.Probability.iIndepFun.pgf_sum_of_abs_le_one — the corresponding formulas on the interval [-1, 1], where integrability is automatic.
• Measure.pgf_conv and Measure.pgf_conv_of_abs_le_one — convolution becomes multiplication under the natural integrability hypotheses, and for finite measures on [-1, 1].
• TauCeti.Probability.hasSum_pgf and TauCeti.Probability.pgf_eq_tsum — the power-series expansion in the singleton masses, valid on [-1, 1].
• TauCeti.Probability.hasFPowerSeriesOnBall_pgf and TauCeti.Probability.analyticOnNhd_pgf — analyticity on the open unit ball.
• TauCeti.Probability.iteratedDeriv_pgf_one — under a positive exponential moment, the derivatives at one are the factorial moments.
• TauCeti.Probability.tendsto_iteratedDeriv_pgf_nhdsLT_one — under a finite factorial moment, the corresponding derivative tends to that moment as the argument tends to one from below.
• TauCeti.Probability.iteratedDeriv_pgf_zero — the Taylor coefficients at the origin are the singleton masses, with TauCeti.Probability.pgf_zero and TauCeti.Probability.deriv_pgf_zero reading off the first two.
• TauCeti.Probability.measure_eq_of_pgf_eventuallyEq and TauCeti.Probability.identDistrib_of_pgf_eventuallyEq — uniqueness of the law from the germ of the generating function at 0, with the corollaries TauCeti.Probability.measure_eq_of_pgf_eqOn and TauCeti.Probability.identDistrib_of_pgf_eqOn reading the hypothesis off (-1, 1).

noncomputable def TauCeti.Probability.pgf {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℕ) (μ : MeasureTheory.Measure Ω) (t : ℝ) : ℝ

The probability-generating function of a natural-number-valued random variable X with respect to a measure μ.

theorem TauCeti.Probability.pgf_def {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℕ) (μ : MeasureTheory.Measure Ω) (t : ℝ) : pgf X μ t = ∫ (ω : Ω), t ^ X ω ∂μ

The defining integral formula for the probability-generating function. This is the canonical way to unfold pgf, which is otherwise sealed.

theorem TauCeti.Probability.pgf_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℕ} (hXY : X =ᵐ[μ] Y) : pgf X μ = pgf Y μ

The probability-generating function is unchanged by replacing the random variable almost everywhere.

@[simp]

theorem TauCeti.Probability.pgf_zero_measure {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℕ) : pgf X 0 = 0

The probability-generating function of the zero measure vanishes.

@[simp]

theorem TauCeti.Probability.pgf_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (X : Ω → ℕ) : pgf X μ 1 = μ.real Set.univ

Evaluation of a probability-generating function at one gives the total mass.

@[simp]

theorem TauCeti.Probability.pgf_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (n : ℕ) (t : ℝ) : pgf (fun (x : Ω) => n) μ t = μ.real Set.univ * t ^ n

A constant natural-number-valued random variable has the expected monomial generating function.

theorem TauCeti.Probability.pgf_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℕ} (hX : AEMeasurable X μ) (t : ℝ) : pgf id (MeasureTheory.Measure.map X μ) t = pgf X μ t

The probability-generating function can be computed on the law of the random variable.

theorem TauCeti.Probability.HasLaw.pgf_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℕ} {ν : MeasureTheory.Measure ℕ} (hX : ProbabilityTheory.HasLaw X ν μ) (t : ℝ) : pgf X μ t = pgf id ν t

Random variables with a given law have the same probability-generating function as that law.

theorem TauCeti.Probability.pgf_exp {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℕ) (μ : MeasureTheory.Measure Ω) (t : ℝ) : pgf X μ (Real.exp t) = ProbabilityTheory.mgf (fun (ω : Ω) => ↑(X ω)) μ t

Evaluating the probability-generating function at exp t recovers the moment-generating function of the real-valued cast of the random variable.

theorem TauCeti.Probability.mgf_id_map_natCast (ν : MeasureTheory.Measure ℕ) (t : ℝ) : ProbabilityTheory.mgf id (MeasureTheory.Measure.map Nat.cast ν) t = pgf id ν (Real.exp t)

The moment-generating function of the real cast of a law on ℕ is its probability-generating function evaluated at exp t.

theorem TauCeti.Probability.integrable_pow_of_abs_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℕ} (hX : AEMeasurable X μ) {t : ℝ} (ht : |t| ≤ 1) : MeasureTheory.Integrable (fun (ω : Ω) => t ^ X ω) μ

For a finite measure, the integrand of a probability-generating function is integrable on [-1, 1].

theorem MeasureTheory.Measure.abs_pgf_sub_one_sub_mul_le (ν : Measure ℕ) [IsProbabilityMeasure ν] {z : ℝ} (hz : |z| ≤ 1) : |TauCeti.Probability.pgf id ν z - 1 - (z - 1) * ν.real {1}| ≤ 2 * ν.real (Set.Ici 2)

For a probability law on ℕ, the error in the approximation pgf id ν z ≈ 1 + (z - 1) * ν.real {1} is bounded by twice the multiple-occurrence probability. The estimate holds on the entire interval [-1, 1].

theorem TauCeti.Probability.IndepFun.pgf_add {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℕ} (hXY : ProbabilityTheory.IndepFun X Y μ) (t : ℝ) (hXt : MeasureTheory.Integrable (fun (ω : Ω) => t ^ X ω) μ) (hYt : MeasureTheory.Integrable (fun (ω : Ω) => t ^ Y ω) μ) : pgf (X + Y) μ t = pgf X μ t * pgf Y μ t

The probability-generating function of a sum of two independent natural-number-valued random variables is the product of their generating functions whenever both factor integrands are integrable.

The integrability hypotheses deliberately restrict the public statement so that it expresses a product of genuine expectations. Mathlib's totalized integral gives the same equality without these hypotheses, but in the non-integrable cases it is merely an artifact of totalization.

theorem TauCeti.Probability.IndepFun.pgf_add_of_abs_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X Y : Ω → ℕ} (hXY : ProbabilityTheory.IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) {t : ℝ} (ht : |t| ≤ 1) : pgf (X + Y) μ t = pgf X μ t * pgf Y μ t

Under a finite measure, on [-1, 1] the probability-generating function of a sum of two independent natural-number-valued random variables is the product of their generating functions.

theorem MeasureTheory.Measure.pgf_conv (μ ν : Measure ℕ) (t : ℝ) (hμ : Integrable (fun (k : ℕ) => t ^ k) μ) (hν : Integrable (fun (k : ℕ) => t ^ k) ν) : TauCeti.Probability.pgf id (μ.conv ν) t = TauCeti.Probability.pgf id μ t * TauCeti.Probability.pgf id ν t

The probability-generating function sends convolution to multiplication whenever both factor integrands are integrable.

theorem MeasureTheory.Measure.pgf_conv_of_abs_le_one (μ ν : Measure ℕ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] {t : ℝ} (ht : |t| ≤ 1) : TauCeti.Probability.pgf id (μ.conv ν) t = TauCeti.Probability.pgf id μ t * TauCeti.Probability.pgf id ν t

On [-1, 1], the probability-generating function sends convolution of finite measures to multiplication.

theorem TauCeti.Probability.iIndepFun.pgf_sum {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℕ} (h_indep : ProbabilityTheory.iIndepFun X μ) (s : Finset ι) (t : ℝ) (h_int : ∀ i ∈ s, MeasureTheory.Integrable (fun (ω : Ω) => t ^ X i ω) μ) : pgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, pgf (X i) μ t

A probability-generating function turns a finite sum of independent random variables into the product of their generating functions whenever every factor integrand is integrable.

theorem TauCeti.Probability.iIndepFun.pgf_sum_of_abs_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℕ} (h_indep : ProbabilityTheory.iIndepFun X μ) (s : Finset ι) (h_meas : ∀ i ∈ s, AEMeasurable (X i) μ) {t : ℝ} (ht : |t| ≤ 1) : pgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, pgf (X i) μ t

On [-1, 1], a probability-generating function turns a finite sum of independent random variables into the product of their generating functions.

Coefficient recovery and uniqueness

A finite measure on ℕ is the weighted sum of Dirac masses ∑ ν {n} • δ n, so its generating function is the sum of the power series ∑ ν.real {n} * t ^ n. The masses are bounded by the total mass, so that series converges on the whole open unit ball and the generating function is analytic there. Reading its Taylor coefficients at the origin returns the masses, and hence a finite measure on ℕ, in particular a probability measure, is determined by its generating function near 0.

theorem TauCeti.Probability.hasSum_pgf_of_integrable (ν : MeasureTheory.Measure ℕ) {t : ℝ} (ht : MeasureTheory.Integrable (fun (n : ℕ) => t ^ n) ν) : HasSum (fun (n : ℕ) => ν.real {n} * t ^ n) (pgf id ν t)

If the monomial integrand is integrable, the probability-generating function is the sum of the power series whose coefficients are the singleton masses.

theorem TauCeti.Probability.hasSum_pgf (ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure ν] {t : ℝ} (ht : |t| ≤ 1) : HasSum (fun (n : ℕ) => ν.real {n} * t ^ n) (pgf id ν t)

Under a finite measure on ℕ, the probability-generating function is the sum of the power series whose coefficients are the singleton masses, on [-1, 1].

theorem TauCeti.Probability.pgf_eq_tsum (ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure ν] {t : ℝ} (ht : |t| ≤ 1) : pgf id ν t = ∑' (n : ℕ), ν.real {n} * t ^ n

The power-series expansion of the probability-generating function of a finite measure on ℕ on [-1, 1].

theorem TauCeti.Probability.hasFPowerSeriesOnBall_pgf_of_integrable_exp_mul_natCast {ν : MeasureTheory.Measure ℕ} {t : ℝ} (hExp : MeasureTheory.Integrable (fun (k : ℕ) => Real.exp (t * ↑k)) ν) : HasFPowerSeriesOnBall (pgf id ν) (FormalMultilinearSeries.ofScalars ℝ fun (k : ℕ) => ν.real {k}) 0 (ENNReal.ofReal (Real.exp t))

An exponential moment extends the power-series representation of a probability-generating function to the open ball of radius exp t.

theorem TauCeti.Probability.hasFPowerSeriesOnBall_pgf (ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure ν] : HasFPowerSeriesOnBall (pgf id ν) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => ν.real {n}) 0 1

The probability-generating function of a finite measure on ℕ has, at the origin, the formal power series whose coefficients are the singleton masses, and that series converges on the open unit ball.

theorem TauCeti.Probability.integrable_descFactorial_of_integrable_pow_natCast {ν : MeasureTheory.Measure ℕ} {n : ℕ} (h : MeasureTheory.Integrable (fun (k : ℕ) => ↑k ^ n) ν) : MeasureTheory.Integrable (fun (k : ℕ) => ↑(k.descFactorial n)) ν

An integrable nth power of a natural-number-valued function makes its nth falling factorial integrable.

theorem TauCeti.Probability.integrable_descFactorial_of_integrable_exp_mul_natCast {ν : MeasureTheory.Measure ℕ} {t : ℝ} (ht : 0 < t) (hExp : MeasureTheory.Integrable (fun (k : ℕ) => Real.exp (t * ↑k)) ν) (n : ℕ) : MeasureTheory.Integrable (fun (k : ℕ) => ↑(k.descFactorial n)) ν

A positive exponential moment makes every natural falling factorial integrable.

theorem TauCeti.Probability.iteratedDeriv_pgf_one {ν : MeasureTheory.Measure ℕ} {t : ℝ} (ht : 0 < t) (hExp : MeasureTheory.Integrable (fun (k : ℕ) => Real.exp (t * ↑k)) ν) (n : ℕ) : iteratedDeriv n (pgf id ν) 1 = ∫ (k : ℕ), ↑(k.descFactorial n) ∂ν

If a measure on ℕ has a positive exponential moment, then the nth derivative at one of its probability-generating function is its nth factorial moment.

theorem TauCeti.Probability.tendsto_iteratedDeriv_pgf_nhdsLT_one {ν : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure ν] {n : ℕ} (hdesc : MeasureTheory.Integrable (fun (k : ℕ) => ↑(k.descFactorial n)) ν) : Filter.Tendsto (fun (z : ℝ) => iteratedDeriv n (pgf id ν) z) (nhdsWithin 1 (Set.Iio 1)) (nhds (∫ (k : ℕ), ↑(k.descFactorial n) ∂ν))

If a finite measure on ℕ has a finite nth factorial moment, then the nth derivative of its probability-generating function tends to that moment as the argument tends to one from below.

theorem TauCeti.Probability.tendsto_iteratedDeriv_pgf_nhdsLT_one_of_integrable_pow_natCast {ν : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure ν] {n : ℕ} (hn : MeasureTheory.Integrable (fun (k : ℕ) => ↑k ^ n) ν) : Filter.Tendsto (fun (z : ℝ) => iteratedDeriv n (pgf id ν) z) (nhdsWithin 1 (Set.Iio 1)) (nhds (∫ (k : ℕ), ↑(k.descFactorial n) ∂ν))

If a finite measure on ℕ has a finite nth ordinary moment, then the nth derivative of its probability-generating function tends to the nth factorial moment as the argument tends to one from below.

theorem TauCeti.Probability.analyticOnNhd_pgf (ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure ν] : AnalyticOnNhd ℝ (pgf id ν) (Set.Ioo (-1) 1)

The probability-generating function of a finite measure on ℕ is analytic on (-1, 1).

@[simp]

theorem TauCeti.Probability.iteratedDeriv_pgf_zero (ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure ν] (n : ℕ) : iteratedDeriv n (pgf id ν) 0 = ↑n.factorial * ν.real {n}

The Taylor coefficients at the origin of the probability-generating function of a finite measure on ℕ are its singleton masses.

@[simp]

theorem TauCeti.Probability.pgf_zero (ν : MeasureTheory.Measure ℕ) : pgf id ν 0 = ν.real {0}

Evaluating at the origin the probability-generating function of a measure on ℕ gives the real-valued mass ν.real {0}; if ν {0} = ∞ both sides are 0, as ν.real sends infinite mass to zero. For a finite measure this is the n = 0 case of iteratedDeriv_pgf_zero, which simp normalises away from iteratedDeriv.

@[simp]

theorem TauCeti.Probability.deriv_pgf_zero (ν : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure ν] : deriv (pgf id ν) 0 = ν.real {1}

The derivative at the origin of the probability-generating function of a finite measure on ℕ is the mass of {1}. This is the n = 1 case of iteratedDeriv_pgf_zero, which simp normalises away from iteratedDeriv.

theorem TauCeti.Probability.measure_eq_of_pgf_eventuallyEq {ν ν' : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ν'] (h : pgf id ν =ᶠ[nhds 0] pgf id ν') : ν = ν'

A finite measure on ℕ, in particular a probability measure, is determined by the germ at the origin of its probability-generating function.

theorem TauCeti.Probability.measure_eq_of_pgf_eqOn {ν ν' : MeasureTheory.Measure ℕ} [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure ν'] (h : Set.EqOn (pgf id ν) (pgf id ν') (Set.Ioo (-1) 1)) : ν = ν'

A finite measure on ℕ, in particular a probability measure, is determined by its probability-generating function on (-1, 1).

theorem TauCeti.Probability.identDistrib_of_pgf_eventuallyEq {Ω : Type u_1} [MeasurableSpace Ω] {Ω' : Type u_2} [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] {X : Ω → ℕ} {Y : Ω' → ℕ} (hX : AEMeasurable X P) (hY : AEMeasurable Y Q) (h : pgf X P =ᶠ[nhds 0] pgf Y Q) : ProbabilityTheory.IdentDistrib X Y P Q

Two natural-number-valued random variables whose probability-generating functions agree near the origin are identically distributed.

theorem TauCeti.Probability.identDistrib_of_pgf_eqOn {Ω : Type u_1} [MeasurableSpace Ω] {Ω' : Type u_2} [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] {X : Ω → ℕ} {Y : Ω' → ℕ} (hX : AEMeasurable X P) (hY : AEMeasurable Y Q) (h : Set.EqOn (pgf X P) (pgf Y Q) (Set.Ioo (-1) 1)) : ProbabilityTheory.IdentDistrib X Y P Q

Two natural-number-valued random variables whose probability-generating functions agree on (-1, 1) are identically distributed.