∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    HasFPowerSeriesAt (ProbabilityTheory.mgf X μ)
      (FormalMultilinearSeries.ofScalars ℝ fun n =>
        (∫ (x : Ω), (fun ω => X ω ^ n * Real.exp (v * X ω)) x ∂μ) / ↑n.factorial)
      v