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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * r * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
exact h.integrable_exp_mul (t * r)

Premises used: HMul.hMul, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
h₁ :
  ∀ (ω : Ω')
    (hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (t : ℝ),
    mgf (m := mΩ) (fun (ω : Ω) ↦ r * X ω) ((κ : (a : Ω') → Measure Ω) ω) t ≤
      rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ) (fun (ω : Ω) ↦ r * X ω) ((κ : (a : Ω') → Measure Ω) ω') t ≤
        rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
filter_upwards [h.mgf_le] with ω hω t

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
h₁ :
  mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) (t * r) ≤
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf (m := mΩ) (fun (ω : Ω) ↦ r * X ω) ((κ : (a : Ω') → Measure Ω) ω) t ≤
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [mgf_const_mul, mul_comm]

Premises used: mul_comm, ProbabilityTheory.mgf_const_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) (t * r) ≤
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
(hω (t * r)).trans_eq ?_

Premises used: HMul.hMul, LE.le.trans_eq
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
h₁ :
  rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2) =
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) (t * r) ≤
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
refine (hω (t * r)).trans_eq ?_

Premises used: HMul.hMul, LE.le.trans_eq
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
h₁ :
  (↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2 =
    (↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2) =
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
congr 1
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
⊢ (↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2 = HPow.hPow (β := ℕ) r 2 * (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
ring
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h₁ :
  IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω') →
    ∀ (t : ℝ),
      0 ≤ t →
        Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
          rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω') →
    ∀ (t : ℝ),
      0 ≤ t →
        Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
          rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
_
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
h₁ :
  ∀ (ω' : Ω')
    (h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')),
    IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω') →
      ∀ (t : ℝ) (ht : 0 ≤ t),
        Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
          rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      0 ≤ t →
        Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
          rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul, h.isFiniteMeasure] with ω' h1 h2 _ t ht

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.isFiniteMeasure, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
ht : 0 ≤ t
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
    rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t

Tactic:
measure_ge_le_exp_mul_mgf ε ht (h2 t)

Premises used: ProbabilityTheory.measure_ge_le_exp_mul_mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
ht : 0 ≤ t
rw :
  rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp (-t * ε) * rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
ht : 0 ≤ t
hbc : mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp (-t * ε) * rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
ht : 0 ≤ t
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h1 t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
ht : 0 ≤ t
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact h1 t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h2 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
ht : 0 ≤ t
calc :
  rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
    rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
calc (κ ω').real {ω | ε ≤ X ω}
  _ ≤ exp (-t * ε) * mgf X (κ ω') t := measure_ge_le_exp_mul_mgf ε ht (h2 t)
  _ ≤ exp (-t * ε + c * t ^ 2 / 2) := by
    rw [exp_add]
    gcongr
    exact h1 t

Premises used: HMul.hMul, setOf, MeasureTheory.Measure.real, HDiv.hDiv, LE.le, Real.exp, HPow.hPow, HAdd.hAdd, ProbabilityTheory.measure_ge_le_exp_mul_mgf, ProbabilityTheory.mgf, OfNat.ofNat, DFunLike.coe, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
pos :
  ∀ (hc0 : c = 0),
    ∀ᵐ (ω' : Ω') ∂ν,
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
        rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
neg :
  ∀ (hc0 : ¬c = 0),
    ∀ᵐ (ω' : Ω') ∂ν,
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
        rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
by_cases hc0 : c = 0
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
h₁ :
  ∀ (ω' : Ω')
    (h :
      LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞)
        (1 : ℝ≥0∞)),
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
filter_upwards [h.measure_univ_le_one] with ω' h

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_univ_le_one
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤ 1
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
simp only [hc0, NNReal.coe_zero, mul_zero, div_zero, exp_zero]

Premises used: NNReal.coe_zero, MulZeroClass.mul_zero, Real.exp_zero, div_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤ 1

Tactic:
ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Premises used: MeasureTheory.Measure.real, zero_le_one, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
h₁ : (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} ≤ ENNReal.ofReal 1
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤ 1

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Premises used: zero_le_one, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
h₁ :
  LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} : ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} ≤ ENNReal.ofReal 1

Tactic:
simp only [ENNReal.ofReal_one]

Premises used: ENNReal.ofReal_one
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
(measure_mono (Set.subset_univ _)).trans h

Premises used: Set.subset_univ, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
ω' : Ω'
h : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
exact (measure_mono (Set.subset_univ _)).trans h

Premises used: Set.subset_univ, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
h₁ :
  ∀ (ω' : Ω')
    (h :
      ∀ (t : ℝ),
        0 ≤ t →
          Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
            rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)),
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
filter_upwards [measure_ge_le_exp_add h ε] with ω' h

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le_exp_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
        rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ 0 ≤ ε / (↑c : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
        rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
e_x :
  -(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2 = -HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ))
⊢ rexp (-(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2) =
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
        rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ -(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2 = -HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ))

Tactic:
field
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
        rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
calc :
  rexp (-(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2) =
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
calc (κ ω').real {ω | ε ≤ X ω}
  -- choose the minimizer of the r.h.s. of `h` for `t ≥ 0`. That is, `t = ε / c`.
  _ ≤ exp (-(ε / c) * ε + c * (ε / c) ^ 2 / 2) := h (ε / c) (by positivity)
  _ = exp (- ε ^ 2 / (2 * c)) := by congr; field

Premises used: HMul.hMul, setOf, MeasureTheory.Measure.real, HDiv.hDiv, LE.le, Real.exp, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
h₁ :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | 0 < X ω} ω ↔
      Membership.mem (γ := Set Ω) (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω}) ω
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})

Tactic:
ext ω
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
h₁ : 0 < X ω ↔ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | 0 < X ω} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω}) ω

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_iUnion, Subtype.exists, exists_prop]

Premises used: Set.mem_iUnion, Subtype.exists, Set.mem_setOf_eq, exists_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
h₁ : 0 < X ω → ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
h₂ : (∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω) → 0 < X ω
⊢ 0 < X ω ↔ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
hp : 0 < X ω
h₁ : ∀ (q : ℚ) (h1 : LT.lt (α := ℝ) 0 (↑q : ℝ)) (h2 : (↑q : ℝ) < X ω), ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
⊢ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω

Tactic:
obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp

Premises used: exists_rat_btwn
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
hp : 0 < X ω
q : ℚ
h1 : LT.lt (α := ℝ) 0 (↑q : ℝ)
h2 : (↑q : ℝ) < X ω
⊢ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω

Tactic:
⟨q, (q.cast_pos.1 h1), h2.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro, Iff.mp, Rat.cast_pos
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
hp : 0 < X ω
q : ℚ
h1 : LT.lt (α := ℝ) 0 (↑q : ℝ)
h2 : (↑q : ℝ) < X ω
⊢ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω

Tactic:
exact ⟨q, (q.cast_pos.1 h1), h2.le⟩
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
q : ℚ
h1 : 0 < q
h2 : (↑q : ℝ) ≤ X ω
⊢ 0 < X ω

Tactic:
lt_of_lt_of_le (q.cast_pos.2 h1) h2

Premises used: Iff.mpr, Rat.cast_pos, lt_of_lt_of_le