English
If X and Y are a.e.-equal under the kernel, then HasSubgaussianMGF X c κ ν holds iff HasSubgaussianMGF Y c κ ν.
Русский
Если X и Y равны почти повсеместно относительно ядра, то HasSubgaussianMGF X и HasSubgaussianMGF Y эквивалентны.
LaTeX
$$$(\\nu.bind(\\kappa).ae)\\;\\Rightarrow\\; \\mathrm{HasSubgaussianMGF}(X,c,\\kappa,\\nu) \\iff \\mathrm{HasSubgaussianMGF}(Y,c,\\kappa,\\nu).$$$
Lean4
theorem congr {Y : Ω → ℝ} (h : HasSubgaussianMGF X c κ ν) (h' : X =ᵐ[κ ∘ₘ ν] Y) : HasSubgaussianMGF Y c κ ν
where
integrable_exp_mul
t := by
refine (integrable_congr ?_).mpr (h.integrable_exp_mul t)
filter_upwards [h'] with ω hω using by rw [hω]
mgf_le := by
have h'' := Measure.ae_ae_of_ae_comp h'
filter_upwards [h.mgf_le, h''] with ω' h_mgf h' t
rw [mgf_congr (Filter.EventuallyEq.symm h')]
exact h_mgf t
