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. Finally it computes the generating functions of the standard discrete families: Bernoulli, binomial, Poisson, and geometric, the last one on its exact integrability domain.

These results implement the definition, the generic API, the coefficient-recovery and uniqueness statements, and the distribution-specific formulas of the probability-generating-function target in TauCetiRoadmap/StandardDistributions/README.md, Layer 1.

The Poisson series calculation follows the proof pattern of Mathlib's ProbabilityTheory.charFun_map_cast_poissonMeasure: both factor the Poisson weights out of the exponential power series. The Bernoulli, binomial, and geometric calculations use Mathlib's corresponding measure-integral formulas directly.

Main declarations

• TauCeti.Probability.pgf — the probability-generating function.
• TauCeti.Probability.pgf_exp — evaluation at exp t is a moment-generating function.
• 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_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).
• TauCeti.Probability.pgf_bernoulliMeasure, pgf_binomial, pgf_poissonMeasure, and pgf_geometricMeasure — the standard discrete-family formulas.

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 μ.

Equations

• TauCeti.Probability.pgf X μ t = ∫ (ω : Ω), t ^ X ω ∂μ

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.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 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 ℕ) [SFinite μ] [SFinite ν] (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 (ν : 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 (ν : 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.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 ℕ) [MeasureTheory.IsFiniteMeasure ν] : pgf id ν 0 = ν.real {0}

Evaluating at the origin the probability-generating function of a finite measure on ℕ gives the mass of {0}. 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.

theorem TauCeti.Probability.pgf_bernoulliMeasure (p : ↑unitInterval) (t : ℝ) : pgf id (ProbabilityTheory.bernoulliMeasure 1 0 p) t = 1 - ↑p + ↑p * t

The probability-generating function of a Bernoulli distribution.

theorem TauCeti.Probability.pgf_binomial (n : ℕ) (p : ↑unitInterval) (t : ℝ) : pgf id (ProbabilityTheory.binomial n p) t = (1 - ↑p + ↑p * t) ^ n

The probability-generating function of a binomial distribution.

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.pgf_geometricMeasure_zero (t : ℝ) : pgf id (ProbabilityTheory.geometricMeasure 0) t = 1

At the zero parameter, Mathlib's geometric distribution is a Dirac mass at zero, so its probability-generating function is identically one.

theorem TauCeti.Probability.integrable_pow_geometricMeasure_iff {p : ↑unitInterval} (hp : p ≠ 0) (t : ℝ) : MeasureTheory.Integrable (fun (n : ℕ) => t ^ n) (ProbabilityTheory.geometricMeasure p) ↔ |(1 - ↑p) * t| < 1

For a nonzero success probability, the geometric probability-generating-function integrand is integrable exactly on the open interval determined by the geometric-series ratio.

theorem TauCeti.Probability.pgf_geometricMeasure {p : ↑unitInterval} (hp : p ≠ 0) {t : ℝ} (ht : |(1 - ↑p) * t| < 1) : pgf id (ProbabilityTheory.geometricMeasure p) t = ↑p / (1 - (1 - ↑p) * t)

The probability-generating function of a geometric distribution with nonzero parameter, on its exact integrability domain. The boundary case p = 1, whose law is a Dirac mass at zero, is included.