-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ p * exp (v * X)` is integrable for all nonnegative `p : ℝ`. -/
lemma integrable_rpow_mul_exp_of_mem_interior_integrableExpSet
    (hv : v ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ X ω ^ p * exp (v * X ω)) μ

Proof state:
case intro.intro.intro.refine_2
Ω : 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 < (v - l) ⊓ (u - v)
⊢ Integrable (fun ω => rexp ((v + ((v - l) ⊓ (u - v)) / 2) * X ω)) μ

Tactic:
exact h_subset (add_half_inf_sub_mem_Ioo hvlu)

Result:
no goals

Proof state:
Ω : 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 < (v - l) ⊓ (u - v)

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

Result:
no goals

Proof state:
case intro.intro.intro
Ω : 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 < (v - l) ⊓ (u - v)
⊢ Integrable (fun ω => X ω ^ p * rexp (v * X ω)) μ

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

Result:
case intro.intro.intro.refine_1
Ω : 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 < (v - l) ⊓ (u - v)
⊢ ((v - l) ⊓ (u - v)) / 2 ≠ 0

case intro.intro.intro.refine_2
Ω : 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 < (v - l) ⊓ (u - v)
⊢ Integrable (fun ω => rexp ((v + ((v - l) ⊓ (u - v)) / 2) * X ω)) μ

case intro.intro.intro.refine_3
Ω : 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 < (v - l) ⊓ (u - v)
⊢ Integrable (fun ω => rexp ((v - ((v - l) ⊓ (u - v)) / 2) * X ω)) μ

Proof state:
case intro.intro.intro.refine_1
Ω : 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 < (v - l) ⊓ (u - v)
⊢ ((v - l) ⊓ (u - v)) / 2 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro
Ω : 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 ω)) μ

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]

Result:
case intro.intro.intro
Ω : 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 < (v - l) ⊓ (u - v)
⊢ Integrable (fun ω => X ω ^ p * rexp (v * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (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

Result:
Ω : 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 ω)) μ

Proof state:
Ω : 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 ω)) μ

Tactic:
obtain ⟨l, u, hvlu, h_subset⟩ := hv

Result:
case intro.intro.intro
Ω : 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 ω)) μ

Proof state:
case intro.intro.intro.refine_3
Ω : 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 < (v - l) ⊓ (u - v)
⊢ Integrable (fun ω => rexp ((v - ((v - l) ⊓ (u - v)) / 2) * X ω)) μ

Tactic:
exact h_subset (sub_half_inf_sub_mem_Ioo hvlu)

Result:
no goals