Def ProbabilityTheory.complexMGF

Modification history

2026-03-03 17:12
Mathlib/Probability/Moments/ComplexMGF.lean
feat: taylor expansion of the characteristic function (#36025) …
Modified ProbabilityTheory.complexMGFView on Github →
2025-01-29 06:49
Mathlib/Probability/Moments/ComplexMGF.lean
feat: the moment generating function is analytic (#20151) …
Added ProbabilityTheory.complexMGFView on Github →