English
If mgf X μ = mgf Y μ' and the nondegeneracy condition holds, then the complex MGFs are equal on the vertical strip and the equality is preserved by restricting to that strip.
Русский
Если mgf X μ = mgf Y μ' и условие не вырождности выполняется, то комплексные MGФ совпадают на вертикальной полосе и сохранение равенства продолжается при ограничении до полосы.
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 μ)}`.
TODO: once we know that equal `mgf` implies equal distributions, we will be able to show that
the `complexMGF` are equal everywhere, not only on the strip.
This lemma will be used in the proof of the equality of distributions. -/
theorem eqOn_complexMGF_of_mgf' (hXY : mgf X μ = mgf Y μ') (hμμ' : μ = 0 ↔ μ' = 0) :
Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet X μ)} :=
by
by_cases h_empty : interior (integrableExpSet X μ) = ∅
· simp [h_empty]
rw [← ne_eq, ← Set.nonempty_iff_ne_empty] at h_empty
obtain ⟨t, ht⟩ := h_empty
have hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} := analyticOnNhd_complexMGF
have hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')} := analyticOnNhd_complexMGF
rw [integrableExpSet_eq_of_mgf' hXY hμμ'] at hX ht ⊢
refine
AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq hX hY
(convex_integrableExpSet.interior.linear_preimage reLm).isPreconnected (z₀ := (t : ℂ)) (by simp [ht]) ?_
have h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ x = complexMGF Y μ' x :=
by
refine .of_forall fun y ↦ ?_
rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
rw [frequently_iff_seq_forall] at h_real ⊢
obtain ⟨xs, hx_tendsto, hx_eq⟩ := h_real
refine ⟨fun n ↦ xs n, ?_, fun n ↦ ?_⟩
· rw [tendsto_nhdsWithin_iff] at hx_tendsto ⊢
constructor
· rw [tendsto_ofReal_iff]
exact hx_tendsto.1
· simpa using hx_tendsto.2
· simp [hx_eq]
