awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
Y : Ω → ℝ
h' : X =ᶠ[ae μ] Y
apply :
  X =ᶠ[ae (F := Measure Ω)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))]
    Y
⊢ Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) Y c (Kernel.const Unit μ) (Measure.dirac ())

Tactic:
apply h.congr

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
Y : Ω → ℝ
h' : X =ᶠ[ae μ] Y
⊢ X =ᶠ[ae (F := Measure Ω)
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))]
    Y

Tactic:
simpa
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
p : ℝ≥0
rw :
  ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
    (t : ℝ) (p : ℝ≥0), MemLp (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) μ
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
p : ℝ≥0
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) μ

Tactic:
simpa using h.memLp_exp_mul t p

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
rw :
  ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
    (t : ℝ), cgf X μ t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ cgf X μ t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
⊢ cgf X μ t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
simpa using (all_ae_of h.cgf_le t)

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le, MeasureTheory.all_ae_of
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ HasSubgaussianMGF (fun (x : Ω) ↦ 0) 0 μ

Tactic:
simp [HasSubgaussianMGF_iff_kernel]

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsZeroOrProbabilityMeasure μ
⊢ HasSubgaussianMGF 0 0 μ

Tactic:
fun_zero

Premises used: ProbabilityTheory.HasSubgaussianMGF.fun_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ HasSubgaussianMGF (-X) c μ

Tactic:
simpa [HasSubgaussianMGF_iff_kernel] using (HasSubgaussianMGF_iff_kernel.1 h).neg

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel, ProbabilityTheory.Kernel.HasSubgaussianMGF.neg, Iff.mp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)

Tactic:
have h1 := h.integrable_exp_mul t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)
⊢ AEMeasurable Y μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h1 : Integrable (ε := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) ∘ Y) μ),
    Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * (X ∘ Y) ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * (X ∘ Y) ω)) μ

Tactic:
rwa [integrable_map_measure h1.aestronglyMeasurable (by fun_prop)] at h1

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
⊢ mgf (m := mΩ) X (Measure.map Y μ) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
h₁ : mgf (X ∘ Y) μ t = mgf (m := mΩ) X (Measure.map Y μ) t
⊢ mgf (X ∘ Y) μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
convert! h.mgf_le t using 1

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
h₁ h₂ : mgf (X ∘ Y) μ t = mgf (X ∘ Y) μ t
⊢ mgf (X ∘ Y) μ t = mgf (m := mΩ) X (Measure.map Y μ) t

Tactic:
rw [mgf_map hY (h.integrable_exp_mul t).1]

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul, And.left, ProbabilityTheory.mgf_map
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ) ↔ HasSubgaussianMGF X c μ

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

Premises used: ProbabilityTheory.HasSubgaussianMGF.mk, Iff.intro
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)), HasSubgaussianMGF X c μ
refine_2 :
  ∀ (h : HasSubgaussianMGF X c μ) (t : ℝ),
    @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)
refine_3 :
  ∀ (h : HasSubgaussianMGF X c μ) (t : ℝ),
    mgf (m := measurableSpace) id (Measure.map X μ) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ) ↔ HasSubgaussianMGF X c μ

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, fun t ↦ ?_⟩⟩
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
refine_1 : HasSubgaussianMGF (id ∘ X) c μ
⊢ HasSubgaussianMGF X c μ

Tactic:
rw [← Function.id_comp X]

Premises used: Function.id_comp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
⊢ HasSubgaussianMGF (id ∘ X) c μ

Tactic:
.of_map hX h

Premises used: ProbabilityTheory.HasSubgaussianMGF.of_map
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
⊢ HasSubgaussianMGF (id ∘ X) c μ

Tactic:
exact .of_map hX h
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
refine_2 : Integrable (ε := ℝ) ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) μ
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)

Tactic:
rw [integrable_map_measure (by fun_prop) hX]

Premises used: MeasureTheory.integrable_map_measure
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (ε := ℝ) ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) μ

Tactic:
h.integrable_exp_mul t

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul, Real.exp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (ε := ℝ) ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) μ

Tactic:
exact h.integrable_exp_mul t

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
refine_3 : mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf (m := measurableSpace) id (Measure.map X μ) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [mgf_id_map hX]

Premises used: ProbabilityTheory.mgf_id_map
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact h.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
hX : HasSubgaussianMGF X c μ
hXY : IdentDistrib X Y μ μ'
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)

Tactic:
rw [← id_map_iff hXY.aemeasurable_fst] at hX

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.HasSubgaussianMGF.id_map_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
hX : HasSubgaussianMGF X c μ
hXY : IdentDistrib X Y μ μ'
hX₁ : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
⊢ IdentDistrib X Y μ μ'

Tactic:
rw [← id_map_iff hXY.aemeasurable_fst] at hX

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_fst, ProbabilityTheory.HasSubgaussianMGF.id_map_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
hX : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
hXY : IdentDistrib X Y μ μ'
rwa : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map Y μ')
rwa₁ rwa₂ rwa₃ rwa₄ : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
⊢ HasSubgaussianMGF Y c μ'

