LeanMachineLearning exposition

ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_sub🔗

Minimal Lean file

integrable_exp_mul_sub🔗

LemmaProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_sub
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_sub.{u_1}
  {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ}
  [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal}
  (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
  MeasureTheory.Integrable
    (fun ω => Real.exp (t * X ω - ↑c * t ^ 2 / 2)) μ
ProbabilityTheory.HasCondSubgaussianMGF.integrable_exp_mul_sub.{u_1}
  {Ω : Type u_1}
  {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ}
  [StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  {X : Ω → ℝ} {c : NNReal}
  (h : HasCondSubgaussianMGF m hm X c μ)
  (t : ℝ) :
  MeasureTheory.Integrable
    (fun ω =>
      Real.exp (t * X ω - ↑c * t ^ 2 / 2))
    μ

Code

lemma integrable_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
    Integrable (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) μ

Actions: Source · Open Issue

Proof
by
  have h_int := h.integrable_exp_mul t
  simp_rw [exp_sub]
  exact h_int.div_const _