awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
have hu : UniqueDiffOn ℝ (Set.Icc 0 t)
Tactic: have hu : UniqueDiffOn ℝ (Set.Icc 0 t) := uniqueDiffOn_Icc ht
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
have rw : ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [← sub_zero (cgf X μ t)]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
have nth_rw : ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
Tactic: nth_rw 3 [← sub_zero t]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
have rw : ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
Tactic: rw [← Set.uIoo_of_lt ht]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
have h : ∀ (x : ℝ), 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t
Tactic: convert! taylor_mean_remainder_lagrange_iteratedDeriv ht.ne ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
h : ∀ (x : ℝ), 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t
⊢ ∃ u ∈ Set.uIoo 0 t, cgf X μ t - 0 = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) (t - 0) 2 / 2
have convert_3 : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.uIcc 0 t)
Tactic: convert! taylor_mean_remainder_lagrange_iteratedDeriv ht.ne ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0
have h : 0 = deriv (cgf X μ) 0
Tactic: convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
h : 0 = deriv (cgf X μ) 0
⊢ derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0
have convert_2 : UniqueDiffWithinAt ℝ (Set.Icc 0 t) 0
Tactic: convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x : ℝ
⊢ 0 = taylorWithinEval (cgf X μ) 1 (Set.uIcc 0 t) 0 t
have hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0
Tactic: have hd : derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0 := by
      convert! (analyticAt_cgf (hs ⟨le_refl 0, le_of_lt ht⟩)).differentiableAt.derivWithin _
      · simpa [hc] using (deriv_cgf_zero (hs ⟨le_refl 0, le_of_lt ht⟩)).symm
      · exact hu 0 ⟨le_refl 0, le_of_lt ht⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
⊢ ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.uIcc 0 t)
have convert_3 : ContDiffOn ℝ (HAdd.hAdd (α := WithTop ℕ∞) (↑1 : WithTop ℕ∞) 1) (cgf X μ) (Set.Icc 0 t)
Tactic: rw [Set.uIcc_of_lt ht]
-- 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
h : HasSubgaussianMGF X c κ ν
⊢ AEStronglyMeasurable (m₀ := mΩ) X ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have h_int : @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (1 * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: have h_int := h.integrable_exp_mul 1
-- 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
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, AEStronglyMeasurable (m₀ := mΩ) X ((κ : (a : Ω') → Measure Ω) ω')
have h_int : ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: have h_int := h.ae_integrable_exp_mul 1
-- 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
h : HasSubgaussianMGF X c κ ν
h_int : ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, AEStronglyMeasurable (m₀ := mΩ) X ((κ : (a : Ω') → Measure Ω) ω')
have h₁ : ∀ (ω : Ω') (h_int : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (1 * X y)) ((κ : (a : Ω') → Measure Ω) ω)),
  AEStronglyMeasurable (m₀ := mΩ) X ((κ : (a : Ω') → Measure Ω) ω)
Tactic: filter_upwards [h_int] with ω h_int
-- 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
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
have h_int : ∀ (n : ℤ), ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: have h_int (n : ℤ) : ∀ᵐ ω' ∂ν, Integrable (fun ω ↦ exp (n * X ω)) (κ ω') :=
    h.ae_integrable_exp_mul _
-- 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
h : HasSubgaussianMGF X c κ ν
h_int :
  ∀ (n : ℤ),
    ∀ᵐ (ω' : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
have h_int₁ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
Tactic: rw [← ae_all_iff] at h_int
Cleared hypotheses: h_int
-- 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
h : HasSubgaussianMGF X c κ ν
h_int :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
have h₁ : ∀ (ω' : Ω')
  (h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω'))
  (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: filter_upwards [h_int] with ω' h_int 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
have h₁ : ∀ (ω' : Ω') (hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (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
-- 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
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
have h₁ : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
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 Ω) ω')
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω')
have h₂ : @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
have pos : ∀ (hp : p = 0), @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
Tactic: by_cases hp : p = 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 : Ω → ℝ
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 Ω) ω') < ∞
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
have neg : ∀ (hp : ¬p = 0), @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((κ : (a : Ω') → Measure Ω) ω') < ∞
Tactic: by_cases hp : p = 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 : Ω → ℝ
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 Ω) ω') < ∞
have neg : ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp),
      ENNReal.coe_toReal]
-- 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
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
hp : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
have hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp ((↑p : ℝ) * t * X x)) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
Tactic: have hf := (hi (p * t)).lintegral_lt_top
-- 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
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 Ω) ω' < ∞
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(κ : (a : Ω') → Measure Ω) ω' < ∞
have h₁ : ∀ (ω : Ω), ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ENNReal.ofReal (rexp ((↑p : ℝ) * t * X ω))
Tactic: convert! hf using 3 with ω
-- 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
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 Ω) ω' < ∞
ω : Ω
⊢ ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ENNReal.ofReal (rexp ((↑p : ℝ) * t * X ω))
have h₁ : 0 ≤ (↑p : ℝ)
Tactic: rw [enorm_eq_ofReal (by positivity), ENNReal.ofReal_rpow_of_nonneg (by positivity),
      ← exp_mul, mul_comm, ← mul_assoc]
-- 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
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have pos : ∀ (hp0 : p = 0), MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: by_cases hp0 : p = 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
pos :
  ∀ (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 Ω) ∘ₘ ν)
have neg : ∀ (hp0 : ¬p = 0),
  MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: by_cases hp0 : p = 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have neg : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
neg : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ MemLp (ε := ℝ) (m0 := mΩ) (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
have neg₁ : @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) < ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ @eLpNorm _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) (↑p : ℝ≥0∞) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν) < ∞
have neg : ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
Tactic: rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp0) (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ≥0∞).toReal ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
have neg : ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
Tactic: simp only [ENNReal.coe_toReal]
-- 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
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
have h' : @HasFiniteIntegral _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp ((↑p : ℝ) * t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
Tactic: have h' := (h.integrable_exp_mul (p * t)).2
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : @HasFiniteIntegral _ ℝ _ mΩ (fun (ω : Ω) ↦ rexp ((↑p : ℝ) * t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
have h'₁ : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
Tactic: rw [hasFiniteIntegral_def] 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
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p : ℝ) ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
have h₁ : ∀ (ω : Ω), ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ‖rexp ((↑p : ℝ) * t * X ω)‖ₑ
Tactic: convert! h' using 3 with ω
-- 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
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp ((↑p : ℝ) * t * X a)‖ₑ ∂(⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν < ∞
ω : Ω
⊢ ‖rexp (t * X ω)‖ₑ ^ (↑p : ℝ) = ‖rexp ((↑p : ℝ) * t * X ω)‖ₑ
have h₁ : 0 ≤ (↑p : ℝ)
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]
-- 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
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have 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
Tactic: filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul] with ω' h h_int 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 : Ω → ℝ
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 : ℝ
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
have 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))
Tactic: by_cases h0 : κ ω' = 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 : Ω → ℝ
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))
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
have 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))
Tactic: by_cases h0 : κ ω' = 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 : Ω → ℝ
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 Ω)
⊢ log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
have simpa : 0 ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: simpa [h0] using by positivity