English
If two random variables have the same mgf, then their complexMGF agree on the vertical strip given by Re z in interior (integrableExpSet X μ).
Русский
Если две случайные величины имеют одинаковый mgf, то их комплексные MGФ совпадают на вертикальной полосе, задаваемой Re z ∈ interior (integrableExpSet X μ).
LaTeX
$$$\\text{Set.EqOn}(\\text{complexMGF}(X, μ), \\text{complexMGF}(Y, μ'))(\\{ z \\mid \\Re z \\in \\operatorname{Int}(\\mathrm{integrableExpSet}(X, μ))\\})$$$
Lean4
/-- If two random variables have the same moment-generating function then they have
the same `complexMGF` on the vertical strip `{z | z.re ∈ interior (integrableExpSet X μ)}`. -/
theorem eqOn_complexMGF_of_mgf [IsProbabilityMeasure μ] (hXY : mgf X μ = mgf Y μ') :
Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet X μ)} :=
by
refine eqOn_complexMGF_of_mgf' hXY ?_
simp only [IsProbabilityMeasure.ne_zero, false_iff]
suffices mgf Y μ' 0 ≠ 0 by
intro h_contra
simp [h_contra] at this
rw [← hXY]
exact (mgf_pos (by simp)).ne'
