Probability_Generating_Function_of_Binomial_Distribution
Provedbinomial-distributionprobability-generating-functionsproofwiki
Let X be a discrete random variable with the binomial distribution with parameters n and p. Then the p.g.f. of X is Pi_X(s) = ((1-p) + p*s)^n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Probability_Generating_Function_of_Binomial_Distribution (n : Nat) (p s : Real) (hp : 0 <= p) (hp1 : p <= 1) : Finset.sum (Finset.range (n + 1)) (fun k => (Nat.choose n k : Real) * p ^ k * (1 - p) ^ (n - k) * s ^ k) = ((1 - p) + p * s) ^ n := by sorry
Source