awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
refine_3 :
  ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (0 * X ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) μ
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) μ
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ
Tactic: have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n) μ
have h : ∀ (ω : Ω), |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)
Tactic: convert!
    integrable_rpow_abs_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
have refine_3 : ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)) μ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
Tactic: have h := integrable_rpow_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
refine_3 :
  ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)) μ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
have refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ
Tactic: have h := integrable_rpow_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
p : ℝ
hp : 0 ≤ p
refine_3 :
  ∀ (h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)) μ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
refine_1 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ
Tactic: have h := integrable_rpow_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (-t * X ω)) μ
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n) μ
have h : ∀ (ω : Ω), X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)
Tactic: convert!
    integrable_rpow_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u
have h_pos : 0 < min (v - l) (u - v)
Tactic: have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u
have left : l < v + min (v - l) (u - v) / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
left : l < v + min (v - l) (u - v) / 2
⊢ v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u
have right : v + min (v - l) (u - v) / 2 < u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < v + min (v - l) (u - v)
have bc : min (v - l) (u - v) / 2 < min (v - l) (u - v)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) ≤ v + (u - v)
have bc : min (v - l) (u - v) ≤ u - v
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < u
have calc : v + min (v - l) (u - v) / 2 < v + min (v - l) (u - v)
Tactic: calc v + ((v - l) ⊓ (u - v)) / 2
    _ < v + ((v - l) ⊓ (u - v)) := by gcongr; exact half_lt_self (by positivity)
    _ ≤ v + (u - v) := by gcongr; exact inf_le_right
    _ = u := by abel
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
calc : v + min (v - l) (u - v) / 2 < v + min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < u
have calc₁ : v + min (v - l) (u - v) ≤ v + (u - v)
Tactic: calc v + ((v - l) ⊓ (u - v)) / 2
    _ < v + ((v - l) ⊓ (u - v)) := by gcongr; exact half_lt_self (by positivity)
    _ ≤ v + (u - v) := by gcongr; exact inf_le_right
    _ = u := by abel
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
calc : v + min (v - l) (u - v) / 2 < v + min (v - l) (u - v)
calc₁ : v + min (v - l) (u - v) ≤ v + (u - v)
⊢ v + min (v - l) (u - v) / 2 < u
have calc₂ : v + (u - v) = u
Tactic: calc v + ((v - l) ⊓ (u - v)) / 2
    _ < v + ((v - l) ⊓ (u - v)) := by gcongr; exact half_lt_self (by positivity)
    _ ≤ v + (u - v) := by gcongr; exact inf_le_right
    _ = u := by abel
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u
have h_pos : 0 < min (v - l) (u - v)
Tactic: have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u
have left : l < v - min (v - l) (u - v) / 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
left : l < v - min (v - l) (u - v) / 2
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u
have right : v - min (v - l) (u - v) / 2 < u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - (v - l) ≤ v - min (v - l) (u - v)
have h : min (v - l) (u - v) ≤ v - l
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) < v - min (v - l) (u - v) / 2
have h : min (v - l) (u - v) / 2 < min (v - l) (u - v)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l < v - min (v - l) (u - v) / 2
have calc : l = v - (v - l)
Tactic: calc l = v - (v - l) := by abel
    _ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
    _ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
calc : l = v - (v - l)
⊢ l < v - min (v - l) (u - v) / 2
have calc₁ : v - (v - l) ≤ v - min (v - l) (u - v)
Tactic: calc l = v - (v - l) := by abel
    _ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
    _ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
