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 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 : ℝ
h₁ :
  (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2)
⊢ HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑p : ℝ) * X x))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x))
        (1 / (↑q : ℝ)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ))
have h₂ : (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * (↑q : ℝ) * Y x)) ≤
  rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑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 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 : ℝ
⊢ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑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)
have simp_rw : 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_rw [← exp_mul, ← 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 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 : ℝ
⊢ 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)
have 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
Tactic: simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, 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 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 : ℝ
⊢ (↑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
have field_simp : HPow.hPow (β := ℕ) t 2 * ((↑cX : ℝ) * √(↑cY : ℝ) + √(↑cX : ℝ) * (↑cY : ℝ)) =
  HPow.hPow (β := ℕ) t 2 * √(↑cX : ℝ) * √(↑cY : ℝ) * (√(↑cX : ℝ) + √(↑cY : ℝ))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 : ℝ
⊢ mgf (m := mΩ) (fun (ω : Ω) ↦ X ω + Y ω) ((κ : (a : Ω') → Measure Ω) ω') t ≤
    rexp
      ((↑(HPow.hPow (β := ℕ)
                (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
                  ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
                2) :
            ℝ) *
          HPow.hPow (β := ℕ) t 2 /
        2)
have calc : (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) x) ≤
  HPow.hPow (α := ℝ)
      (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * X ω) ^ (↑p : ℝ)) x)
      (1 / (↑p : ℝ)) *
    HPow.hPow (α := ℝ)
      (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ (fun (ω : Ω) ↦ rexp (t * Y ω) ^ (↑q : ℝ)) x)
      (1 / (↑q : ℝ))
Tactic: 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)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 Ω) ∘ₘ ν)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
have pos : ∀ (hν : SFinite ν), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Tactic: by_cases hν : SFinite ν
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 Ω' η) (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
have neg : ∀ (hν : ¬SFinite ν), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Tactic: by_cases hν : SFinite ν
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 Ω' η) (ν ⊗ₘ κ)
have pos : ∀ (hκ : IsSFiniteKernel κ), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 Ω' η) (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
Tactic: by_cases hκ : IsSFiniteKernel κ
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 Ω' η) (ν ⊗ₘ κ)
have pos : ∀ (t : ℝ),
  @Integrable ℝ _ _ _ mΩ'' (fun (ω : Ω'') ↦ rexp (t * Y ω))
    ((⇑(prodMkLeft Ω' η) : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 Ω'') ∘ₘ ν ⊗ₘ κ)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)
have pos₁ : ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ,
  ∀ (t : ℝ),
    mgf (m := mΩ'') Y ((prodMkLeft Ω' η : (a : Ω' × Ω) → Measure Ω'') ω') t ≤
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 : ℝ),
      mgf (m := mΩ'') Y ((prodMkLeft Ω' η : (a : Ω' × Ω) → Measure Ω'') ω') t ≤
        rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h2 : ∀ᵐ (ω' : Ω) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν,
  ∀ (t : ℝ), mgf (m := mΩ'') Y ((η : (a : Ω) → Measure Ω'') ω') t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: have h2 := h.mgf_le
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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)
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ,
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((prodMkLeft Ω' η : (a : Ω' × Ω) → Measure Ω'') ω') t ≤
        rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h2₁ : ∀ᵐ (ω' : Ω) ∂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
Cleared hypotheses: h2
-- 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 η (ν ⊗ₘ κ)
t : ℝ
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have pos : ∀ (hκ : IsSFiniteKernel κ),
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
Tactic: by_cases hκ : IsSFiniteKernel κ
-- 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 η (ν ⊗ₘ κ)
t : ℝ
pos :
  ∀ (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 (Ω × Ω'')) ∘ₘ ν)
have neg : ∀ (hκ : ¬IsSFiniteKernel κ),
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
Tactic: by_cases hκ : IsSFiniteKernel κ
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have 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 (Ω × Ω'')) ∘ₘ ν)
Tactic: rcases eq_zero_or_isMarkovKernel η with rfl | hη
Cleared hypotheses: η, inst_1, hY
-- 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 η (ν ⊗ₘ κ)
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 (Ω × Ω'')) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have pos₁ : ∀ (hη : IsMarkovKernel η),
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
Tactic: rcases eq_zero_or_isMarkovKernel η with rfl | hη
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * (X ω.1 + Y ω.2)))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have pos : @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1) * rexp (t * Y ω.2))
  ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
Tactic: simp_rw [mul_add, 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1) * rexp (t * Y ω.2))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have pos : MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
  ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
Tactic: refine MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_
-- 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 η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
pos :
  MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1) * rexp (t * Y ω.2))
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have pos₁ : MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
  ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
Tactic: refine MemLp.integrable_mul (p := 2) (q := 2) ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have h : MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑2 : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: have h := hX.memLp_exp_mul t 2
-- 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 η (ν ⊗ₘ κ)
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 (Ω × Ω'')) ∘ₘ ν))
have rw : Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
  ((⇑((κ ⊗ₖ η).map Prod.fst) : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]