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 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
have neg : 0 < mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t
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_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
neg : 0 < mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
have neg₁ : 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_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have rw : (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [log_exp]
-- 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 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have calc : log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
Tactic: calc cgf X (κ ω') t
  _ = log (mgf X (κ ω') t) := rfl
  _ ≤ log (exp (c * t ^ 2 / 2)) := by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t
  _ ≤ c * t ^ 2 / 2 := by rw [log_exp]
-- 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 : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
calc : log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
⊢ cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have calc₁ : log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: calc cgf X (κ ω') t
  _ = log (mgf X (κ ω') t) := rfl
  _ ≤ log (exp (c * t ^ 2 / 2)) := by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t
  _ ≤ c * t ^ 2 / 2 := by rw [log_exp]
-- 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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
have h₁ : ∀ (ω' : Ω') (h : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (0 * X y)) ((κ : (a : Ω') → Measure Ω) ω'))
  (h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)),
  IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: filter_upwards [h.ae_integrable_exp_mul 0, h.mgf_le] with ω' h h_mgf
-- 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 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have h₁ : ∀ (ω' : Ω') (h : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω'))
  (h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)),
  LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: filter_upwards [h.isFiniteMeasure, h.mgf_le] with ω' h h_mgf
-- 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 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
this : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') Set.univ ≤ 1
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rwa : (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ ≤ ENNReal.ofReal 1
Tactic: rwa [← ENNReal.ofReal_one, ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) 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 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
this : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') Set.univ ≤ 1
rwa : (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ ≤ ENNReal.ofReal 1
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rwa₁ : ENNReal.toReal ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ) ≤ 1
Tactic: rwa [← ENNReal.ofReal_one, ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) 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 : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') Set.univ ≤ 1
Tactic: suffices (κ ω').real Set.univ ≤ 1 by
    rwa [← ENNReal.ofReal_one, ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) zero_le_one]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ (q : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑q : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h_mgf₁ : ∀ᵐ (a : Ω') ∂ν,
  ∀ (i : ℚ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
      rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
Tactic: rw [← ae_all_iff] at h_mgf
Cleared hypotheses: h_mgf
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
have h_int' : ∀ (n : ℤ), ∀ᵐ (x : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) x)
Tactic: have h_int' (n : ℤ) := Measure.ae_integrable_of_integrable_comp (h_int n)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int' :
  ∀ (n : ℤ), ∀ᵐ (x : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) x)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
have h_int'₁ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
Tactic: rw [← ae_all_iff] at h_int'
Cleared hypotheses: h_int'
-- 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_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int' :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
have h : ∀ (ω' : Ω')
  (h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω'))
  (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: filter_upwards [h_int'] with ω' h_int t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h_int₁ : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: have h_int : ∀ᵐ ω' ∂ν, ∀ t, Integrable (fun ω ↦ exp (t * X ω)) (κ ω') := by
      have h_int' (n : ℤ) := Measure.ae_integrable_of_integrable_comp (h_int n)
      rw [← ae_all_iff] at h_int'
      filter_upwards [h_int'] with ω' h_int t
      exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil 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_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : ∀ (ω' : Ω')
  (h_mgf :
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2))
  (h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')) (t : ℝ),
  mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: filter_upwards [h_mgf, h_int] with ω' h_mgf h_int 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_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf_1 :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int_2 :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
ω' : Ω'
h_mgf :
  ∀ (i : ℚ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
      rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : IsClosed (X := ℝ)
  {b : ℝ | mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') b ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) b 2 / 2)}
Tactic: refine Rat.denseRange_cast.induction_on t ?_ h_mgf
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ HasSubgaussianMGF (mΩ := mΩ) X c 0 ν
have integrable_exp_mul : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑0 : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
integrable_exp_mul : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑0 : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ HasSubgaussianMGF (mΩ := mΩ) X c 0 ν
have mgf_le : ∀ᵐ (ω' : Ω') ∂ν,
  ∀ (t : ℝ),
    mgf (m := mΩ) X (((0 : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : ∀ (a : Ω'),
  Membership.mem (γ := Set Ω')
    {x : Ω' |
      Membership.mem (γ := Set Ω')
          {x : Ω' |
            (fun (ω' : Ω') ↦
                ∀ (t : ℝ),
                  mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
              x}
          x →
        Membership.mem (γ := Set Ω')
          {x : Ω' |
            (fun (ω' : Ω') ↦
                ∀ (t : ℝ),
                  mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
              x}
          x}
    a
Tactic: filter_upwards [h.mgf_le] with ω' hm t using by simpa [mgf] using hm (-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₁ :
  ∀ (a : Ω'),
    Membership.mem (γ := Set Ω')
      {x : Ω' |
        Membership.mem (γ := Set Ω')
            {x : Ω' |
              (fun (ω' : Ω') ↦
                  ∀ (t : ℝ),
                    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
                x}
            x →
          Membership.mem (γ := Set Ω')
            {x : Ω' |
              (fun (ω' : Ω') ↦
                  ∀ (t : ℝ),
                    mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
                x}
            x}
      a
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₂ : ∀ (a : Ω'),
  (∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) →
    ∀ (t : ℝ), mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) a) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: filter_upwards [h.mgf_le] with ω' hm t using by simpa [mgf] using hm (-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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * Y ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have refine : (ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω))
  fun (ω : Ω) ↦ rexp (t * X ω)
Tactic: refine (integrable_congr ?_).mpr (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 Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
t : ℝ
ω : Ω
hω : X ω = Y ω
⊢ rexp (t * Y ω) = rexp (t * X ω)
have rw : rexp (t * Y ω) = rexp (t * Y ω)
Tactic: rw [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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
t : ℝ
⊢ (ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω))
    fun (ω : Ω) ↦ rexp (t * X ω)
have h₁ : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω | (fun (x : Ω) ↦ Eq (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x) ((fun (ω : Ω) ↦ rexp (t * X ω)) x)) x}
          x}
    a
Tactic: filter_upwards [h'] with ω hω using by rw [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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
t : ℝ
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ Eq (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x) ((fun (ω : Ω) ↦ rexp (t * X ω)) x)) x}
            x}
      a
⊢ (ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω))
    fun (ω : Ω) ↦ rexp (t * X ω)
have h₂ : ∀ (a : Ω), X a = Y a → rexp (t * Y a) = rexp (t * X a)
Tactic: filter_upwards [h'] with ω hω using by rw [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 : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω), X ω = Y ω
Tactic: have h'' := Measure.ae_ae_of_ae_comp 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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω), X ω = Y ω
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : ∀ (ω' : Ω')
  (h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
  (h' : ∀ᵐ (ω : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω), X ω = Y ω) (t : ℝ),
  mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: filter_upwards [h.mgf_le, h''] with ω' h_mgf 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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h'_1 : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω), X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h' : ∀ᵐ (ω : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω), X ω = Y ω
t : ℝ
⊢ mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [mgf_congr (Filter.EventuallyEq.symm h')]