awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
hb₁ : ∀ᵐ (ω : Ω) ∂μ, -X ω ∈ Set.Icc (-b) (-a)
hc₁ : Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0
⊢ mgf (-X) μ (-t) ≤ rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2)
have ht₁ : 0 < -t
Tactic: apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
ω : Ω
⊢ X ω ∈ Set.Icc a b → -X ω ∈ Set.Icc (-b) (-a)
have h : ∀ (hl : a ≤ X ω) (hr : X ω ≤ b), -X ω ∈ Set.Icc (-b) (-a)
Tactic: ⟨hl, hr⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
⊢ ∀ᵐ (ω : Ω) ∂μ, -X ω ∈ Set.Icc (-b) (-a)
have h : ∀ (a_1 : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ∈ Set.Icc a b) x} x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ -X ω ∈ Set.Icc (-b) (-a)) x} x}
    a_1
Tactic: filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
h :
  ∀ (a_1 : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ∈ Set.Icc a b) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ -X ω ∈ Set.Icc (-b) (-a)) x} x}
      a_1
⊢ ∀ᵐ (ω : Ω) ∂μ, -X ω ∈ Set.Icc (-b) (-a)
have h₁ : ∀ (a_1 : Ω), X a_1 ∈ Set.Icc a b → -X a_1 ∈ Set.Icc (-b) (-a)
Tactic: filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
h :
  ∀ (a_1 : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ∈ Set.Icc a b) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ -X ω ∈ Set.Icc (-b) (-a)) x} x}
      a_1
h₁ : ∀ (a_1 : Ω), X a_1 ∈ Set.Icc a b → -X a_1 ∈ Set.Icc (-b) (-a)
⊢ ∀ᵐ (ω : Ω) ∂μ, -X ω ∈ Set.Icc (-b) (-a)
have h₂ : ∀ (ω : Ω) (hl : a ≤ X ω) (hr : X ω ≤ b), -X ω ∈ Set.Icc (-b) (-a)
Tactic: filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
⊢ Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0
have hc₁ : Eq (α := ℝ) (-∫ (a : Ω), X a ∂μ) 0
Tactic: rw [integral_neg, hc, neg_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
hc₁ : Eq (α := ℝ) (-∫ (a : Ω), X a ∂μ) 0
⊢ Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0
have hc₂ : Eq (α := ℝ) (-0) 0
Tactic: rw [integral_neg, hc, neg_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
hc₁ : Eq (α := ℝ) (-∫ (a : Ω), X a ∂μ) 0
hc₂ : Eq (α := ℝ) (-0) 0
⊢ Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0
have hc₃ : Eq (α := ℝ) 0 0
Tactic: rw [integral_neg, hc, neg_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have _ : mgf X μ t = mgf (-X) μ (-t)
Tactic: calc
    _ = mgf (-X) μ (-t) := by simp [mgf]
    _ ≤ exp ((‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2) := by
      apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]
    _ = exp (((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2) := by ring_nf
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
_ : mgf X μ t = mgf (-X) μ (-t)
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have _₁ : mgf (-X) μ (-t) ≤ rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2)
Tactic: calc
    _ = mgf (-X) μ (-t) := by simp [mgf]
    _ ≤ exp ((‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2) := by
      apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]
    _ = exp (((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2) := by ring_nf
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
_ : mgf X μ t = mgf (-X) μ (-t)
_₁ : mgf (-X) μ (-t) ≤ rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2)
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have _₂ : rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2) =
  rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: calc
    _ = mgf (-X) μ (-t) := by simp [mgf]
    _ ≤ exp ((‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2) := by
      apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]
    _ = exp (((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2) := by ring_nf
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) μ
have rw : HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ)
  (HPow.hPow (β := ℕ) (‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) 2) μ
Tactic: rw [← sub_sub_sub_cancel_right b a μ[X]]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ)
    (HPow.hPow (β := ℕ) (‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) 2) μ
have hb₁ : ∀ᵐ (ω : Ω) ∂μ, X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
Tactic: apply hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero (hm.sub_const _)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hb₁ : ∀ᵐ (ω : Ω) ∂μ, X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ)
    (HPow.hPow (β := ℕ) (‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) 2) μ
have hc : Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0
Tactic: apply hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero (hm.sub_const _)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
have h : ∀ (a_1 : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ∈ Set.Icc a b) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω | (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)) x}
          x}
    a_1
Tactic: filter_upwards [hb] with ω hab using by simpa using hab
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
h :
  ∀ (a_1 : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (ω : Ω) ↦ X ω ∈ Set.Icc a b) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)) x}
            x}
      a_1
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
have h₁ : ∀ (a_1 : Ω), X a_1 ∈ Set.Icc a b → X a_1 - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
Tactic: filter_upwards [hb] with ω hab using by simpa using hab
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this :
  HasSubgaussianMGF (mΩ := m.prod mΩ) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
