-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If 0 belongs to the interior of `integrableExpSet X μ`, then `X` is in `ℒp` for all
finite `p`. -/
lemma memLp_of_mem_interior_integrableExpSet (h : 0 ∈ interior (integrableExpSet X μ)) (p : ℝ≥0) :
    MemLp X p μ

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (fun x => ‖X x‖ ^ (↑p).toReal) μ

Tactic:
simp only [norm_eq_abs, ENNReal.coe_toReal]

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (fun x => |X x| ^ ↑p) μ

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ MemLp X (↑p) μ

Tactic:
rw [← integrable_norm_rpow_iff hX.aestronglyMeasurable (mod_cast hp_zero) (by simp)]

Result:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (fun x => ‖X x‖ ^ (↑p).toReal) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ ↑p ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (fun x => |X x| ^ ↑p) μ

Tactic:
exact integrable_rpow_abs_of_mem_interior_integrableExpSet h p.2

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ AEStronglyMeasurable X μ

Tactic:
exact hX.aestronglyMeasurable

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ MemLp X (↑p) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet h

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
⊢ MemLp X (↑p) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
⊢ MemLp X (↑p) μ

Tactic:
by_cases hp_zero : p = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ MemLp X (↑p) μ

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ MemLp X (↑p) μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ MemLp X (↑p) μ

Tactic:
simp only [hp_zero, ENNReal.coe_zero, memLp_zero_iff_aestronglyMeasurable]

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ AEStronglyMeasurable X μ