Probability_Generating_Function_of_Degenerate_Distribution
Proveddegenerate-distributionprobability-generating-functionsproofwiki
Let X be the degenerate distribution concentrated at k in N. Then the probability generating function of X is Pi_X(s) = s^k.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Probability_Generating_Function_of_Degenerate_Distribution (k : Nat) (s : Real) : s ^ k = s ^ k := by sorry
Source