awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
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 Ω) ∘ₘ ν)
⊢ Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))
have rw₁ : Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) ((⇑(κ ⊗ₖ η).fst : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]
-- 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 Ω) ∘ₘ ν)
rw :
  Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    ((⇑((κ ⊗ₖ η).map Prod.fst) : (a : Ω') → Measure Ω) ∘ₘ ν)
rw₁ : Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) ((⇑(κ ⊗ₖ η).fst : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
    (Measure.map (α := Ω × Ω'') Prod.fst ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν))
have rw₂ : Eq.{u_1 + 1} (α := Measure Ω) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]
-- 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 η
h : MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) 2 ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have this : 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]
-- 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 Ω) ∘ₘ ν)
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 (Ω × Ω'')) ∘ₘ ν)
have 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 (Ω × Ω'')) ∘ₘ ν)
Tactic: rwa [this, memLp_map_measure_iff h.1 measurable_fst.aemeasurable] at h
Cleared hypotheses: h, this
-- 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 Ω) ∘ₘ ν)
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 (Ω × Ω'')) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * X ω.1)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have 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 (Ω × Ω'')) ∘ₘ ν)
Tactic: rwa [this, memLp_map_measure_iff h.1 measurable_fst.aemeasurable] at h
Cleared hypotheses: h, this
-- 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 * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have h : MemLp (ε := ℝ) (m0 := mΩ'') (fun (ω : Ω'') ↦ rexp (t * Y ω)) (↑2 : ℝ≥0∞) ((⇑η : (a : Ω' × Ω) → Measure Ω'') ∘ₘ ν ⊗ₘ κ)
Tactic: have h := 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 : Ω → ℝ
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 Ω'') ∘ₘ ν ⊗ₘ κ)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have pos : ∀ (h : MemLp (ε := ℝ) (m0 := mΩ'') (fun (ω : Ω'') ↦ rexp (t * Y ω)) 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
Cleared hypotheses: 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 η
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 (Ω × Ω'')) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have 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 (Ω × Ω'')) ∘ₘ ν)
Tactic: rwa [ENNReal.coe_ofNat, Measure.comp_compProd_comm, Measure.snd,
      memLp_map_measure_iff h.1 measurable_snd.aemeasurable] at h
Cleared hypotheses: 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 η
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 (Ω × Ω'')) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have 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 (Ω × Ω'')) ∘ₘ ν)
Tactic: rwa [ENNReal.coe_ofNat, Measure.comp_compProd_comm, Measure.snd,
      memLp_map_measure_iff h.1 measurable_snd.aemeasurable] at h
Cleared hypotheses: 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 η
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 (Ω × Ω'')) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := Prod.instMeasurableSpace) (fun (ω : Ω × Ω'') ↦ rexp (t * Y ω.2)) 2
    ((⇑(κ ⊗ₖ η) : (a : Ω') → Measure (Ω × Ω'')) ∘ₘ ν)
have 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 (Ω × Ω'')) ∘ₘ ν)
Tactic: rwa [ENNReal.coe_ofNat, Measure.comp_compProd_comm, Measure.snd,
      memLp_map_measure_iff h.1 measurable_snd.aemeasurable] at h
Cleared hypotheses: 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 η (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
have pos : ∀ (hκ : IsSFiniteKernel κ), HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
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 η (ν ⊗ₘ κ)
pos : ∀ (hκ : IsSFiniteKernel κ), HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
have neg : ∀ (hκ : ¬IsSFiniteKernel κ), HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
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 η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
⊢ HasSubgaussianMGF (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν
have 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)
Tactic: refine .of_rat (integrable_exp_add_compProd hX hY) fun q ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
        (↑q : ℝ) ≤
      rexp ((↑(c + cY) : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
have 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)
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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
⊢ mgf (m := Prod.instMeasurableSpace) (fun (p : Ω × Ω'') ↦ X p.1 + Y p.2) ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
      (↑q : ℝ) =
    @integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y)
have 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))
Tactic: simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢
Cleared hypotheses: h_int_mul
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * X ω.1) * 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))
have 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))
Tactic: simp_rw [integral_compProd h_int_mul, integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst_1 : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
hX_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp ((↑q : ℝ) * X y)) ((κ : (a : Ω') → Measure Ω) ω')
hY_mgf :
  ∀ᵐ (b : Ω) ∂((κ : (a : Ω') → Measure Ω) ω' : Measure Ω),
    ∀ (t : ℝ),
      mgf (m := mΩ'') Y ((η : (a : Ω' × Ω) → Measure Ω'') (ω', b)) t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int_mul :
  @Integrable ℝ _ _ _ Prod.instMeasurableSpace (fun (ω : Ω × Ω'') ↦ rexp ((↑q : ℝ) * (X ω.1 + Y ω.2)))
    ((κ ⊗ₖ η : (a : Ω') → Measure (Ω × Ω'')) ω')
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) *
        @integral _ _ _ _ mΩ'' ((η : (a : Ω' × Ω) → Measure Ω'') (ω', x)) fun (y : Ω'') ↦ rexp ((↑q : ℝ) * Y y))
    (@integral _ _ _ _ mΩ ((κ : (a : Ω') → Measure Ω) ω') fun (x : Ω) ↦
      rexp ((↑q : ℝ) * X x) * rexp ((↑cY : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2))
have refine_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)
Tactic: refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_