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
⊢ 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)
    κ ν
have pos : ∀ (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: by_cases hY0 : cY = 0
-- 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
pos :
  ∀ (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)
      κ ν
⊢ 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)
    κ ν
have neg : ∀ (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: by_cases hY0 : cY = 0
-- 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
⊢ 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)
    κ ν
have pos : ∀ (hY : HasSubgaussianMGF Y 0 κ ν), HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cX κ ν
Tactic: simp only [hY0, NNReal.sqrt_zero, add_zero, NNReal.sq_sqrt] at hY ⊢
Cleared hypotheses: 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 Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω) cX κ ν
have pos : X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
Tactic: refine hX.congr ?_
-- 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 κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
have h : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ Y x = 0 x) x} x →
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = (fun (ω : Ω) ↦ X ω + Y ω) x) x} x}
    a
Tactic: filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hY] with ω hY0 using by simp [hY0]
-- 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 κ ν
hX0 : ¬cX = 0
hY0 : cY = 0
hY : HasSubgaussianMGF Y 0 κ ν
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ Y x = 0 x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = (fun (ω : Ω) ↦ X ω + Y ω) x) x} x}
      a
⊢ X =ᶠ[ae (F := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)] fun (ω : Ω) ↦ X ω + Y ω
have h₁ : ∀ (a : Ω), Y a = 0 a → X a = X a + Y a
Tactic: filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hY] with ω hY0 using by simp [hY0]
-- 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
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have simp_rw : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) ((⇑κ : (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 Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have convert! : (↑2 : ℝ≥0∞).HolderTriple (↑2 : ℝ≥0∞) 1
Tactic: convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.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 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)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (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 h : ∀ (ω' : Ω')
  (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)
Tactic: 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
-- 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 : ℝ
⊢ (@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 : ℝ))
have simp_rw : (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
  HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
      (1 / (↑p : ℝ)) *
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
      (1 / (↑q : ℝ))
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 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 : ℝ
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))
have hpq : (↑p : ℝ).HolderConjugate (↑q : ℝ)
Tactic: apply integral_mul_le_Lp_mul_Lq_of_nonneg
-- 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 : ℝ
hpq : (↑p : ℝ).HolderConjugate (↑q : ℝ)
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))
have hf_nonneg : (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)
Tactic: apply integral_mul_le_Lp_mul_Lq_of_nonneg
-- 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 : ℝ
hpq : (↑p : ℝ).HolderConjugate (↑q : ℝ)
hf_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))
have hg_nonneg : (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * Y a)
Tactic: apply integral_mul_le_Lp_mul_Lq_of_nonneg
-- 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 : ℝ
hpq : (↑p : ℝ).HolderConjugate (↑q : ℝ)
hf_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)
hg_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * Y a)
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))
have hf : MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * X a)) (ENNReal.ofReal (↑p : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: apply integral_mul_le_Lp_mul_Lq_of_nonneg
-- 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 : ℝ
hpq : (↑p : ℝ).HolderConjugate (↑q : ℝ)
hf_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * X a)
hg_nonneg :
  (ae (F := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω)).EventuallyLE (β := ℝ) 0 fun (a : Ω) ↦ rexp (t * Y a)
hf : MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * X a)) (ENNReal.ofReal (↑p : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) * rexp (t * Y x)) ≤
    HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * X x) ^ (↑p : ℝ))
        (1 / (↑p : ℝ)) *
      HPow.hPow (α := ℝ) (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦ rexp (t * Y x) ^ (↑q : ℝ))
        (1 / (↑q : ℝ))
have hg : MemLp (ε := ℝ) (m0 := mΩ) (fun (a : Ω) ↦ rexp (t * Y a)) (ENNReal.ofReal (↑q : ℝ)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: apply integral_mul_le_Lp_mul_Lq_of_nonneg
-- 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 : ℝ
⊢ 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 : ℝ)) ≤
    rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2) ^ (1 / (↑p : ℝ)) *
      rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) (t * (↑q : ℝ)) 2 / 2) ^ (1 / (↑q : ℝ))
have simp_rw : 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 : ℝ))
Tactic: simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ 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 : ℝ
⊢ 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 * (↑p : ℝ) * X x)) ≤
  rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) (t * (↑p : ℝ)) 2 / 2)
Tactic: gcongr