English
If mgf X μ = mgf Y μ' and the corresponding μ, μ' satisfy a nondegeneracy condition, then complexMGF X μ and complexMGF Y μ' agree on the vertical strip {z : Re z ∈ interior (integrableExpSet X μ)}.
Русский
Если mgf X μ = mgf Y μ' и меры не вырождены, то complexMGF X μ и complexMGF Y μ' совпадают на вертикальной полосе {z : Re z ∈ interior (integrableExpSet X μ)}.
LaTeX
$$$hXY:\\ mgf X μ = mgf Y μ' \\Rightarrow \\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 `integrableExpSet`. -/
theorem integrableExpSet_eq_of_mgf [IsProbabilityMeasure μ] (hXY : mgf X μ = mgf Y μ') :
integrableExpSet X μ = integrableExpSet Y μ' :=
by
refine integrableExpSet_eq_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'
