Probability_Generating_Function_of_Discrete_Uniform_Distribution
Proveddiscrete-uniform-distributionprobability-generating-functionsproofwiki
Let X be a discrete random variable with the discrete uniform distribution with parameter n. Then the p.g.f. of X is Pi_X(s) = s*(1 - s^n) / (n*(1 - s)).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Probability_Generating_Function_of_Discrete_Uniform_Distribution (n : Nat) (hn : 0 < n) (s : Real) (hs : s != 1) : Finset.sum (Finset.range n) (fun k => (1 / (n : Real)) * s ^ (k + 1)) = s * (1 - s ^ n) / ((n : Real) * (1 - s)) := by sorry
Source