awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * (X ∘ Y) ω)) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)
have h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑(κ.map Y) : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: have h1 := h.integrable_exp_mul t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
t : ℝ
h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑(κ.map Y) : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * (X ∘ Y) ω)) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)
have rwa : ∀ (h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν))),
  @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * (X ∘ Y) ω)) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)
Tactic: rwa [← Measure.map_comp _ _ hY, integrable_map_measure h1.aestronglyMeasurable (by fun_prop)]
      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 Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
t : ℝ
h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑(κ.map Y) : (a : Ω') → Measure Ω) ∘ₘ ν)
rwa :
  ∀ (h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν))),
    @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * (X ∘ Y) ω)) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * (X ∘ Y) ω)) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)
have rwa₁ : ∀ (h1 : @Integrable ℝ _ _ _ mΩ'' ((fun (ω : Ω) ↦ rexp (t * X ω)) ∘ Y) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)),
  @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * (X ∘ Y) ω)) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)
Tactic: rwa [← Measure.map_comp _ _ hY, integrable_map_measure h1.aestronglyMeasurable (by fun_prop)]
      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 Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : ∀ (ω' : Ω')
  (h_int :
    ∀ (t : ℝ),
      @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω'))
  (h_mgf :
    ∀ (t : ℝ),
      mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤
        rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
  (t : ℝ), mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: filter_upwards [h.ae_forall_integrable_exp_mul, h.mgf_le] with ω' h_int h_mgf t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
ω' : Ω'
h_int :
  ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤
      rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
⊢ mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') =
  mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
Tactic: convert! h_mgf t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
ω' : Ω'
h_int :
  ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤
      rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
⊢ mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') =
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
have h₁ : ∀ (t : ℝ),
  mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t =
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
ω' : Ω'
h_int :
  ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤
      rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t_1 t : ℝ
⊢ mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t =
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t
have h₁ : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω))
  (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
Tactic: rw [map_apply _ hY, mgf_map hY.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
ω' : Ω'
h_int :
  ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤
      rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t_1 t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω))
    (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
have h₁ : Eq (α := autoParam (Measure Ω) AEStronglyMeasurable._auto_1) (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
  (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
Tactic: convert! (h_int t).1
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF (mΩ := mΩ) X c (κ.map Y) ν
ω' : Ω'
h_int :
  ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤
      rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t_1 t : ℝ
⊢ Eq (α := autoParam (Measure Ω) AEStronglyMeasurable._auto_1) (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
    (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
have h₁ : Eq (α := autoParam (Measure Ω) AEStronglyMeasurable._auto_1) (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
  (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
Tactic: rw [map_apply _ hY]
-- 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
hX : Measurable X
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν ↔ HasSubgaussianMGF X c κ ν
have refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν), HasSubgaussianMGF X c κ ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, ?_⟩⟩
-- 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
hX : Measurable X
refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν), HasSubgaussianMGF X c κ ν
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν ↔ HasSubgaussianMGF X c κ ν
have refine_2 : ∀ (h : HasSubgaussianMGF X c κ ν) (t : ℝ),
  @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) ((⇑(κ.map X) : (a : Ω') → Measure ℝ) ∘ₘ ν)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, ?_⟩⟩
-- 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
hX : Measurable X
refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν), HasSubgaussianMGF X c κ ν
refine_2 :
  ∀ (h : HasSubgaussianMGF X c κ ν) (t : ℝ),
    @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) ((⇑(κ.map X) : (a : Ω') → Measure ℝ) ∘ₘ ν)
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν ↔ HasSubgaussianMGF X c κ ν
have refine_3 : ∀ (h : HasSubgaussianMGF X c κ ν),
  ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := measurableSpace) id (((κ.map X : Kernel Ω' ℝ) : (a : Ω') → Measure ℝ) ω') t ≤
        rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, ?_⟩⟩
-- 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
hX : Measurable X
h : HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν
⊢ HasSubgaussianMGF X c κ ν
have refine_1 : HasSubgaussianMGF (id ∘ X) c κ ν
Tactic: change HasSubgaussianMGF (id ∘ X) c κ ν
-- 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
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) ((⇑(κ.map X) : (a : Ω') → Measure ℝ) ∘ₘ ν)
have refine_2 : @Integrable ℝ _ _ _ mΩ ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: rw [← Kernel.deterministic_comp_eq_map hX, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map, integrable_map_measure (by fun_prop) hX.aemeasurable]
-- 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 : HasSubgaussianMGF X c κ ν
r t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * (r * X ω))) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have simp_rw : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * r * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: simp_rw [← mul_assoc]
-- 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 : HasSubgaussianMGF X c κ ν
r : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ) (fun (ω : Ω) ↦ r * X ω) ((κ : (a : Ω') → Measure Ω) ω') t ≤
        rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have 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) sorry * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: filter_upwards [h.mgf_le] with ω hω t
-- 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 : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
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)
have h₁ : mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) (t * r) ≤
  rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) sorry * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [mgf_const_mul, mul_comm]
-- 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 : 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)
have h₁ : rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2) =
  rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) sorry * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: refine (hω (t * r)).trans_eq ?_
-- 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 : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
⊢ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2) =
    rexp ((↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) ⋯ * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : (↑c : ℝ) * HPow.hPow (β := ℕ) (t * r) 2 / 2 =
  (↑(NNReal.mk (HPow.hPow (β := ℕ) r 2) sorry * c) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: congr 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      0 ≤ t →
        Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
          rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have 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)
Tactic: filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul, h.isFiniteMeasure] with ω' h1 h2 _ t ht
-- 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 : 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
⊢ rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp (-t * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have rw : rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
  rexp (-t * ε) * rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [exp_add]
-- 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 : 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
⊢ rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp (-t * ε) * rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have hbc : mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: gcongr
-- 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 : 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 * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have calc : rexp (-t * ε) * mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤
  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
-- 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 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have pos : ∀ (hc0 : c = 0),
  ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
Tactic: by_cases hc0 : c = 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 : Ω → ℝ
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 : ℝ)))
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have neg : ∀ (hc0 : ¬c = 0),
  ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
Tactic: by_cases hc0 : c = 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : c = 0
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have 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 : ℝ)))
Tactic: filter_upwards [h.measure_univ_le_one] with ω' h
-- 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 : 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 : ℝ)))
have h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤ 1
Tactic: simp only [hc0, NNReal.coe_zero, mul_zero, div_zero, exp_zero]
-- 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 : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤ 1
have h₁ : (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} ≤ ENNReal.ofReal 1
Tactic: refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
-- 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 : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} ≤ ENNReal.ofReal 1
have h₁ : LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | ε ≤ X ω} : ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: simp only [ENNReal.ofReal_one]
-- 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 : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') {ω : Ω | ε ≤ X ω} ≤
      rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have 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 : ℝ)))
Tactic: filter_upwards [measure_ge_le_exp_add h ε] with ω' h
-- 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)
⊢ rexp (-(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2) =
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have e_x : -(ε / (↑c : ℝ)) * ε + (↑c : ℝ) * HPow.hPow (β := ℕ) (ε / (↑c : ℝ)) 2 / 2 = -HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ))
Tactic: congr