⊢ HasSubgaussianMGF (X + Y) (cX + cY) μ
have h_eq : X + Y = (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)
Tactic: have h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ (fun ω ↦ (id ω, id ω)) := rfl
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this :
  HasSubgaussianMGF (mΩ := m.prod mΩ) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
h_eq : X + Y = (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)
⊢ HasSubgaussianMGF (X + Y) (cX + cY) μ
have rw : HasSubgaussianMGF ((fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)) (cX + cY) μ
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this :
  HasSubgaussianMGF (mΩ := m.prod mΩ) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
h_eq : X + Y = (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)
⊢ HasSubgaussianMGF ((fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)) (cX + cY) μ
have refine : AEMeasurable (β := Ω × Ω) (fun (ω : Ω) ↦ (id ω, id ω)) μ
Tactic: refine HasSubgaussianMGF.of_map ?_ this
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ HasSubgaussianMGF (X + Y) (cX + cY) μ
have suffices : HasSubgaussianMGF (mΩ := m.prod mΩ) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
  (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
Tactic: suffices HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY)
      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ) by
    have h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ (fun ω ↦ (id ω, id ω)) := rfl
    rw [h_eq]
    refine HasSubgaussianMGF.of_map ?_ this
    exact @Measurable.aemeasurable _ _ _ (m.prod mΩ) _ _
      ((measurable_id'' hm).prodMk measurable_id)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ HasSubgaussianMGF (mΩ := m.prod mΩ) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
have rw : ∀
  (hX :
    Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ()))
  (hY : HasCondSubgaussianMGF m hm Y cY μ),
  Kernel.HasSubgaussianMGF (mΩ := m.prod mΩ) (mΩ' := PUnit.instMeasurableSpace) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2)
    (cX + cY) (Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)) (Measure.dirac ())
Tactic: rw [HasSubgaussianMGF_iff_kernel] at hX ⊢
Cleared hypotheses: hX, hY
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ Kernel.HasSubgaussianMGF (mΩ := m.prod mΩ) (mΩ' := PUnit.instMeasurableSpace) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2)
    (cX + cY) (Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)) (Measure.dirac ())
have hY' : Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
  (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
    (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))
Tactic: have hY' : Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
      (Kernel.const Unit (μ.trim hm) ∘ₘ Measure.dirac ()) := by simpa
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' :
  Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))
⊢ Kernel.HasSubgaussianMGF (mΩ := m.prod mΩ) (mΩ' := PUnit.instMeasurableSpace) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2)
    (cX + cY) (Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)) (Measure.dirac ())
have h : m.prod mΩ = Prod.instMeasurableSpace →
  Eq (α := Kernel Unit (Ω × Ω)) (Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ))
    (Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m))
Tactic: convert! hX.add_comp hY'
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' :
  Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))
e_3 : m.prod mΩ = Prod.instMeasurableSpace
⊢ Eq (α := Kernel Unit (Ω × Ω)) (Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ))
    (Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m))
have h : ∀ (a : Unit),
  Eq (α := Measure (Ω × Ω))
    ((Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
    ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' :
  Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))
e_3 : m.prod mΩ = Prod.instMeasurableSpace
a : Unit
⊢ Eq (α := Measure (Ω × Ω))
    ((Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
    ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
have h : Eq (α := Measure (Ω × Ω)) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
  ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a)
Tactic: rw [Kernel.const_apply, ← Measure.compProd, compProd_trim_condExpKernel]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' :
  Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))
e_3 : m.prod mΩ = Prod.instMeasurableSpace
a : Unit
h :
  Eq (α := Measure (Ω × Ω)) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
    ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a)
⊢ Eq (α := Measure (Ω × Ω))
    ((Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
    ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
have h₁ : Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ = μ.trim hm ⊗ₘ condExpKernel μ m
Tactic: rw [Kernel.const_apply, ← Measure.compProd, compProd_trim_condExpKernel]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : StandardBorelSpace Ω
inst_1 : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
hY' :
  Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))
e_3 : m.prod mΩ = Prod.instMeasurableSpace
a : Unit
h :
  Eq (α := Measure (Ω × Ω)) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
    ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a)
h₁ : Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ = μ.trim hm ⊗ₘ condExpKernel μ m
⊢ Eq (α := Measure (Ω × Ω))
    ((Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
    ((Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m) : (a : Unit) → Measure (Ω × Ω)) a :
      Measure (Ω × Ω))
have h₂ : Eq (α := Measure (Ω × Ω)) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
Tactic: rw [Kernel.const_apply, ← Measure.compProd, compProd_trim_condExpKernel]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst_1 : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted (β := fun (i : ℕ) ↦ ℝ) ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
h :
  ∀
    (hn :
      ∀ (h_subG : ∀ i < n - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ)
    (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
hn :
  ∀ (h_subG : ∀ i < n + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1 + 1), Y i ω) (∑ i ∈ Finset.range (n + 1 + 1), cY i) μ
have hn₁ : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
Tactic: specialize hn fun i hi ↦ h_subG i (by lia)
Cleared hypotheses: hn