Theorem ProbabilityTheory.deriv_mgf

Modification history

2025-01-29 06:49

Mathlib/Probability/Moments/MGFAnalytic.lean

feat: the moment generating function is analytic (#20151) …

Added ProbabilityTheory.deriv_mgf View on Github →