Tactic:
rwa [← id_map_iff hXY.aemeasurable_snd, ← hXY.map_eq]

Premises used: ProbabilityTheory.IdentDistrib.aemeasurable_snd, ProbabilityTheory.HasSubgaussianMGF.id_map_iff, ProbabilityTheory.IdentDistrib.map_eq
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (μ.trim hm)

Tactic:
(hX.integrable_exp_mul t).trim hm ?_

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul, MeasureTheory.Integrable.trim
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
refine : StronglyMeasurable (β := ℝ) fun (ω : Ω) ↦ rexp (t * X ω)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (μ.trim hm)

Tactic:
refine (hX.integrable_exp_mul t).trim hm ?_

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul, MeasureTheory.Integrable.trim
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Measurable (β := ℝ) fun (ω : Ω) ↦ rexp (t * X ω)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ StronglyMeasurable (β := ℝ) fun (ω : Ω) ↦ rexp (t * X ω)

Tactic:
exact Measurable.stronglyMeasurable <| by fun_prop

Premises used: Measurable.stronglyMeasurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
rw : ∫ (x : Ω), rexp (t * X x) ∂μ ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hf : StronglyMeasurable (β := ℝ) fun (ω : Ω) ↦ rexp (t * X ω)
⊢ mgf X (μ.trim hm) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [mgf, ← integral_trim]

Premises used: ProbabilityTheory.mgf, MeasureTheory.integral_trim
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ ∫ (x : Ω), rexp (t * X x) ∂μ ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
hX.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ ∫ (x : Ω), rexp (t * X x) ∂μ ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact hX.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
r : ℝ
rw :
  ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
    (r : ℝ),
    Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ r * X ω)
      (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HPow.hPow (β := ℕ) r 2) ⋯ * c) (Kernel.const Unit μ) (Measure.dirac ())
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ r * X ω) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HPow.hPow (β := ℕ) r 2) ⋯ * c) μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h ⊢

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
r : ℝ
⊢ Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ r * X ω)
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HPow.hPow (β := ℕ) r 2) ⋯ * c) (Kernel.const Unit μ) (Measure.dirac ())

Tactic:
Kernel.HasSubgaussianMGF.const_mul h r

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.const_mul, NNReal.mk
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
r : ℝ
⊢ Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ r * X ω)
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HPow.hPow (β := ℕ) r 2) ⋯ * c) (Kernel.const Unit μ) (Measure.dirac ())

Tactic:
exact Kernel.HasSubgaussianMGF.const_mul h r

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.const_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
h : ∀ (t : ℝ), t ∈ integrableExpSet X μ ↔ Membership.mem (γ := Set ℝ) Set.univ t
⊢ integrableExpSet X μ = Set.univ

Tactic:
ext t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ t ∈ integrableExpSet X μ ↔ Membership.mem (γ := Set ℝ) Set.univ t

Tactic:
simpa using hX.integrable_exp_mul t

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
p : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet X μ)

Tactic:
simp [integrableExpSet_eq_univ hX]

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrableExpSet_eq_univ
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
⊢ 0 ∈ interior (integrableExpSet X μ)

Tactic:
simp [integrableExpSet_eq_univ hX]

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrableExpSet_eq_univ
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
ε : ℝ
hε : 0 ≤ ε
rw :
  ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
    {ε : ℝ} (hε : 0 ≤ ε), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))

Tactic:
simpa using h.measure_ge_le hε

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.measure_ge_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 μ
⊢ X =ᶠ[ae μ] 0

Tactic:
simpa using (HasSubgaussianMGF_iff_kernel.1 h).ae_eq_zero_of_hasSubgaussianMGF_zero

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel, Iff.mp, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
⊢ Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    (Kernel.const Unit μ) (Measure.dirac ())

Tactic:
have := (HasSubgaussianMGF_iff_kernel.1 hX).add (HasSubgaussianMGF_iff_kernel.1 hY)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
this :
  Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    (Kernel.const Unit μ) (Measure.dirac ())
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    μ

Tactic:
simpa [HasSubgaussianMGF_iff_kernel] using this

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) μ

Tactic:
simp_rw [mul_add, exp_add]

Premises used: mul_add, Real.exp_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (HMul.hMul (α := Ω → ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) fun (ω : Ω) ↦ rexp (t * Y ω)) μ

Tactic:
MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)

Premises used: MeasureTheory.MemLp.integrable_mul, ProbabilityTheory.HasSubgaussianMGF.memLp_exp_mul, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
convert! : (↑2 : ℝ≥0∞).HolderTriple (↑2 : ℝ≥0∞) 1
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ ENNReal.HolderTriple 2 2 1

Tactic:
infer_instance
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
hindep.mgf_add (hX.integrable_exp_mul t).1 (hY.integrable_exp_mul t).1

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul, And.left, ProbabilityTheory.IndepFun.mgf_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
c0 : 0 ≤ mgf Y μ t
h₁ : mgf X μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h₂ : mgf Y μ t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf X μ t * mgf Y μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
gcongr