LeanMachineLearning exposition

ProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul_sub🔗

Minimal Lean file

memLp_exp_mul_sub🔗

LemmaProbabilityTheory.HasCondSubgaussianMGF.memLp_exp_mul_sub
Details

No docstring.

🔗theorem
ProbabilityTheory.HasCondSubgaussianMGF.memLp_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 : ℝ) (p : NNReal) :
  MeasureTheory.MemLp (fun ω => Real.exp (t * X ω - ↑c * t ^ 2 / 2))
    (↑p) μ
ProbabilityTheory.HasCondSubgaussianMGF.memLp_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 : ℝ) (p : NNReal) :
  MeasureTheory.MemLp
    (fun ω =>
      Real.exp (t * X ω - ↑c * t ^ 2 / 2))
    (↑p) μ

Code

lemma memLp_exp_mul_sub (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) (p : ℝ≥0) :
    MemLp (fun ω ↦ exp (t * X ω - c * t ^ 2 / 2)) p μ

Actions: Source · Open Issue

Proof
by
  have h_lp := h.memLp_exp_mul t p
  simp_rw [sub_eq_add_neg, exp_add]
  exact h_lp.mul_const _