awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 (Ω × Ω'')) ω')
refine_1 :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (x : Ω) ↦
    rexp ((↑q : ℝ) * X x) *
      @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)
⊢ 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))
have refine_2 : (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ)
  (fun (x : Ω) ↦
    rexp ((↑q : ℝ) * X x) *
      @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y))
  fun (x : Ω) ↦ rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
Tactic: refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 (Ω × Ω'')) ω')
⊢ (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ)
    (fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y))
    fun (x : Ω) ↦ rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have h : ∀ (ω : Ω)
  (hY_mgf :
    mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', ω)) (↑q : ℝ) ≤
      rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)),
  (rexp ((↑q : ℝ) * X ω) *
      @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', ω)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)) ≤
    rexp ((↑q : ℝ) * X ω) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
Tactic: filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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)
⊢ (rexp ((↑q : ℝ) * X ω) *
      @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', ω)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)) ≤
    rexp ((↑q : ℝ) * X ω) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have h : (@integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', ω)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)) ≤
  rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have 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)
Tactic: rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2) ≤
    rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2) *
      rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have hbc : (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (a : Ω) ↦ rexp ((↑q : ℝ) * X a)) ≤
  rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 (Ω × Ω'')) ω')
⊢ mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
      (↑q : ℝ) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have 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)
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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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)
⊢ mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
      (↑q : ℝ) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have 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))
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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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))
⊢ mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
      (↑q : ℝ) ≤
    rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have 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)
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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 : ℝ
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have 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)
Tactic: have h_eq := condExp_ae_eq_trim_integral_condExpKernel hm (h.integrable_exp_mul t)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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)
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h_eq₁ : (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
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ω)
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have 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)
Tactic: filter_upwards [h.mgf_le, h_eq] with ω' h_mgf h_eq
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ω))
⊢ μ[fun (ω : Ω) ↦ rexp (t * X ω) | m] ω' ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω') fun (ω : Ω) ↦ rexp (t * X ω)) ≤
  rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
⊢ AEStronglyMeasurable X μ
have h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (1 * X ω)) μ
Tactic: have h_int := h.integrable_exp_mul 1
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
Y : Ω → ℝ
h' : X =ᶠ[ae μ] Y
⊢ HasSubgaussianMGF Y c μ
have 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 ())
Tactic: rw [HasSubgaussianMGF_iff_kernel] at h ⊢
Cleared hypotheses: h, Y, h'
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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
⊢ Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) Y c (Kernel.const Unit μ) (Measure.dirac ())
have apply : X =ᶠ[ae (F := Measure Ω)
    (Measure.bind (mα := PUnit.instMeasurableSpace) (Measure.dirac ())
      (⇑(Kernel.const Unit μ) : (a : Unit) → Measure Ω))]
  Y
Tactic: apply h.congr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
p : ℝ≥0
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) μ
have rw : ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())) (t : ℝ)
  (p : ℝ≥0), MemLp (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) μ
Tactic: rw [HasSubgaussianMGF_iff_kernel] at h
Cleared hypotheses: h, t, p
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ cgf X μ t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have rw : ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
  (t : ℝ), cgf X μ t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [HasSubgaussianMGF_iff_kernel] at h
Cleared hypotheses: h, t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * (X ∘ Y) ω)) μ
have h1 : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (Measure.map Y μ)
Tactic: have h1 := h.integrable_exp_mul t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 μ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * (X ∘ Y) ω)) μ
have rwa : ∀ (h1 : Integrable (ε := ℝ) ((fun (ω : Ω) ↦ rexp (t * X ω)) ∘ Y) μ),
  Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * (X ∘ Y) ω)) μ
Tactic: rwa [integrable_map_measure h1.aestronglyMeasurable (by fun_prop)] at h1
Cleared hypotheses: h1