awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)
h1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0} : ℝ≥0∞)
    (0 : ℝ≥0∞)
calc :
  Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ≠ 0} : ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0 ∨ 0 < X ω} : ℝ≥0∞)
calc₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0} : ℝ≥0∞)
      ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞) =
    0
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {x : Ω | (fun (x : Ω) ↦ X x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
calc (κ ω') {ω | X ω ≠ 0}
  _ = (κ ω') {ω | X ω < 0 ∨ 0 < X ω} := by simp_rw [ne_iff_lt_or_gt]
  _ ≤ (κ ω') {ω | X ω < 0} + (κ ω') {ω | 0 < X ω} := measure_union_le _ _
  _ = 0 := by simp [h1, h2]

Premises used: setOf, Ne, LT.lt, Or, OfNat.ofNat, DFunLike.coe, MeasureTheory.measure_union_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ Measurable.{u_1, 0} (α := Ω) (β := ℝ) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
rw : ∀ᵐ (y : Ω') ∂ν, ∀ᵐ (z : Ω) ∂((κ : (a : Ω') → Measure Ω) y : Measure Ω), X z = 0 z
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] 0

Tactic:
rw [Filter.EventuallyEq, Measure.ae_comp_iff (measurableSet_eq_fun hX (by fun_prop))]

Premises used: measurableSet_eq_fun, Filter.EventuallyEq, MeasureTheory.Measure.ae_comp_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (y : Ω') ∂ν, ∀ᵐ (z : Ω) ∂((κ : (a : Ω') → Measure Ω) y : Measure Ω), X z = 0 z

Tactic:
h.ae_eq_zero_of_hasSubgaussianMGF_zero

Premises used: Filter.EventuallyEq, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (y : Ω') ∂ν, ∀ᵐ (z : Ω) ∂((κ : (a : Ω') → Measure Ω) y : Measure Ω), X z = 0 z

Tactic:
exact h.ae_eq_zero_of_hasSubgaussianMGF_zero

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
have hX := h.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hX : AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ HasSubgaussianMGF (AEStronglyMeasurable.mk X hX) 0 κ ν

Tactic:
have h' : HasSubgaussianMGF (hX.mk X) 0 κ ν := h.congr hX.ae_eq_mk
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hX : AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h' : HasSubgaussianMGF (AEStronglyMeasurable.mk X hX) 0 κ ν
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] 0

Tactic:
hX.ae_eq_mk.trans (ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable hX.measurable_mk h')

Premises used: Filter.EventuallyEq.trans, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.measurable_mk, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hX : AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h' : HasSubgaussianMGF (AEStronglyMeasurable.mk X hX) 0 κ ν
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] 0

Tactic:
exact hX.ae_eq_mk.trans (ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable hX.measurable_mk h')

Premises used: Filter.EventuallyEq.trans, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.measurable_mk, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
pos :
  ∀ (hX0 : cX = 0),
    HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
      (HPow.hPow (β := ℕ)
        (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
        2)
      κ ν
neg :
  ∀ (hX0 : ¬cX = 0),
    HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
      (HPow.hPow (β := ℕ)
        (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
        2)
      κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    κ ν

Tactic:
by_cases hX0 : cX = 0
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
pos : ∀ (hX : HasSubgaussianMGF X 0 κ ν), HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cY κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    κ ν

Tactic:
simp only [hX0, NNReal.sqrt_zero, zero_add, NNReal.sq_sqrt] at hX ⊢

Premises used: NNReal.sqrt_zero, zero_add, NNReal.sq_sqrt
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cY κ ν

Tactic:
hY.congr ?_

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
pos : Y =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cY κ ν

Tactic:
refine hY.congr ?_

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0_1 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
ω : Ω
hX0 : X ω = 0 ω
⊢ Y ω = X ω + Y ω

Tactic:
simp [hX0]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = 0 x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ Y x = (fun (ω : Ω) ↦ X ω + Y ω) x) x} x}
      a
