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 Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
simp :
  (↑cX : ℝ) * HPow.hPow (β := ℕ) (t * ((√(↑cX : ℝ) + √(↑cY : ℝ)) / √(↑cX : ℝ))) 2 / 2 *
        (√(↑cX : ℝ) / (√(↑cX : ℝ) + √(↑cY : ℝ))) +
      (↑cY : ℝ) * HPow.hPow (β := ℕ) (t * ((√(↑cX : ℝ) + √(↑cY : ℝ)) / √(↑cY : ℝ))) 2 / 2 *
        (√(↑cY : ℝ) / (√(↑cX : ℝ) + √(↑cY : ℝ))) =
    HPow.hPow (β := ℕ) (√(↑cX : ℝ) + √(↑cY : ℝ)) 2 * HPow.hPow (β := ℕ) t 2 / 2
⊢ rexp
      ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2 * (1 / (↑p : ℝ)) +
        (↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2 * (1 / (↑q : ℝ))) =
    rexp
      (HPow.hPow (β := ℕ) ((↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX) : ℝ) + (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY) : ℝ))
            2 *
          HPow.hPow (β := ℕ) t 2 /
        2)

Tactic:
simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]

Premises used: Real.exp_eq_exp, NNReal.coe_add, NNReal.coe_div, one_div, inv_div, Real.coe_sqrt
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
field_simp :
  HPow.hPow (β := ℕ) t 2 * ((↑cX : ℝ) * √(↑cY : ℝ) + √(↑cX : ℝ) * (↑cY : ℝ)) =
    HPow.hPow (β := ℕ) t 2 * √(↑cX : ℝ) * √(↑cY : ℝ) * (√(↑cX : ℝ) + √(↑cY : ℝ))
⊢ (↑cX : ℝ) * HPow.hPow (β := ℕ) (t * ((√(↑cX : ℝ) + √(↑cY : ℝ)) / √(↑cX : ℝ))) 2 / 2 *
        (√(↑cX : ℝ) / (√(↑cX : ℝ) + √(↑cY : ℝ))) +
      (↑cY : ℝ) * HPow.hPow (β := ℕ) (t * ((√(↑cX : ℝ) + √(↑cY : ℝ)) / √(↑cY : ℝ))) 2 / 2 *
        (√(↑cY : ℝ) / (√(↑cX : ℝ) + √(↑cY : ℝ))) =
    HPow.hPow (β := ℕ) (√(↑cX : ℝ) + √(↑cY : ℝ)) 2 * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
field_simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
q : ℝ≥0 :=
  HDiv.hDiv (β := ℝ≥0)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0)
ω' : Ω'
hmX : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hmY : ∀ (t : ℝ), mgf (m := mΩ) Y ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hlX : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
hlY : ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * Y ω)) (↑q : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ HPow.hPow (β := ℕ) t 2 * ((↑cX : ℝ) * √(↑cY : ℝ) + √(↑cX : ℝ) * (↑cY : ℝ)) =
    HPow.hPow (β := ℕ) t 2 * √(↑cX : ℝ) * √(↑cY : ℝ) * (√(↑cX : ℝ) + √(↑cY : ℝ))

Tactic:
linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg)

Premises used: HMul.hMul, HSub.hSub, Real.sqrt, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
⊢ 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:
exact
  { integrable_exp_mul t := by
      simp_rw [mul_add, exp_add]
      convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
      norm_cast
      infer_instance
    mgf_le := by
      let p := (cX.sqrt + cY.sqrt) / cX.sqrt
      let q := (cX.sqrt + cY.sqrt) / cY.sqrt
      filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p,
        hY.ae_forall_memLp_exp_mul q] with ω' hmX hmY hlX hlY t
      calc (κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
      _ ≤ (κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
          (κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) := by
        simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)
      _ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) *
          exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) := by
        simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
        gcongr
        · exact hmX (t * p)
        · exact hmY (t * q)
      _ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) := by
        simp_rw [← exp_mul, ← exp_add]
        simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
        field_simp
        linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg
            -√↑cX * Real.sq_sqrt cY.coe_nonneg) }
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
pos : ∀ (hν : SFinite ν), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
neg : ∀ (hν : ¬SFinite ν), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
by_cases hν : SFinite ν

