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
h : HasSubgaussianMGF X c κ ν
h_int_1 : ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω')
ω : Ω'
h_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω)
⊢ AEStronglyMeasurable (m₀ := mΩ) X ((κ : (a : Ω') → Measure Ω) ω)

Tactic:
simpa using (aemeasurable_of_aemeasurable_exp h_int.1.aemeasurable).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Real.aemeasurable_of_aemeasurable_exp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ ∀ (n : ℤ),
    ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
have h_int (n : ℤ) : ∀ᵐ ω' ∂ν, Integrable (fun ω ↦ exp (n * X ω)) (κ ω') :=
    h.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
h : HasSubgaussianMGF X c κ ν
h_int :
  ∀ (n : ℤ),
    ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)

Tactic:
rw [← ae_all_iff] at h_int

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
h₁ :
  ∀ (ω' : Ω')
    (h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω'))
    (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
filter_upwards [h_int] with ω' h_int t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int_1 :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
ω' : Ω'
h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)

Premises used: Int.le_ceil, ProbabilityTheory.integrable_exp_mul_of_le_of_le, Int.floor_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int_1 :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
ω' : Ω'
h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)

Premises used: Int.le_ceil, ProbabilityTheory.integrable_exp_mul_of_le_of_le, Int.floor_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
h₁ :
  ∀ (ω' : Ω') (hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω'))
    (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
filter_upwards [h.ae_forall_integrable_exp_mul] with ω' hi t

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h₁ : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h₂ : @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
(hi t).1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
exact (hi t).1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
pos : ∀ (hp : p = 0), @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
neg : ∀ (hp : ¬p = 0), @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : p = 0
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞

Tactic:
simp [hp]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
⊢ (↑p : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
neg : ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp),
      ENNReal.coe_toReal]

Premises used: ENNReal.coe_toReal, MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞

Tactic:
have hf := (hi (p * t)).lintegral_lt_top
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
⊢ ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞

Tactic:
hf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
h₁ : ∀ (ω : Ω), ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ENNReal.ofReal (rexp ((↑p : ℝ) * t * X ω))
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞

Tactic:
convert! hf using 3 with ω
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
ω : Ω
⊢ 0 ≤ rexp (t * X ω)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
ω : Ω
h₁ : 0 ≤ (↑p : ℝ)
⊢ ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ENNReal.ofReal (rexp ((↑p : ℝ) * t * X ω))

Tactic:
rw [enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
      ← exp_mul, mul_comm, ← mul_assoc]

Premises used: Real.exp_mul, mul_assoc, ENNReal.ofReal_rpow_of_nonneg, mul_comm, Real.enorm_eq_ofReal
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
ω : Ω
⊢ 0 ≤ (↑p : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
pos :
  ∀ (hp0 : p = 0),
    MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
neg :
  ∀ (hp0 : ¬p = 0),
    MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : p = 0
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simpa [hp0] using (h.integrable_exp_mul t).1

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
neg : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
neg₁ : @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) < ∞
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
(h.integrable_exp_mul t).1

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
exact (h.integrable_exp_mul t).1

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, And.left
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ (↑p : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
neg : ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp)]

Premises used: MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
neg : ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞

Tactic:
simp only [ENNReal.coe_toReal]

Premises used: ENNReal.coe_toReal
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ @HasFiniteIntegral _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp ((↑p : ℝ) * t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
have h' := (h.integrable_exp_mul (p * t)).2
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : @HasFiniteIntegral _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp ((↑p : ℝ) * t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞

Tactic:
rw [hasFiniteIntegral_def] at h'

Premises used: MeasureTheory.hasFiniteIntegral_def
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
⊢ ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞

Tactic:
h'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
h₁ : ∀ (ω : Ω), ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ‖rexp ((↑p : ℝ) * t * X ω)‖ₑ
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞

Tactic:
convert! h' using 3 with ω
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ rexp (t * X ω)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ rexp ((↑p : ℝ) * t * X ω)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
ω : Ω
h₁ : 0 ≤ (↑p : ℝ)
⊢ ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ‖rexp ((↑p : ℝ) * t * X ω)‖ₑ

Tactic:
rw [enorm_eq_ofReal (by positivity), enorm_eq_ofReal (by positivity),
      ENNReal.ofReal_rpow_of_nonneg (by positivity), ← exp_mul, mul_comm, ← mul_assoc]

Premises used: Real.exp_mul, mul_assoc, ENNReal.ofReal_rpow_of_nonneg, mul_comm, Real.enorm_eq_ofReal
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ (↑p : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h₁ :
  ∀ (ω' : Ω')
    (h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
    (h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')) (t : ℝ),
    cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul] with ω' h h_int t

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_forall_integrable_exp_mul, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t = log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t)

Tactic:
rfl

Premises used: ProbabilityTheory.cgf, rfl
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
pos :
  ∀ (h0 : Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)),
    log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
neg :
  ∀ (h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)),
    log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))

Tactic:
by_cases h0 : κ ω' = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
⊢ 0 ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
simpa : 0 ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))

Tactic:
simpa [h0] using by positivity
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
neg : 0 < mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t
neg₁ : mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))

Tactic:
gcongr