English
If h is HasSubgaussianMGF, then for every p>0, and almost every ω', exp(t X(·)) belongs to L^p with respect to κ ω' for all real t.
Русский
Пусть h имеет субгауссов MGФ; тогда для каждого p>0 и почти каждого ω' функция exp(t X(·)) принадлежит L^p по κ ω' для всех t.
LaTeX
$$$\\forall \\omega'\\, \\nu,\\ ∀p>0,\\ MemLp(\\lambda \\omega: e^{t X(\\omega)})\\, p\\, (\\kappa(\\omega')).$$$
Lean4
theorem ae_forall_memLp_exp_mul (h : HasSubgaussianMGF X c κ ν) (p : ℝ≥0) :
∀ᵐ ω' ∂ν, ∀ t, MemLp (fun ω ↦ exp (t * X ω)) p (κ ω') :=
by
filter_upwards [h.ae_forall_integrable_exp_mul] with ω' hi t
constructor
· exact (hi t).1
· by_cases hp : p = 0
· simp [hp]
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp), ENNReal.coe_toReal]
have hf := (hi (p * t)).lintegral_lt_top
convert hf using 3 with ω
rw [enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity), ← exp_mul, mul_comm, ←
mul_assoc]
positivity