Premises used: MeasureTheory.SFinite
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : ¬SFinite ν
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
simp [hν]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
pos : ∀ (hκ : IsSFiniteKernel κ), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
neg : ∀ (hκ : ¬IsSFiniteKernel κ), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : ¬IsSFiniteKernel κ
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
simp [hκ]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
pos :
  ∀ (t : ℝ),
    @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * Y ω))
      ((⇑(prodMkLeft Ω' η) : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)
pos₁ :
  ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ,
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((prodMkLeft Ω' η : (a : Ω' × Ω) → Measure Ω'') ω') t ≤
        rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ (t : ℝ),
    @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * Y ω))
      ((⇑(prodMkLeft Ω' η) : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)

Tactic:
simpa using h.integrable_exp_mul

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 Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (ω' : Ω) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν,
    ∀ (t : ℝ), mgf (m := mΩ'') Y ((η : (a : Ω) → Measure Ω'') ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
have h2 := h.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 :
  ∀ᵐ (ω' : Ω) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν,
    ∀ (t : ℝ), mgf (m := mΩ'') Y ((η : (a : Ω) → Measure Ω'') ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ),
    ∀ (t : ℝ), mgf (m := mΩ'') Y ((η : (a : Ω) → Measure Ω'') ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [← Measure.snd_compProd, Measure.snd] at h2

Premises used: MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.snd
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 :
  ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ),
    ∀ (t : ℝ), mgf (m := mΩ'') Y ((η : (a : Ω) → Measure Ω'') ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ AEMeasurable Prod.snd (ν ⊗ₘ κ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 :
  ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ),
    ∀ (t : ℝ), mgf (m := mΩ'') Y ((η : (a : Ω) → Measure Ω'') ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ,
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((prodMkLeft Ω' η : (a : Ω' × Ω) → Measure Ω'') ω') t ≤
        rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact ae_of_ae_map (by fun_prop) h2

Premises used: MeasureTheory.ae_of_ae_map
-- 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 η (ν ⊗ₘ κ)
t : ℝ
pos :
  ∀ (hκ : IsSFiniteKernel κ),
    @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
neg :
  ∀ (hκ : ¬IsSFiniteKernel κ),
    @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
by_cases hκ : IsSFiniteKernel κ

Premises used: ProbabilityTheory.IsSFiniteKernel
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : ¬IsSFiniteKernel κ
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
simp [hκ]
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
pos :
  ∀ [IsZeroOrMarkovKernel (α := Ω' × Ω) (β := Ω'') (mα := Prod.instMeasurableSpace) (mβ := mΩ'') 0]
    (hY : HasSubgaussianMGF (mΩ := mΩ'') Y cY 0 (ν ⊗ₘ κ)),
    @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
      ((⇑(κ ⊗ₖ 0) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
pos₁ :
  ∀ (hη : IsMarkovKernel η),
    @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
rcases eq_zero_or_isMarkovKernel η with rfl | hη

Premises used: ProbabilityTheory.eq_zero_or_isMarkovKernel, rfl
-- 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 ν
hX : HasSubgaussianMGF X c κ ν
t : ℝ
hκ : IsSFiniteKernel κ
inst_1 : IsZeroOrMarkovKernel (α := Ω' × Ω) (β := Ω'') (mα := Prod.instMeasurableSpace) (mβ := mΩ'') 0
hY : HasSubgaussianMGF (mΩ := mΩ'') Y cY 0 (ν ⊗ₘ κ)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ 0) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
simp
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
pos :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1) * rexp (t * Y ω.2))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
simp_rw [mul_add, exp_add]

Premises used: mul_add, Real.exp_add
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1) * rexp (t * Y ω.2))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_

Premises used: MeasureTheory.MemLp.integrable_mul
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
pos :
  MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
pos₁ :
  MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1) * rexp (t * Y ω.2))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
refine MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_

Premises used: MeasureTheory.MemLp.integrable_mul
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑2 : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
have h := hX.memLp_exp_mul t 2
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) 2 ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
rw :
  Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    ((⇑((κ ⊗ₖ η).map Prod.fst) : (a : Ω') → Measure Ω) ∘ₘ ν)
rw₁ : Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) ((⇑(κ ⊗ₖ η).fst : (a : Ω') → Measure Ω) ∘ₘ ν)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))

Tactic:
rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]

Premises used: MeasureTheory.Measure.map_comp, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.fst_compProd, measurable_fst
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) 2 ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))

Tactic:
have : κ ∘ₘ ν = ((κ ⊗ₖ η) ∘ₘ ν).map Prod.fst := by
      rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) 2 ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
this :
  Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))
pos :
  ∀
    (h :
      MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) 2
        (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)))
    (this :
      Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
        (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))),
    MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
pos₁ pos₂ pos₃ pos₄ :
  ∀
    (h :
      MemLp (α := Ω × Ω'') (ε := ℝ) (m0 := Prod.instMeasurableSpace) ((fun (ω : Ω) ↦ rexp (t * X ω)) ∘ Prod.fst) 2
        ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))
    (this :
      Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
        (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))),
    MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
rwa [this, memLp_map_measure_iff h.1 measurable_fst.aemeasurable] at h

Premises used: Measurable.aemeasurable, measurable_fst, MeasureTheory.memLp_map_measure_iff