awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
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)
h₂ : ∀ (ω : Ω) (hl : a ≤ X ω) (hr : X ω ≤ b), -X ω ∈ Set.Icc (-b) (-a)
⊢ ∀ᵐ (ω : Ω) ∂μ, -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⟩
-- Module: Mathlib.Probability.Moments.SubGaussian
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
hc₃ hc₄ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0

Tactic:
rw [integral_neg, hc, neg_zero]

Premises used: MeasureTheory.integral_neg, neg_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
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
ht₁ ht₂ ht₃ ht₄ : t < 0
⊢ 0 < -t

Tactic:
rwa [Left.neg_pos_iff]

Premises used: Left.neg_pos_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ 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:
ring_nf
-- Module: Mathlib.Probability.Moments.SubGaussian
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)
_₂ :
  rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2) =
    rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf X μ t ≤ 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

Premises used: HMul.hMul, NNNorm.nnnorm, HSub.hSub, HDiv.hDiv, Real.exp, HPow.hPow, ProbabilityTheory.mgf, OfNat.ofNat, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
rw :
  HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ)
    (HPow.hPow (β := ℕ) (‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) 2) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) μ

Tactic:
rw [← sub_sub_sub_cancel_right b a μ[X]]

Premises used: sub_sub_sub_cancel_right, MeasureTheory.integral
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ∂μ)
hc : Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ)
    (HPow.hPow (β := ℕ) (‖b - ∫ (x : Ω), X x ∂μ - (a - ∫ (x : Ω), X x ∂μ)‖₊ / 2) 2) μ

Tactic:
apply hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero (hm.sub_const _)

Premises used: ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero, AEMeasurable.sub_const
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
ω : Ω
hab : X ω ∈ Set.Icc a b
⊢ X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)

Tactic:
simpa using hab
-- Module: Mathlib.Probability.Moments.SubGaussian
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
h₁ h₂ :
  ∀ (ω : Ω) (hab : X ω ∈ Set.Icc a b), X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)

Tactic:
filter_upwards [hb] with ω hab using by simpa using hab
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ Eq (α := ℝ) (∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ) 0

Tactic:
simp [integral_sub (Integrable.of_mem_Icc a b hm hb) (integrable_const _)]

Premises used: MeasureTheory.integral_sub, MeasureTheory.Integrable.of_mem_Icc, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)) μ)
⊢ 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
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)
rw : HasSubgaussianMGF ((fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)) (cX + cY) μ
⊢ HasSubgaussianMGF (X + Y) (cX + cY) μ

Tactic:
rw [h_eq]
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ

Tactic:
HasSubgaussianMGF.of_map ?_ this

Premises used: ProbabilityTheory.HasSubgaussianMGF.of_map
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)
refine : AEMeasurable (β := Ω × Ω) (fun (ω : Ω) ↦ (id ω, id ω)) μ
⊢ HasSubgaussianMGF ((fun (p : Ω × Ω) ↦ X p.1 + Y p.2) ∘ fun (ω : Ω) ↦ (id ω, id ω)) (cX + cY) μ

Tactic:
refine HasSubgaussianMGF.of_map ?_ this

Premises used: ProbabilityTheory.HasSubgaussianMGF.of_map
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)
⊢ AEMeasurable (β := Ω × Ω) (fun (ω : Ω) ↦ (id ω, id ω)) μ

Tactic:
@Measurable.aemeasurable _ _ _ (m.prod mΩ) _ _
      ((measurable_id'' hm).prodMk measurable_id)

Premises used: Measurable.aemeasurable, measurable_id, Measurable.prodMk, measurable_id''
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)
⊢ AEMeasurable (β := Ω × Ω) (fun (ω : Ω) ↦ (id ω, id ω)) μ

Tactic:
exact @Measurable.aemeasurable _ _ _ (m.prod mΩ) _ _
      ((measurable_id'' hm).prodMk measurable_id)

Premises used: Measurable.aemeasurable, measurable_id, Measurable.prodMk, measurable_id''
-- Module: Mathlib.Probability.Moments.SubGaussian
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 μ
suffices :
  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) μ

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)
-- Module: Mathlib.Probability.Moments.SubGaussian
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 μ
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 ())
⊢ HasSubgaussianMGF (mΩ := m.prod mΩ) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at hX ⊢

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
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 Y cY (condExpKernel μ m)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit (μ.trim hm)) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Moments.SubGaussian
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 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
-- Module: Mathlib.Probability.Moments.SubGaussian
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Ω' := PUnit.instMeasurableSpace) (fun (p : Ω × Ω) ↦ X p.1 + Y p.2) (cX + cY)
    (Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m)) (Measure.dirac ())

Tactic:
hX.add_comp hY'

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp
-- Module: Mathlib.Probability.Moments.SubGaussian
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 Ω))
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))
⊢ 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:
convert! hX.add_comp hY'

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp
-- Module: Mathlib.Probability.Moments.SubGaussian
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
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 (Ω × Ω))
⊢ Eq (α := Kernel Unit (Ω × Ω)) (Kernel.const Unit (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ))
    (Kernel.const Unit (μ.trim hm) ⊗ₖ Kernel.prodMkLeft Unit (condExpKernel μ m))

Tactic:
ext
-- Module: Mathlib.Probability.Moments.SubGaussian
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
h₂ h₃ :
  Eq (α := Measure (Ω × Ω)) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
⊢ 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:
rw [Kernel.const_apply, ← Measure.compProd, compProd_trim_condExpKernel]

Premises used: ProbabilityTheory.compProd_trim_condExpKernel, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
h_subG :
  ∀ i < HSub.hSub (α := ℕ) 0 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
hn :
  ∀
    (h_subG :
      ∀ i < HSub.hSub (α := ℕ) 0 1,
        HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range 0, Y i ω) (∑ i ∈ Finset.range 0, cY i) μ
h_subG :
  ∀ i < HAdd.hAdd (α := ℕ) 0 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), Y i ω)
    (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), cY i) μ

Tactic:
simp [h0]
-- Module: Mathlib.Probability.Moments.SubGaussian
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)) μ
i : ℕ
hi : i < n + 1 - 1
⊢ i < n + 1 + 1 - 1

Tactic:
lia
-- Module: Mathlib.Probability.Moments.SubGaussian
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), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ

Tactic:
specialize hn fun i hi ↦ h_subG i (by lia)
-- Module: Mathlib.Probability.Moments.SubGaussian
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) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF ((↑ℱ : ℕ → MeasurableSpace Ω) i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
hn : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
succ :
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1), Y i ω + Y (n + 1) ω)
    (∑ i ∈ Finset.range (n + 1), cY i + cY (n + 1)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Finset.range (n + 1 + 1), Y i ω) (∑ i ∈ Finset.range (n + 1 + 1), cY i) μ

Tactic:
simp_rw [Finset.sum_range_succ _ (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, Finset.sum_range_succ