awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
ω : Ω
⊢ |X ω ^ p| ≤ |X ω| ^ p

Tactic:
abs_rpow_le_abs_rpow _ _

Premises used: Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
ω : Ω
⊢ |X ω ^ p| ≤ |X ω| ^ p

Tactic:
exact abs_rpow_le_abs_rpow _ _

Premises used: Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
funProp : 0 ≤ p
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
n : ℕ
h : ∀ (ω : Ω), X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_mul_exp_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω

Premises used: ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + t) * X ω)) μ
ht_int_neg : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - t) * X ω)) μ
n : ℕ
ω : Ω
⊢ X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) μ

Tactic:
have h := integrable_rpow_abs_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (0 * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) μ

Tactic:
simpa using h
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 (ω : Ω) ↦ rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ

Tactic:
simpa using ht_int_neg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 : ℕ
h : ∀ (ω : Ω), |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n) μ

Tactic:
convert!
    integrable_rpow_abs_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω

Premises used: ProbabilityTheory.integrable_rpow_abs_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 : ℕ
ω : Ω
⊢ |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 ω)) μ
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((0 - t) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ

Tactic:
have h := integrable_rpow_mul_exp_of_integrable_exp_mul (μ := μ) (X := X) ht (v := 0) ?_ ?_ hp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
h : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ

Tactic:
simpa using h
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 : ℕ
h : ∀ (ω : Ω), X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n) μ

Tactic:
convert!
    integrable_rpow_of_integrable_exp_mul ht ht_int_pos ht_int_neg
      (by positivity : 0 ≤ (n : ℝ)) with
    ω

Premises used: ProbabilityTheory.integrable_rpow_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 : ℕ
ω : Ω
⊢ X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ 0 < min (v - l) (u - v)

Tactic:
simp [hv.1, hv.2]

Premises used: And.right, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
⊢ 0 < min (v - l) (u - v)

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hv.1, hv.2]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
right : v + min (v - l) (u - v) / 2 < u
⊢ v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l < v

Tactic:
hv.1

Premises used: And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ 0 ≤ min (v - l) (u - v) / 2

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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

Tactic:
calc l < v := hv.1
    _ ≤ v + ((v - l) ⊓ (u - v)) / 2 := le_add_of_nonneg_right (by positivity)

Premises used: HSub.hSub, le_add_of_nonneg_right, And.left, Min.min
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
bc : min (v - l) (u - v) / 2 < min (v - l) (u - v)
⊢ v + min (v - l) (u - v) / 2 < v + min (v - l) (u - v)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ 0 < min (v - l) (u - v)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ min (v - l) (u - v) / 2 < min (v - l) (u - v)

Tactic:
exact half_lt_self (by positivity)

Premises used: half_lt_self
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
bc : min (v - l) (u - v) ≤ u - v
⊢ v + min (v - l) (u - v) ≤ v + (u - v)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ min (v - l) (u - v) ≤ u - v

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ min (v - l) (u - v) ≤ u - v

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v + (u - v) = u

Tactic:
abel
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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)
calc₂ : v + (u - v) = u
⊢ v + min (v - l) (u - v) / 2 < 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

Premises used: HSub.hSub, Min.min
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
right : v - min (v - l) (u - v) / 2 < u
⊢ v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ l = v - (v - l)

Tactic:
abel
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
h : min (v - l) (u - v) ≤ v - l
⊢ v - (v - l) ≤ v - min (v - l) (u - v)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ min (v - l) (u - v) ≤ v - l

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ min (v - l) (u - v) ≤ v - l

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
h : min (v - l) (u - v) / 2 < min (v - l) (u - v)
⊢ v - min (v - l) (u - v) < v - min (v - l) (u - v) / 2

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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)
calc₂ : v - min (v - l) (u - v) < v - min (v - l) (u - v) / 2
⊢ l < 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)

Premises used: HSub.hSub, Min.min
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
rw : v ≤ v + min (v - l) (u - v) / 2
⊢ v - min (v - l) (u - v) / 2 ≤ v

