The moment-generating function is analytic

The moment-generating function mgf X μ of a random variable X with respect to a measure μ is analytic on the interior of integrableExpSet X μ, the interval on which it is defined.

Main results

• analyticOn_mgf: the moment-generating function is analytic on the interior of the interval on which it is defined.

• iteratedDeriv_mgf: the n-th derivative of the mgf at t is μ[X ^ n * exp (t * X)].

• analyticOn_cgf: the cumulant-generating function is analytic on the interior of the interval integrableExpSet X μ.

theorem ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) : HasDerivAt (fun (t : ℝ) => ∫ (x : Ω), (fun (ω : Ω) => X ω ^ n * Real.exp (t * X ω)) x ∂μ) (∫ (x : Ω), (fun (ω : Ω) => X ω ^ (n + 1) * Real.exp (t * X ω)) x ∂μ) t

For t : ℝ with t ∈ interior (integrableExpSet X μ), the derivative of the function x ↦ μ[X ^ n * exp (x * X)] at t is μ[X ^ (n + 1) * exp (t * X)].

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

For t ∈ interior (integrableExpSet X μ), the derivative of mgf X μ at t is μ[X * exp (t * X)].

theorem ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) : HasDerivAt (iteratedDeriv n (mgf X μ)) (∫ (x : Ω), (fun (ω : Ω) => X ω ^ (n + 1) * Real.exp (t * X ω)) x ∂μ) t

theorem ProbabilityTheory.iteratedDeriv_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun (ω : Ω) => X ω ^ n * Real.exp (t * X ω)) x ∂μ

For t ∈ interior (integrableExpSet X μ), the n-th derivative of mgf X μ at t is μ[X ^ n * exp (t * X)].

theorem ProbabilityTheory.iteratedDeriv_mgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) : iteratedDeriv n (mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ

The derivatives of the moment-generating function at zero are the moments.

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

For t ∈ interior (integrableExpSet X μ), the derivative of mgf X μ at t is μ[X * exp (t * X)].

theorem ProbabilityTheory.deriv_mgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) : deriv (mgf X μ) 0 = ∫ (x : Ω), X x ∂μ

theorem ProbabilityTheory.analyticAt_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) : AnalyticAt ℝ (mgf X μ) t

The moment-generating function is analytic at every t ∈ interior (integrableExpSet X μ).

theorem ProbabilityTheory.analyticOnNhd_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOnNhd ℝ (mgf X μ) (interior (integrableExpSet X μ))

theorem ProbabilityTheory.analyticOn_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOn ℝ (mgf X μ) (interior (integrableExpSet X μ))

The moment-generating function is analytic on the interior of the interval on which it is defined.

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

theorem ProbabilityTheory.differentiableAt_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} (ht : t ∈ interior (integrableExpSet X μ)) : DifferentiableAt ℝ (mgf X μ) t

theorem ProbabilityTheory.differentiableOn_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : DifferentiableOn ℝ (mgf X μ) (interior (integrableExpSet X μ))

theorem ProbabilityTheory.continuousOn_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : ContinuousOn (mgf X μ) (interior (integrableExpSet X μ))

theorem ProbabilityTheory.continuous_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : ∀ (t : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : Continuous (mgf X μ)

theorem ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (n : ℕ) : AnalyticOnNhd ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

theorem ProbabilityTheory.analyticOn_iteratedDeriv_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (n : ℕ) : AnalyticOn ℝ (iteratedDeriv n (mgf X μ)) (interior (integrableExpSet X μ))

theorem ProbabilityTheory.analyticAt_iteratedDeriv_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) : AnalyticAt ℝ (iteratedDeriv n (mgf X μ)) v

theorem ProbabilityTheory.differentiableAt_iteratedDeriv_mgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) : DifferentiableAt ℝ (iteratedDeriv n (mgf X μ)) v

theorem ProbabilityTheory.analyticAt_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (h : v ∈ interior (integrableExpSet X μ)) : AnalyticAt ℝ (cgf X μ) v

theorem ProbabilityTheory.analyticOnNhd_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOnNhd ℝ (cgf X μ) (interior (integrableExpSet X μ))

theorem ProbabilityTheory.analyticOn_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} : AnalyticOn ℝ (cgf X μ) (interior (integrableExpSet X μ))

The cumulant-generating function is analytic on the interior of the interval integrableExpSet X μ.

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

theorem ProbabilityTheory.deriv_cgf_zero {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : 0 ∈ interior (integrableExpSet X μ)) : deriv (cgf X μ) 0 = (∫ (x : Ω), X x ∂μ) / μ.real Set.univ

theorem ProbabilityTheory.iteratedDeriv_two_cgf {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (h : v ∈ interior (integrableExpSet X μ)) : iteratedDeriv 2 (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) => X ω ^ 2 * Real.exp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

theorem ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ} (h : v ∈ interior (integrableExpSet X μ)) : iteratedDeriv 2 (cgf X μ) v = (∫ (x : Ω), (fun (ω : Ω) => (X ω - deriv (cgf X μ) v) ^ 2 * Real.exp (v * X ω)) x ∂μ) / mgf X μ v

theorem ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (ht : 0 < t) (hc : ∫ (x : Ω), X x ∂μ = 0) (hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)) : ∃ u ∈ Set.Ioo 0 t, cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2