Basic facts about moment-generating functions

This file supplements Mathlib's basic moment-generating-function API.

Main results

• TauCeti.isProbabilityMeasure_of_mgf_zero_eq_one: a measure is a probability measure if the moment-generating function of any real-valued statistic equals 1 at zero.
• TauCeti.isFiniteMeasure_of_zero_mem_integrableExpSet: a measure with an exponential moment at 0 is finite.
• TauCeti.mgf_id_conv: the moment-generating function of a convolution of two s-finite measures on ℝ is the product of their moment-generating functions. This is the transform side of MeasureTheory.Measure.conv, the companion of MeasureTheory.charFun_conv.

theorem TauCeti.isProbabilityMeasure_of_mgf_zero_eq_one {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hmgf : ProbabilityTheory.mgf X μ 0 = 1) : MeasureTheory.IsProbabilityMeasure μ

A measure is a probability measure if the moment-generating function of any real-valued statistic equals 1 at zero.

theorem TauCeti.isFiniteMeasure_of_zero_mem_integrableExpSet {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (h : 0 ∈ ProbabilityTheory.integrableExpSet X μ) : MeasureTheory.IsFiniteMeasure μ

A measure admitting an exponential moment at rate 0 is finite: at rate 0 the integrand is the constant 1, whose integrability is finiteness of the measure.

@[simp]

theorem TauCeti.mgf_id_conv {μ ν : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] : ProbabilityTheory.mgf id (μ.conv ν) = ProbabilityTheory.mgf id μ * ProbabilityTheory.mgf id ν

The moment-generating function of a convolution is the product of the two moment-generating functions. This is the transform companion of MeasureTheory.charFun_conv. No integrability hypothesis is needed, even though Mathlib totalizes a divergent mgf to 0.