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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf_1 :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
ω : Ω
hY_mgf :
  mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', ω)) (↑q : ℝ) ≤
    rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
⊢ (@integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', ω)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)) ≤
    rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
exact hY_mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
rw :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (a : Ω) ↦ rexp ((↑q : ℝ) * X a)) *
      rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2) ≤
    rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2) *
      rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]

Premises used: add_mul, NNReal.coe_add, Real.exp_add, MeasureTheory.integral_mul_const, add_div
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
hbc :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (a : Ω) ↦ rexp ((↑q : ℝ) * X a)) ≤
    rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (a : Ω) ↦ rexp ((↑q : ℝ) * X a)) *
      rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2) ≤
    rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2) *
      rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (a : Ω) ↦ rexp ((↑q : ℝ) * X a)) ≤
    rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
hX_mgf q

Premises used: Rat.cast, ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (a : Ω) ↦ rexp ((↑q : ℝ) * X a)) ≤
    rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
exact hX_mgf q

Premises used: Rat.cast
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
calc :
  mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
      (↑q : ℝ) =
    @integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)
calc₁ :
  LE.le (α := ℝ)
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y))
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2))
calc₂ :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
⊢ mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
      (↑q : ℝ) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
calc mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') q
  _ = ∫ x, exp (q * X x) * ∫ y, exp (q * Y y) ∂(η (ω', x)) ∂(κ ω') := by
    simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢
    simp_rw [integral_compProd h_int_mul, integral_const_mul]
  _ ≤ ∫ x, exp (q * X x) * exp (cY * q ^ 2 / 2) ∂(κ ω') := by
    refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
    · exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity)
        (integral_nonneg (fun _ ↦ by positivity))
    · filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
      gcongr
      exact hY_mgf
  _ ≤ exp (↑(c + cY) * q ^ 2 / 2) := by
    rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
    gcongr
    exact hX_mgf q

Premises used: HMul.hMul, HDiv.hDiv, Rat.cast, Real.exp, HPow.hPow, HAdd.hAdd, ProbabilityTheory.mgf, OfNat.ofNat, DFunLike.coe, NNReal.toReal, ProbabilityTheory.Kernel.compProd
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel Ω Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ prodMkLeft Ω' η) ν

Tactic:
hX.add_compProd hY.prodMkLeft_compProd

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.add_compProd, ProbabilityTheory.Kernel.HasSubgaussianMGF.prodMkLeft_compProd
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm,
    ∀ (t : ℝ),
      mgf (m := mΩ) X ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
Kernel.HasSubgaussianMGF.mgf_le h

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm,
    ∀ (t : ℝ), cgf (m := mΩ) X ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
Kernel.HasSubgaussianMGF.cgf_le h

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.cgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
⊢ (ae (Measure.trim ((⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm) hm)).EventuallyEq (β := ℝ)
    (condExp m (m₀ := mΩ) ((⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm) fun (ω : Ω) ↦ rexp (t * X ω))
    fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ
      ((condExpKernel ((⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm) m : (a : Ω) → Measure Ω) ω)
      fun (y : Ω) ↦ rexp (t * X y)

Tactic:
have h_eq := condExp_ae_eq_trim_integral_condExpKernel hm (h.integrable_exp_mul t)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq :
  (ae (Measure.trim ((⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm) hm)).EventuallyEq (β := ℝ)
    (condExp m (m₀ := mΩ) ((⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm) fun (ω : Ω) ↦ rexp (t * X ω))
    fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ
      ((condExpKernel ((⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm) m : (a : Ω) → Measure Ω) ω)
      fun (y : Ω) ↦ rexp (t * X y)
⊢ (ae (μ.trim hm)).EventuallyEq (β := ℝ) μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (ω : Ω) ↦ rexp (t * X ω)

Tactic:
simp_rw [condExpKernel_comp_trim] at h_eq

Premises used: ProbabilityTheory.condExpKernel_comp_trim
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq :
  (ae (μ.trim hm)).EventuallyEq (β := ℝ) μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (ω : Ω) ↦ rexp (t * X ω)
h₁ :
  ∀ (ω' : Ω)
    (h_mgf :
      ∀ (t : ℝ),
        mgf (m := mΩ) X ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (h_eq :
      Eq (α := ℝ) (μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω')
        (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω))),
    μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
filter_upwards [h.mgf_le, h_eq] with ω' h_mgf h_eq

Premises used: ProbabilityTheory.HasCondSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq_1 :
  (ae (μ.trim hm)).EventuallyEq (β := ℝ) μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (ω : Ω) ↦ rexp (t * X ω)
ω' : Ω
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_eq :
  Eq (α := ℝ) (μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω')
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω))
h₁ :
  (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω)) ≤
    rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [h_eq]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq_1 :
  (ae (μ.trim hm)).EventuallyEq (β := ℝ) μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (ω : Ω) ↦ rexp (t * X ω)
ω' : Ω
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_eq :
  Eq (α := ℝ) (μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω')
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω))
⊢ (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω)) ≤
    rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h_mgf t

Premises used: ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq_1 :
  (ae (μ.trim hm)).EventuallyEq (β := ℝ) μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (ω : Ω) ↦ rexp (t * X ω)
ω' : Ω
h_mgf :
  ∀ (t : ℝ),
    mgf (m := mΩ) X ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_eq :
  Eq (α := ℝ) (μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω')
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω))
⊢ (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω)) ≤
    rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact h_mgf t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
⊢ ∀ᵐ (ω' : Ω) ∂μ, μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
ae_of_ae_trim hm (h.ae_trim_condExp_le t)

Premises used: MeasureTheory.ae_of_ae_trim, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ HasCondSubgaussianMGF m hm (fun (x : Ω) ↦ 0) 0 μ

Tactic:
Kernel.HasSubgaussianMGF.fun_zero

Premises used: ProbabilityTheory.HasCondSubgaussianMGF, ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ HasCondSubgaussianMGF m hm 0 0 μ

Tactic:
Kernel.HasSubgaussianMGF.zero

Premises used: ProbabilityTheory.HasCondSubgaussianMGF, ProbabilityTheory.Kernel.HasSubgaussianMGF.zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
p : ℝ≥0
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) μ

Tactic:
condExpKernel_comp_trim (μ := μ) hm ▸ Kernel.HasSubgaussianMGF.memLp_exp_mul h t p

Premises used: ProbabilityTheory.condExpKernel_comp_trim, ProbabilityTheory.Kernel.HasSubgaussianMGF.memLp_exp_mul, Eq.rec
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
condExpKernel_comp_trim (μ := μ) hm ▸ Kernel.HasSubgaussianMGF.integrable_exp_mul h t

Premises used: ProbabilityTheory.condExpKernel_comp_trim, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, Eq.rec
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
h1 : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h2 : ∀ (t : ℝ), mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ (t : ℝ),
    @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω))
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))

