∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    deriv (ProbabilityTheory.mgf X μ) t = ∫ (x : Ω), (fun ω => X ω * Real.exp (t * X ω)) x ∂μ