English
If two real-valued random variables X and Y have the same complex MGFs with respect to finite measures μ and μ', then their integrableExpSets are equal.
Русский
Если две случайные величины X, Y имеют одинаковые комплексные MGФ относительно конечных мер μ, μ', то их интегрируемые экспоненциальные множества совпадают.
LaTeX
$$$(\\mgf X μ) = (\\mgf Y μ') \\Rightarrow (\\mathrm{integrableExpSet}(X, μ) = \\mathrm{integrableExpSet}(Y, μ'))$$$
Lean4
/-- If two random variables have the same moment-generating function then they have
the same `integrableExpSet`. -/
theorem integrableExpSet_eq_of_mgf' (hXY : mgf X μ = mgf Y μ') (hμμ' : μ = 0 ↔ μ' = 0) :
integrableExpSet X μ = integrableExpSet Y μ' := by
ext t
simp only [integrableExpSet, Set.mem_setOf_eq]
by_cases hμ : μ = 0
· simp [hμ, hμμ'.mp hμ]
have : NeZero μ := ⟨hμ⟩
have : NeZero μ' := ⟨(not_iff_not.mpr hμμ').mp hμ⟩
rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]
