English
If 0 lies in the interior of integrableExpSet X μ, then X belongs to Lp for all finite p.
Русский
Если ноль лежит во внутренности интегрируемого экспоненциального множества, то X ∈ Lp для всех конечных p.
LaTeX
$$$0 \\in \\operatorname{Int}(\\mathrm{integrableExpSet}(X,\\mu)) \\Rightarrow \\mathrm{MemLp}(X,p;\\mu)$ for all finite p$$
Lean4
/-- If 0 belongs to the interior of `integrableExpSet X μ`, then `X` is in `ℒp` for all
finite `p`. -/
theorem memLp_of_mem_interior_integrableExpSet (h : 0 ∈ interior (integrableExpSet X μ)) (p : ℝ≥0) : MemLp X p μ :=
by
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet h
by_cases hp_zero : p = 0
· simp only [hp_zero, ENNReal.coe_zero, memLp_zero_iff_aestronglyMeasurable]
exact hX.aestronglyMeasurable
rw [← integrable_norm_rpow_iff hX.aestronglyMeasurable (mod_cast hp_zero) (by simp)]
simp only [norm_eq_abs, ENNReal.coe_toReal]
exact integrable_rpow_abs_of_mem_interior_integrableExpSet h p.2
