awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ω' : Ω'
hm : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
t : ℝ
⊢ mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simpa [mgf] using hm (-t)

Premises used: ProbabilityTheory.mgf, Neg.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
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
h₂ h₃ :
  ∀ (ω' : Ω')
    (hm : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (t : ℝ), mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) (-X) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
filter_upwards [h.mgf_le] with ω' hm t using by simpa [mgf] using hm (-t)

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
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 Ω) ∘ₘ ν)

Tactic:
(integrable_congr ?_).mpr (h.integrable_exp_mul t)

Premises used: Iff.mpr, MeasureTheory.integrable_congr, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
refine :
  (ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω))
    fun (ω : Ω) ↦ rexp (t * X ω)
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * Y ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
refine (integrable_congr ?_).mpr (h.integrable_exp_mul t)

Premises used: Iff.mpr, MeasureTheory.integrable_congr, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω
rw rw₁ : rexp (t * Y ω) = rexp (t * Y ω)
⊢ rexp (t * Y ω) = rexp (t * X ω)

Tactic:
rw [hω]
-- Module: Mathlib.Probability.Moments.SubGaussian
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
h₂ h₃ : ∀ (ω : Ω) (hω : X ω = Y ω), rexp (t * Y ω) = rexp (t * X ω)
⊢ (ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω))
    fun (ω : Ω) ↦ rexp (t * X ω)

Tactic:
filter_upwards [h'] with ω hω using by rw [hω]
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω), X ω = Y ω

Tactic:
have h'' := Measure.ae_ae_of_ae_comp h'
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω
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)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (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

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
h₁ : mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [mgf_congr (Filter.EventuallyEq.symm h')]

Premises used: ProbabilityTheory.mgf_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Moments.SubGaussian
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Ω) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h_mgf t
-- Module: Mathlib.Probability.Moments.SubGaussian
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Ω) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact h_mgf t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] Y
⊢ HasSubgaussianMGF X c κ ν ↔ HasSubgaussianMGF Y c κ ν

Tactic:
⟨fun hX ↦ congr hX h, fun hY ↦ congr hY (ae_eq_symm h)⟩

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.congr, MeasureTheory.ae_eq_symm, Iff.intro
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)) ((⇑(κ.map Y) : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
have h1 := h.integrable_exp_mul t
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)) (Measure.map Y ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν))
⊢ AEMeasurable (_m := mΩ'') Y ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
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 Ω'') ∘ₘ ν)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h1 : @Integrable ℝ _ _ _ mΩ'' ((fun (ω : Ω) ↦ rexp (t * X ω)) ∘ Y) ((⇑κ : (a : Ω') → Measure Ω'') ∘ₘ ν)),
    @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

Premises used: MeasureTheory.Measure.map_comp, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Moments.SubGaussian
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₁ :
  ∀ (ω' : Ω')
    (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)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (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

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
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 (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h_mgf t
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
h₁ :
  mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') =
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
⊢ mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
convert! h_mgf t
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
h₁ :
  ∀ (t : ℝ),
    mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t =
      mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t
⊢ mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') =
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')

Tactic:
ext t
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
h₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω))
    (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
⊢ mgf (m := mΩ'') (X ∘ Y) ((κ : (a : Ω') → Measure Ω'') ω') t =
    mgf (m := mΩ) X (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t

Tactic:
rw [map_apply _ hY, mgf_map hY.aemeasurable]

Premises used: ProbabilityTheory.Kernel.map_apply, Measurable.aemeasurable, ProbabilityTheory.mgf_map
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω))
    (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')

Tactic:
(h_int t).1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
h₁ :
  Eq (α := autoParam (Measure Ω) AEStronglyMeasurable._auto_1) (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
    (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω))
    (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))

Tactic:
convert! (h_int t).1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : ℝ
h₁ h₂ :
  Eq (α := autoParam (Measure Ω) AEStronglyMeasurable._auto_1) (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
    (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
⊢ Eq (α := autoParam (Measure Ω) AEStronglyMeasurable._auto_1) (Measure.map Y ((κ : (a : Ω') → Measure Ω'') ω'))
    (((κ.map Y : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω')

Tactic:
rw [map_apply _ hY]

Premises used: ProbabilityTheory.Kernel.map_apply
-- Module: Mathlib.Probability.Moments.SubGaussian
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 κ ν

Tactic:
⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, ?_⟩⟩

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.mk, Iff.intro
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ℝ) ∘ₘ ν)
refine_3 :
  ∀ (h : HasSubgaussianMGF X c κ ν),
    ∀ᵐ (ω' : Ω') ∂ν,
      ∀ (t : ℝ),
        mgf (m := measurableSpace) id (((κ.map X : Kernel Ω' ℝ) : (a : Ω') → Measure ℝ) ω') t ≤
          rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (κ.map X) ν ↔ HasSubgaussianMGF X c κ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, ?_⟩⟩
-- Module: Mathlib.Probability.Moments.SubGaussian
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) ν
refine_1 : HasSubgaussianMGF (id ∘ X) c κ ν
⊢ HasSubgaussianMGF X c κ ν

Tactic:
change HasSubgaussianMGF (id ∘ X) c κ ν

Premises used: Function.comp, id, ProbabilityTheory.Kernel.HasSubgaussianMGF
-- Module: Mathlib.Probability.Moments.SubGaussian
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 (id ∘ X) c κ ν

Tactic:
.of_map hX h

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.of_map
-- Module: Mathlib.Probability.Moments.SubGaussian
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 (id ∘ X) c κ ν

Tactic:
exact .of_map hX h
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (ω : ℝ) ↦ rexp (t * id ω))
    (Measure.map X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
refine_2 : @Integrable ℝ _ _ _ mΩ ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) ((⇑(κ.map 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]

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.deterministic_comp_eq_map, MeasureTheory.Measure.deterministic_comp_eq_map, MeasureTheory.Measure.comp_assoc, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ℝ _ _ _ mΩ ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
h.integrable_exp_mul t

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, Real.exp
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ℝ _ _ _ mΩ ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
exact h.integrable_exp_mul t

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := measurableSpace) id (((κ.map X : Kernel Ω' ℝ) : (a : Ω') → Measure ℝ) ω') t ≤
        rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simpa [Kernel.map_apply _ hX, mgf_id_map hX.aemeasurable] using h.mgf_le

Premises used: ProbabilityTheory.Kernel.map_apply, Measurable.aemeasurable, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le, ProbabilityTheory.mgf_id_map
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r t : ℝ
simp_rw : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * r * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * (r * X ω))) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Moments.SubGaussian
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 Ω) ∘ₘ ν)

Tactic:
h.integrable_exp_mul (t * r)

Premises used: HMul.hMul, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul