awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (ε := ℝ) (m0 := mΩ'') (fun (ω : Ω'') ↦ rexp (t * Y ω)) (↑2 : ℝ≥0∞) ((⇑η : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)

Tactic:
have h := hY.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 * Y ω)) (↑2 : ℝ≥0∞) ((⇑η : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)
pos :
  ∀ (h : MemLp (ε := ℝ) (m0 := mΩ'') (fun (ω : Ω'') ↦ rexp (t * Y ω)) 2 ((⇑η : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)),
    MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
pos₁ :
  ∀
    (h :
      MemLp (ε := ℝ) (m0 := mΩ'') (fun (ω : Ω'') ↦ rexp (t * Y ω)) 2
        (Measure.snd.{u_1, u_3} (α := Ω) ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))),
    MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
pos₂ :
  ∀
    (h :
      MemLp (ε := ℝ) (m0 := mΩ'') (fun (ω : Ω'') ↦ rexp (t * Y ω)) 2
        (Measure.map (α := Ω × Ω'') Prod.snd ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))),
    MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
pos₃ pos₄ pos₅ pos₆ :
  ∀
    (h :
      MemLp (α := Ω × Ω'') (ε := ℝ) (m0 := Prod.instMeasurableSpace) ((fun (ω : Ω'') ↦ rexp (t * Y ω)) ∘ Prod.snd) 2
        ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)),
    MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
      ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)

Tactic:
rwa [ENNReal.coe_ofNat, Measure.comp_compProd_comm, Measure.snd,
      memLp_map_measure_iff h.1 measurable_snd.aemeasurable] at h

Premises used: MeasureTheory.Measure.comp_compProd_comm, Measurable.aemeasurable, MeasureTheory.Measure.snd, measurable_snd, ENNReal.coe_ofNat, MeasureTheory.memLp_map_measure_iff
-- 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 η (ν ⊗ₘ κ)
pos : ∀ (hκ : IsSFiniteKernel κ), HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
neg : ∀ (hκ : ¬IsSFiniteKernel κ), HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

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 η (ν ⊗ₘ κ)
hκ : ¬IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

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 η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

Tactic:
.of_rat (integrable_exp_add_compProd hX hY) fun q ↦ ?_

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

Tactic:
refine .of_rat (integrable_exp_add_compProd hX hY) fun q ↦ ?_
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
h :
  ∀ (ω' : Ω')
    (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)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
        (↑q : ℝ) ≤
      rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)

Tactic:
filter_upwards [hX.mgf_le, hX.ae_integrable_exp_mul q, Measure.ae_ae_of_ae_compProd hY.mgf_le,
    Measure.ae_integrable_of_integrable_comp <| integrable_exp_add_compProd hX hY q]
    with ω' hX_mgf hX_int hY_mgf h_int_mul

Premises used: MeasureTheory.Measure.ae_ae_of_ae_compProd, ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_add_compProd, Rat.cast, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le, MeasureTheory.Measure.ae_integrable_of_integrable_comp, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_integrable_exp_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 η (ν ⊗ₘ κ)
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 (Ω × Ω'')) ω')
simp_rw :
  ∀
    (h_int_mul :
      @Integrable ℝ _ _ _ Prod.instMeasurableSpace
        (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * X ω.1) * rexp ((↑q : ℝ) * Y ω.2))
        ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')),
    Eq (α := ℝ)
      (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω') fun (x : Ω × Ω'') ↦
        rexp ((↑q : ℝ) * X x.1) * rexp ((↑q : ℝ) * Y x.2))
      (@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 : ℝ) =
    @integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)

Tactic:
simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢

Premises used: mul_add, ProbabilityTheory.mgf, 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 η (ν ⊗ₘ κ)
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) * rexp ((↑q : ℝ) * Y ω.2))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
simp_rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦
        rexp ((↑q : ℝ) * X x) * rexp ((↑q : ℝ) * Y y))
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω') fun (x : Ω × Ω'') ↦
      rexp ((↑q : ℝ) * X x.1) * rexp ((↑q : ℝ) * Y x.2))
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y))

Tactic:
simp_rw [integral_compProd h_int_mul, integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, ProbabilityTheory.integral_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 η (ν ⊗ₘ κ)
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 (Ω × Ω'')) ω')
⊢ 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:
integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_

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

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

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

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

Tactic:
exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity)
        (integral_nonneg (fun _ ↦ by positivity))

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

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

Tactic:
hY_mgf

Premises used: ProbabilityTheory.mgf