Tactic:
simpa
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
h1 : ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h2 : ∀ (t : ℝ), mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Unit) ∂Measure.dirac (),
    ∀ (t : ℝ),
      mgf (m := mΩ) X ((Kernel.const Unit μ : (a : Unit) → Measure Ω) ω') t ≤
        rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simpa
-- 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 ())
h1 :
  ∀ (t : ℝ),
    @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω))
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))
h2 :
  ∀ᵐ (ω' : Unit) ∂Measure.dirac (),
    ∀ (t : ℝ),
      mgf (m := mΩ) X ((Kernel.const Unit μ : (a : Unit) → Measure Ω) ω') t ≤
        rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ (t : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
simpa using h1
-- 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 ())
h1 :
  ∀ (t : ℝ),
    @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω))
      (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
        (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))
h2 :
  ∀ᵐ (ω' : Unit) ∂Measure.dirac (),
    ∀ (t : ℝ),
      mgf (m := mΩ) X ((Kernel.const Unit μ : (a : Unit) → Measure Ω) ω') t ≤
        rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ (t : ℝ), mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simpa using h2
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (1 * X ω)) μ

Tactic:
have h_int := h.integrable_exp_mul 1
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (1 * X ω)) μ
⊢ AEStronglyMeasurable X μ

Tactic:
simpa using (aemeasurable_of_aemeasurable_exp h_int.1.aemeasurable).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Real.aemeasurable_of_aemeasurable_exp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ AEMeasurable X μ

Tactic:
h.aestronglyMeasurable.aemeasurable

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ProbabilityTheory.HasSubgaussianMGF.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
Y : Ω → ℝ
h' : X =ᶠ[ae μ] Y
rw :
  ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
    {Y : Ω → ℝ} (h' : X =ᶠ[ae μ] Y),
    Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) Y c (Kernel.const Unit μ) (Measure.dirac ())
⊢ HasSubgaussianMGF Y c μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h ⊢

Premises used: ProbabilityTheory.HasSubgaussianMGF_iff_kernel