Tactic:
rw [sub_le_iff_le_add]

Premises used: sub_le_iff_le_add
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v ≤ v + min (v - l) (u - v) / 2

Tactic:
exact le_add_of_nonneg_right (by positivity)

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
l u v : ℝ
hv : v ∈ Set.Ioo l u
h_pos : 0 < min (v - l) (u - v)
⊢ v < u

Tactic:
hv.2

Premises used: And.right
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
⊢ v - min (v - l) (u - v) / 2 < u

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

Premises used: HSub.hSub, And.right, Min.min
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ ∃ (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

Premises used: mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
obtain : ∀ (l u : ℝ) (hvlu : v ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ), AEMeasurable X μ
⊢ AEMeasurable X μ

Tactic:
obtain ⟨l, u, hvlu, h_subset⟩ := hv
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
⊢ 0 < min (v - l) (u - v)

Tactic:
simp [hvlu.1, hvlu.2]

Premises used: And.right, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
⊢ 0 < min (v - l) (u - v)

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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)
⊢ 0 < t

Tactic:
have ht : 0 < t := half_pos h_pos
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 μ
neg : ∀ (hvt : ¬v + t = 0), AEMeasurable X μ
⊢ AEMeasurable X μ

Tactic:
by_cases hvt : v + t = 0
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
rw : v ≠ t
⊢ v - t ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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

Tactic:
fun h_eq ↦ ht.ne' ?_

Premises used: LT.lt.ne', Not
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
refine : ∀ (h_eq : v = t), t = 0
⊢ v ≠ t

Tactic:
refine fun h_eq ↦ ht.ne' ?_

Premises used: LT.lt.ne'
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
h_eq : v = t
⊢ t = 0

Tactic:
simpa [h_eq] using hvt
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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

Tactic:
have hvt' : v - t ≠ 0 := by
      rw [sub_ne_zero]
      refine fun h_eq ↦ ht.ne' ?_
      simpa [h_eq] using hvt
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
hvt' : v - t ≠ 0
⊢ AEMeasurable X μ

Tactic:
aemeasurable_of_aemeasurable_exp_mul hvt'
      (h_subset (sub_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Premises used: ProbabilityTheory.sub_half_inf_sub_mem_Ioo, MeasureTheory.Integrable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
hvt' : v - t ≠ 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hvt'
      (h_subset (sub_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Premises used: ProbabilityTheory.sub_half_inf_sub_mem_Ioo, MeasureTheory.Integrable.aemeasurable, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 μ

Tactic:
aemeasurable_of_aemeasurable_exp_mul hvt
      (h_subset (add_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Premises used: MeasureTheory.Integrable.aemeasurable, ProbabilityTheory.add_half_inf_sub_mem_Ioo, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hvt
      (h_subset (add_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Premises used: MeasureTheory.Integrable.aemeasurable, ProbabilityTheory.add_half_inf_sub_mem_Ioo, Real.aemeasurable_of_aemeasurable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
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 ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv

Premises used: mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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
obtain :
  ∀ (l u : ℝ) (hvlu : v ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
obtain ⟨l, u, hvlu, h_subset⟩ := hv
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 μ
⊢ 0 < min (v - l) (u - v)

Tactic:
simp [hvlu.1, hvlu.2]

Premises used: And.right, And.left
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 μ
⊢ 0 < min (v - l) (u - v)

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 ω)) μ

Tactic:
integrable_rpow_abs_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 ω)) μ
refine_3 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (v * X ω)) μ

Tactic:
refine integrable_rpow_abs_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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)
⊢ min (v - l) (u - v) / 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
h_subset (add_half_inf_sub_mem_Ioo hvlu)

Premises used: Set.Mem, setOf, MeasureTheory.Integrable, ProbabilityTheory.integrableExpSet, ProbabilityTheory.add_half_inf_sub_mem_Ioo
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
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 (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
exact h_subset (add_half_inf_sub_mem_Ioo hvlu)

Premises used: ProbabilityTheory.add_half_inf_sub_mem_Ioo