calc : l = v - (v - l)
calc₁ : v - (v - l) ≤ v - min (v - l) (u - v)
⊢ l < v - min (v - l) (u - v) / 2
have calc₂ : v - min (v - l) (u - v) < v - min (v - l) (u - v) / 2
Tactic: calc l = v - (v - l) := by abel
    _ ≤ v - ((v - l) ⊓ (u - v)) := by gcongr; exact inf_le_left
    _ < v - ((v - l) ⊓ (u - v)) / 2 := by gcongr; exact half_lt_self (by positivity)
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 ≤ v
have rw : v ≤ v + min (v - l) (u - v) / 2
Tactic: rw [sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) / 2 < u
have calc : v - min (v - l) (u - v) / 2 ≤ v
Tactic: calc v - ((v - l) ⊓ (u - v)) / 2
    _ ≤ v := by
      rw [sub_le_iff_le_add]
      exact le_add_of_nonneg_right (by positivity)
    _ < u := hv.2
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X μ
have hv₁ : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
Tactic: rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
⊢ AEMeasurable X μ
have obtain : ∀ (l u : ℝ) (hvlu : v ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ), AEMeasurable X μ
Tactic: obtain ⟨l, u, hvlu, h_subset⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
⊢ AEMeasurable X μ
have h_pos : 0 < min (v - l) (u - v)
Tactic: have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
⊢ AEMeasurable X μ
have ht : 0 < t
Tactic: have ht : 0 < t := half_pos h_pos
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
⊢ AEMeasurable X μ
have pos : ∀ (hvt : v + t = 0), AEMeasurable X μ
Tactic: by_cases hvt : v + t = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
pos : ∀ (hvt : v + t = 0), AEMeasurable X μ
⊢ AEMeasurable X μ
have neg : ∀ (hvt : ¬v + t = 0), AEMeasurable X μ
Tactic: by_cases hvt : v + t = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ v - t ≠ 0
have rw : v ≠ t
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ v ≠ t
have refine : ∀ (h_eq : v = t), t = 0
Tactic: refine fun h_eq ↦ ht.ne' ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (v - l) (u - v) / 2
h_pos : 0 < min (v - l) (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ AEMeasurable X μ
have hvt' : v - t ≠ 0
Tactic: have hvt' : v - t ≠ 0 := by
      rw [sub_ne_zero]
      refine fun h_eq ↦ ht.ne' ?_
      simpa [h_eq] using hvt
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
have rw : ∀ (hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ) {p : ℝ} (hp : 0 ≤ p),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
Tactic: rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
Cleared hypotheses: hv, p, hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
have obtain : ∀ (l u : ℝ) (hvlu : v ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
Tactic: obtain ⟨l, u, hvlu, h_subset⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
have h_pos : 0 < min (v - l) (u - v)
Tactic: have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
have refine_1 : min (v - l) (u - v) / 2 ≠ 0
Tactic: refine integrable_rpow_abs_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
refine_1 : min (v - l) (u - v) / 2 ≠ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ
Tactic: refine integrable_rpow_abs_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
refine_1 : min (v - l) (u - v) / 2 ≠ 0
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
have refine_3 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ
Tactic: refine integrable_rpow_abs_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n * rexp (v * X ω)) μ
have h : ∀ (ω : Ω), |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)
Tactic: convert!
    integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hv
      (by positivity : 0 ≤ (n : ℝ)) with
    ω
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
have rw : ∀ (hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ) {p : ℝ} (hp : 0 ≤ p),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
Tactic: rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv
Cleared hypotheses: hv, p, hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
have obtain : ∀ (l u : ℝ) (hvlu : v ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
Tactic: obtain ⟨l, u, hvlu, h_subset⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
have h_pos : 0 < min (v - l) (u - v)
Tactic: have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
have refine_1 : min (v - l) (u - v) / 2 ≠ 0
Tactic: refine integrable_rpow_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
refine_1 : min (v - l) (u - v) / 2 ≠ 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
have refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ
Tactic: refine integrable_rpow_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
refine_1 : min (v - l) (u - v) / 2 ≠ 0
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
have refine_3 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ
Tactic: refine integrable_rpow_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n * rexp (v * X ω)) μ
have h : ∀ (ω : Ω), X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)
Tactic: convert!
    integrable_rpow_mul_exp_of_mem_interior_integrableExpSet hv (by positivity : 0 ≤ (n : ℝ)) with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) μ
have h₁ : Eq.{u_1 + 1} (α := Ω → ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) fun (ω : Ω) ↦ |X ω| ^ p * rexp (0 * X ω)
Tactic: convert! integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet h hp using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n) μ
have h₁ : ∀ (x : Ω), |X x| ^ n = |X x| ^ n * rexp (0 * X x)
Tactic: convert! integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet h n
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ
have h₁ : Eq.{u_1 + 1} (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω ^ p) fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)
Tactic: convert! integrable_rpow_mul_exp_of_mem_interior_integrableExpSet h hp using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n) μ
have h₁ : ∀ (x : Ω), X x ^ n = X x ^ n * rexp (0 * X x)
Tactic: convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h n
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ MemLp X (↑p : ℝ≥0∞) μ
have hX : AEMeasurable X μ
Tactic: have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet h
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
⊢ MemLp X (↑p : ℝ≥0∞) μ
have pos : ∀ (hp_zero : p = 0), MemLp X (↑p : ℝ≥0∞) μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
pos : ∀ (hp_zero : p = 0), MemLp X (↑p : ℝ≥0∞) μ
⊢ MemLp X (↑p : ℝ≥0∞) μ
have neg : ∀ (hp_zero : ¬p = 0), MemLp X (↑p : ℝ≥0∞) μ
Tactic: by_cases hp_zero : p = 0
-- Lean 4 proof step from Mathlib.Probability.Moments.IntegrableExpMul (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ MemLp X (↑p : ℝ≥0∞) μ
have pos : AEStronglyMeasurable X μ
Tactic: simp only [hp_zero, ENNReal.coe_zero, memLp_zero_iff_aestronglyMeasurable]