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