h₁ h₂ : ∀ (ω : Ω) (hX0 : X ω = 0 ω), Y ω = X ω + Y ω
⊢ Y =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω

Tactic:
filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
pos :
  ∀ (hY0 : cY = 0),
    HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
      (HPow.hPow (β := ℕ)
        (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
        2)
      κ ν
neg :
  ∀ (hY0 : ¬cY = 0),
    HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
      (HPow.hPow (β := ℕ)
        (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
        2)
      κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    κ ν

Tactic:
by_cases hY0 : cY = 0
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
pos : ∀ (hY : HasSubgaussianMGF Y 0 κ ν), HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cX κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    κ ν

Tactic:
simp only [hY0, NNReal.sqrt_zero, add_zero, NNReal.sq_sqrt] at hY ⊢

Premises used: NNReal.sqrt_zero, add_zero, NNReal.sq_sqrt
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cX κ ν

Tactic:
hX.congr ?_

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
pos : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cX κ ν

Tactic:
refine hX.congr ?_

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0_1 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
ω : Ω
hY0 : Y ω = 0 ω
⊢ X ω = X ω + Y ω

Tactic:
simp [hY0]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ Y x = 0 x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = (fun (ω : Ω) ↦ X ω + Y ω) x) x} x}
      a
h₁ h₂ : ∀ (ω : Ω) (hY0 : Y ω = 0 ω), X ω = X ω + Y ω
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω

Tactic:
filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hY] with ω hY0 using by simp [hY0]

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
t : ℝ
simp_rw : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simp_rw [mul_add, exp_add]

Premises used: mul_add, Real.exp_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
t : ℝ
⊢ @Integrable _ _ _ _ mΩ (HMul.hMul (α := Ω → ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω))
    ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)

Premises used: MeasureTheory.MemLp.integrable_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
t : ℝ
convert! : (↑2 : ℝ≥0∞).HolderTriple (↑2 : ℝ≥0∞) 1
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
t : ℝ
⊢ ENNReal.HolderTriple 2 2 1

Tactic:
infer_instance
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
h :
  ∀ (ω' : Ω')
    (hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (hlX :
      ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω'))
    (hlY :
      ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω'))
    (t : ℝ),
    mgf (m := mΩ) (fun (ω : Ω) ↦ X ω + Y ω) ((κ : (a : Ω') → Measure Ω) ω') t ≤
      rexp
        ((↑(HPow.hPow (β := ℕ)
                  (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
                    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
                  2) :
              ℝ) *
            HPow.hPow (β := ℕ) t 2 /
          2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ) (fun (ω : Ω) ↦ X ω + Y ω) ((κ : (a : Ω') → Measure Ω) ω') t ≤
        rexp
          ((↑(HPow.hPow (β := ℕ)
                    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
                      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
                    2) :
                ℝ) *
              HPow.hPow (β := ℕ) t 2 /
            2)

Tactic:
filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p,
        hY.ae_forall_memLp_exp_mul q] with ω' hmX hmY hlX hlY t

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_memLp_exp_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
simp_rw :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) x) ≤
    HPow.hPow (α := ℝ)
        (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω) ^ (↑p : ℝ)) x)
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ)
        (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * Y ω) ^ (↑q : ℝ)) x)
        (1 / (↑q : ℝ))

Tactic:
simp_rw [mul_add, exp_add]

Premises used: mul_add, Real.exp_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hpq : (↑p : ℝ).HolderConjugate (↑q : ℝ)
hf_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)
hg_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * Y a)
hf : MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * X a)) (ENNReal.ofReal (↑p : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')
hg : MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * Y a)) (ENNReal.ofReal (↑q : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))

Tactic:
apply integral_mul_le_Lp_mul_Lq_of_nonneg

Premises used: MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ (↑p : ℝ)⁻¹ + (↑q : ℝ)⁻¹ = 1⁻¹

Tactic:
simp [field, p, q]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ 0 < (↑p : ℝ)

Tactic:
positivity