noncomputable def momentGeneratingFunction {Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) (t : ℝ) : ℝ

Moment generating function (Lecture 8): for a real-valued random variable X with law μ, the moment generating function is M_X(t) = E[e^{tX}], defined here as the Bochner integral ∫ exp (t · X ω) ∂μ.