awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have calc : rexp (-(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2) =
  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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ω})
have h₁ : ∀ (ω : Ω),
  Membership.mem (γ := Set Ω) {ω : Ω | 0 < X ω} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω}) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | 0 < X ω} ω ↔
    Membership.mem (γ := Set Ω) (⋃ (ε : { ε : ℚ // 0 < ε }), {ω : Ω | (↑(↑ε : ℚ) : ℝ) ≤ X ω}) ω
have h₁ : 0 < X ω ↔ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
Tactic: simp only [Set.mem_setOf_eq, Set.mem_iUnion, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ 0 < X ω ↔ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
have h₁ : 0 < X ω → ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ω
⊢ 0 < X ω ↔ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
have h₂ : (∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω) → 0 < X ω
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
hp : 0 < X ω
⊢ ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
have h₁ : ∀ (q : ℚ) (h1 : LT.lt (α := ℝ) 0 (↑q : ℝ)) (h2 : (↑q : ℝ) < X ω), ∃ (a : ℚ), 0 < a ∧ (↑a : ℝ) ≤ X ω
Tactic: obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)
have hs : 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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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∞)
have 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∞)
Tactic: filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 < ε
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)
have hm₁ : ∀ (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
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 * (↑ε : ℝ)))
⊢ Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ X ω} : ℝ≥0∞)
    (0 : ℝ≥0∞)
have h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} = 0
Tactic: suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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)
have apply : Filter.Tendsto (β := ℝ) (fun (t : ℝ) ↦ t * (↑ε : ℝ)) Filter.atTop Filter.atTop
Tactic: apply tendsto_exp_neg_atTop_nhds_zero.comp
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 * (↑ε : ℝ)))
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} = 0
have hl : 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)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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
have h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} ≤ 0
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω} = 0
have h₂ : 0 ≤ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | (↑ε : ℝ) ≤ X ω}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 ω})
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)
have hb : ∀ (ε : ℚ),
  ∀ᵐ (ω' : Ω') ∂ν,
    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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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∞)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥0∞)
      (0 : ℝ≥0∞)
have 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∞)
Tactic: filter_upwards [ae_all_iff.2 hb] with ω' hn
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, X =ᶠ[ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)] 0
have 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
Tactic: filter_upwards [(h.neg).measure_pos_eq_zero_of_hasSubGaussianMGF_zero,
    h.measure_pos_eq_zero_of_hasSubGaussianMGF_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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∞)
⊢ X =ᶠ[ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)] 0
have h1₁ : 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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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∞)
⊢ X =ᶠ[ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)] 0
have h₁ : LE.le (α := ℝ≥0∞)
  ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {x : Ω | (fun (x : Ω) ↦ X x = 0 x) x}ᶜ : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: apply nonpos_iff_eq_zero.1
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {x : Ω | (fun (x : Ω) ↦ X x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
have calc : Eq (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω ≠ 0} : ℝ≥0∞)
  ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0 ∨ 0 < X ω} : ℝ≥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]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {x : Ω | (fun (x : Ω) ↦ X x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
have calc₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | X ω < 0} : ℝ≥0∞)
    ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | 0 < X ω} : ℝ≥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]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
hX : Measurable X
h : HasSubgaussianMGF X 0 κ ν
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] 0
have rw : ∀ᵐ (y : Ω') ∂ν, ∀ᵐ (z : Ω) ∂((κ : (a : Ω') → Measure Ω) y : Measure Ω), X z = 0 z
Tactic: rw [Filter.EventuallyEq, Measure.ae_comp_iff (measurableSet_eq_fun hX (by fun_prop))]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] 0
have hX : AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: have hX := h.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 Ω) ∘ₘ ν)
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] 0
have h' : HasSubgaussianMGF (AEStronglyMeasurable.mk X hX) 0 κ ν
Tactic: have h' : HasSubgaussianMGF (hX.mk X) 0 κ ν := h.congr hX.ae_eq_mk
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 κ ν
⊢ 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)
    κ ν
have 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)
    κ ν
Tactic: by_cases hX0 : cX = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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)
      κ ν
⊢ 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)
    κ ν
have 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)
    κ ν
Tactic: by_cases hX0 : cX = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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
⊢ 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)
    κ ν
have pos : ∀ (hX : HasSubgaussianMGF X 0 κ ν), HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cY κ ν
Tactic: simp only [hX0, NNReal.sqrt_zero, zero_add, NNReal.sq_sqrt] at hX ⊢
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 κ ν
have pos : Y =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
Tactic: refine hY.congr ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 κ ν
⊢ Y =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
have 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
Tactic: filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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
⊢ Y =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
have h₁ : ∀ (a : Ω), X a = 0 a → Y a = X a + Y a
Tactic: filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]