Probability_Generating_Function_of_Bernoulli_Distribution
Provedbernoulli-distributionprobability-generating-functionsproofwiki
Let X be a discrete random variable with the Bernoulli distribution with parameter p. Then the p.g.f. of X is Pi_X(s) = (1-p) + p*s.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Probability_Generating_Function_of_Bernoulli_Distribution (p s : Real) (hp : 0 <= p) (hp1 : p <= 1) : (1 - p) + p * s = (1 - p) + p * s := by sorry
Source