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 κ ν
ω : Ω
q : ℚ
h1 : 0 < q
h2 : (↑q : ℝ) ≤ X ω
⊢ 0 < X ω

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

Premises used: Iff.mpr, Rat.cast_pos, lt_of_lt_of_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})

Tactic:
have hs : {ω | 0 < X ω} = ⋃ ε : {ε : ℚ // 0 < ε}, {ω | ε ≤ X ω} := by
    ext ω
    simp only [Set.mem_setOf_eq, Set.mem_iUnion, Subtype.exists, exists_prop]
    constructor
    · intro hp
      obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
      exact ⟨q, (q.cast_pos.1 h1), h2.le⟩
    · intro ⟨q, h1, h2⟩
      exact lt_of_lt_of_le (q.cast_pos.2 h1) h2
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-t * (↑ε : ℝ) + (↑0 : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h₁ :
  IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω') →
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω') →
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
h₁ :
  ∀ (ω' : Ω')
    (hm :
      ∀ (t : ℝ),
        0 ≤ t →
          Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
            rexp (-t * (↑ε : ℝ) + (↑0 : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)),
    IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω') →
      ∀ (hε : 0 < ε),
        Eq (α := ℝ≥0∞)
          ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε

Premises used: Rat.cast, ProbabilityTheory.Kernel.HasSubgaussianMGF.isFiniteMeasure, 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 : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-t * (↑ε : ℝ) + (↑0 : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
⊢ ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))

Tactic:
simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm

Premises used: MulZeroClass.zero_mul, zero_div, NNReal.coe_zero, neg_mul, add_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
this : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} = 0
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simpa [Measure.real, ENNReal.toReal_eq_zero_iff]

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} = 0
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
apply : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ t * (↑ε : ℝ)) Filter.atTop Filter.atTop
⊢ Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)

Tactic:
apply tendsto_exp_neg_atTop_nhds_zero.comp

Premises used: Real.tendsto_exp_neg_atTop_nhds_zero, Filter.Tendsto.comp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
⊢ Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ t * (↑ε : ℝ)) Filter.atTop Filter.atTop

Tactic:
Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)

Premises used: Iff.mpr, Filter.Tendsto.atTop_mul_const, 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 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
⊢ Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ t * (↑ε : ℝ)) Filter.atTop Filter.atTop

Tactic:
exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)

Premises used: Iff.mpr, Filter.Tendsto.atTop_mul_const, 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 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
⊢ Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)

Tactic:
have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) := by
      apply tendsto_exp_neg_atTop_nhds_zero.comp
      exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
hl : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)
h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤ 0
h₂ : 0 ≤ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω}
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} = 0

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
hl : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤ 0

Tactic:
ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)

Premises used: Iff.mpr, ge_of_tendsto, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
hl : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤ 0

Tactic:
exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)

Premises used: Iff.mpr, ge_of_tendsto, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
hl : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)
⊢ 0 ≤ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω}

Tactic:
measureReal_nonneg

Premises used: MeasureTheory.measureReal_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
ε : ℚ
ω' : Ω'
h_1 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
hε : 0 < ε
hm :
  ∀ (t : ℝ),
    0 ≤ t →
      Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤
        rexp (-(t * (↑ε : ℝ)))
hl : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ rexp (-(t * (↑ε : ℝ)))) Filter.atTop (𝓝 0)
⊢ 0 ≤ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω}

Tactic:
exact measureReal_nonneg

Premises used: MeasureTheory.measureReal_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
⊢ ∀ (ε : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      0 < ε →
        Eq (α := ℝ≥0∞)
          ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞)

Tactic:
have hb (ε : ℚ) : ∀ᵐ ω' ∂ν, 0 < ε → (κ ω') {ω | ε ≤ X ω} = 0 := by
    filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε
    simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm
    suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
    have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) := by
      apply tendsto_exp_neg_atTop_nhds_zero.comp
      exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)
    apply le_antisymm
    · exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)
    · exact measureReal_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
hb :
  ∀ (ε : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      0 < ε →
        Eq (α := ℝ≥0∞)
          ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞)
h₁ :
  ∀ (ω' : Ω')
    (hn :
      ∀ (i : ℚ),
        0 < i →
          Eq (α := ℝ≥0∞)
            ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑i : ℝ) ≤ X ω} : ℝ≥0∞)
            (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
filter_upwards [ae_all_iff.2 hb] with ω' hn

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
hb :
  ∀ (ε : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      0 < ε →
        Eq (α := ℝ≥0∞)
          ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞)
ω' : Ω'
hn h₁ :
  ∀ (a : ℚ) (b : 0 < a),
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑a : ℝ) ≤ X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp only [hs, measure_iUnion_null_iff, Subtype.forall]

Premises used: MeasureTheory.measure_iUnion_null_iff, Subtype.forall
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
hb :
  ∀ (ε : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      0 < ε →
        Eq (α := ℝ≥0∞)
          ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞)
ω' : Ω'
hn :
  ∀ (i : ℚ),
    0 < i →
      Eq (α := ℝ≥0∞)
        ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑i : ℝ) ≤ X ω} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (a : ℚ) (b : 0 < a),
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑a : ℝ) ≤ X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
fun _ ↦ hn _
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
hs : Eq.{u_1 + 1} (α := Set Ω) {ω : Ω | 0 < X ω} (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω})
hb :
  ∀ (ε : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      0 < ε →
        Eq (α := ℝ≥0∞)
          ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞)
ω' : Ω'
hn :
  ∀ (i : ℚ),
    0 < i →
      Eq (α := ℝ≥0∞)
        ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑i : ℝ) ≤ X ω} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (a : ℚ) (b : 0 < a),
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑a : ℝ) ≤ X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
exact fun _ ↦ hn _
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
h₁ :
  ∀ (a : Ω'),
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < (-X) ω} : ℝ≥0∞)
        (0 : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
          (0 : ℝ≥0∞) →
        X =ᶠ[ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) a : Measure Ω)] 0
⊢ ∀ᵐ (ω' : Ω') ∂ν, X =ᶠ[ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)] 0

Tactic:
filter_upwards [(h.neg).measure_pos_eq_zero_of_hasSubGaussianMGF_zero,
    h.measure_pos_eq_zero_of_hasSubGaussianMGF_zero]

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_pos_eq_zero_of_hasSubGaussianMGF_zero, ProbabilityTheory.Kernel.HasSubgaussianMGF.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 :
  Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < (-X) ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)
h2 :
  Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp_rw [Pi.neg_apply, Left.neg_pos_iff] at h1

Premises used: Left.neg_pos_iff, Pi.neg_apply
-- 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∞)
h₁ :
  LE.le (α := ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {x : Ω | (fun (x : Ω) ↦ X x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ X =ᶠ[ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)] 0

Tactic:
apply nonpos_iff_eq_zero.1

Premises used: Iff.mp, nonpos_iff_eq_zero
-- 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∞)
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ≠ 0} : ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0 ∨ 0 < X ω} : ℝ≥0∞)

Tactic:
simp_rw [ne_iff_lt_or_gt]

Premises used: ne_iff_lt_or_gt
-- 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∞)
⊢ (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0 ∨ 0 < X ω} ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0} : ℝ≥0∞)
      ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)

Tactic:
measure_union_le _ _

Premises used: Set.union, Set.Mem, setOf, MeasureTheory.measure_union_le
-- 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∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0} : ℝ≥0∞)
      ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞) =
    0

Tactic:
simp [h1, h2]