English
For HasSubgaussianMGF, for any p in NNReal, almost surely exp(t X) lies in L^p with respect to the kernel for all t.
Русский
Для любого p из NNReal почти наверняка exp(t X) лежит в L^p по κ ω' для всех t.
LaTeX
$$$\\forall p\\,\\text{NNReal},\\ \\forall\\omega'\\,\\nu,\\ ∀t,\\ MemLp(\\lambda \\omega: e^{t X(\\omega)})\, (\\ENNReal.ofNNReal p)\, (\\kappa(\\omega')).$$$
Lean4
theorem memLp_exp_mul (h : HasSubgaussianMGF X c κ ν) (t : ℝ) (p : ℝ≥0) : MemLp (fun ω ↦ exp (t * X ω)) p (κ ∘ₘ ν) :=
by
by_cases hp0 : p = 0
· simpa [hp0] using (h.integrable_exp_mul t).1
constructor
· exact (h.integrable_exp_mul t).1
· rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp)]
simp only [ENNReal.coe_toReal]
have h' := (h.integrable_exp_mul (p * t)).2
rw [hasFiniteIntegral_def] at h'
convert h' using 3 with ω
rw [enorm_eq_ofReal (by positivity), enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
← exp_mul, mul_comm, ← mul_assoc]
positivity
