English
The constant zero function has subgaussian MGF with c=0; all required integrability conditions hold trivially.
Русский
Постоянно нулевая функция имеет субгауссов MGФ нулевого параметра с условием интегрируемости выполняется тривиально.
LaTeX
$$$\\text{HasSubgaussianMGF}(0,0,\\kappa,\\nu).$$$
Lean4
protected theorem of_rat (h_int : ∀ t : ℝ, Integrable (fun ω ↦ exp (t * X ω)) (κ ∘ₘ ν))
(h_mgf : ∀ q : ℚ, ∀ᵐ ω' ∂ν, mgf X (κ ω') q ≤ exp (c * q ^ 2 / 2)) : Kernel.HasSubgaussianMGF X c κ ν
where
integrable_exp_mul := h_int
mgf_le := by
rw [← ae_all_iff] at h_mgf
have h_int : ∀ᵐ ω' ∂ν, ∀ t, Integrable (fun ω ↦ exp (t * X ω)) (κ ω') :=
by
have h_int' (n : ℤ) := Measure.ae_integrable_of_integrable_comp (h_int n)
rw [← ae_all_iff] at h_int'
filter_upwards [h_int'] with ω' h_int t
exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)
filter_upwards [h_mgf, h_int] with ω' h_mgf h_int t
refine Rat.denseRange_cast.induction_on t ?_ h_mgf
exact isClosed_le (continuous_mgf h_int) (by fun_prop)
