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 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 < (↑q : ℝ)

Tactic:
positivity
-- 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 : ℝ).HolderConjugate (↑q : ℝ)

Tactic:
exact ⟨by simp [field, p, q], by positivity, by positivity⟩
-- 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 : ℝ
⊢ (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)

Tactic:
ae_of_all _ fun _ ↦ exp_nonneg _

Premises used: HMul.hMul, MeasureTheory.ae_of_all, Real.exp_nonneg, Filter.EventuallyLE
-- 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 : ℝ
⊢ (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)

Tactic:
exact ae_of_all _ fun _ ↦ exp_nonneg _

Premises used: MeasureTheory.ae_of_all, Real.exp_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 : ℝ
⊢ (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * Y a)

Tactic:
ae_of_all _ fun _ ↦ exp_nonneg _

Premises used: HMul.hMul, MeasureTheory.ae_of_all, Real.exp_nonneg, Filter.EventuallyLE
-- 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 : ℝ
⊢ (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * Y a)

Tactic:
exact ae_of_all _ fun _ ↦ exp_nonneg _

Premises used: MeasureTheory.ae_of_all, Real.exp_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 : ℝ
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * X a)) (ENNReal.ofReal (↑p : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
simpa using (hlX t)
-- 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 : ℝ
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * Y a)) (ENNReal.ofReal (↑q : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
simpa using (hlY t)
-- 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 :
  HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x))
        (1 / (↑q : ℝ)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ))
⊢ 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 : ℝ)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ))

Tactic:
simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]

Premises used: Real.exp_mul, mul_right_comm, NNReal.toReal
-- 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 : ℝ
h₁ :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2)
h₂ :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x)) ≤
    rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2)
⊢ HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x))
        (1 / (↑q : ℝ)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ))

Tactic:
gcongr
-- 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 : ℝ
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2)

Tactic:
hmX (t * p)

Premises used: HMul.hMul, ProbabilityTheory.mgf, NNReal.toReal
-- 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 : ℝ
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2)

Tactic:
exact hmX (t * p)

Premises used: HMul.hMul, NNReal.toReal
-- 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 : ℝ
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x)) ≤
    rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2)

Tactic:
hmY (t * q)

Premises used: HMul.hMul, ProbabilityTheory.mgf, NNReal.toReal
-- 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 : ℝ
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x)) ≤
    rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2)

Tactic:
exact hmY (t * q)

Premises used: HMul.hMul, NNReal.toReal
-- 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 :
  rexp
      ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2 * (1 / (↑p : ℝ)) +
        (↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2 * (1 / (↑q : ℝ))) =
    rexp
      (HPow.hPow (β := ℕ) ((↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX) : ℝ) + (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY) : ℝ))
            2 *
          HPow.hPow (β := ℕ) t 2 /
        2)
⊢ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ)) =
    rexp
      (HPow.hPow (β := ℕ) ((↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX) : ℝ) + (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY) : ℝ))
            2 *
          HPow.hPow (β := ℕ) t 2 /
        2)

Tactic:
simp_rw [← exp_mul, ← exp_add]

Premises used: Real.exp_mul, Real.exp_add