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