L^p membership as finiteness of a Lebesgue integral #
The interpolation argument of InterpolationBasic.lean works throughout with
Lebesgue integrals of the ℝ≥0∞-valued modulus absE f x = ENNReal.ofReal |f x|
of a real function. To feed its conclusions back into Mathlib's Bochner theory
one has to translate between that modulus and the L^p predicates MemLp,
Integrable and the integral ∫⁻ x, ‖f x‖ₑ.
This file records the four translations needed for that purpose. They rely on
the identity ‖r‖ₑ = ENNReal.ofReal |r| for real r, which makes absE f
agree pointwise with ‖f ·‖ₑ. The results are:
- membership in
L^pfor realp > 0implies finiteness of∫⁻ x, absE f x ^ p(lintegral_absE_rpow_lt_top); - conversely finiteness of that integral, together with a.e. strong
measurability, gives membership in
L^p(memLp_ofReal_of_lintegral_absE_rpow_lt_top); - the case
p = 2, stated separately because the exponent2there is a natural-number power (memLp_two_of_lintegral_absE_sq_lt_top); - finiteness of
∫⁻ x, absE f xis exactly Bochner integrability off(integrable_of_lintegral_absE_lt_top).
theorem
CKN.Foundation.Euclidean.lintegral_absE_rpow_lt_top
{f : Parabolic.Vec3 → ℝ}
{p : ℝ}
(hp : 0 < p)
(hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume)
:
theorem
CKN.Foundation.Euclidean.memLp_ofReal_of_lintegral_absE_rpow_lt_top
{f : Parabolic.Vec3 → ℝ}
{p : ℝ}
(hp : 0 < p)
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(h : ∫⁻ (x : Parabolic.Vec3), absE f x ^ p < ⊤)
:
theorem
CKN.Foundation.Euclidean.memLp_two_of_lintegral_absE_sq_lt_top
{f : Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(h : ∫⁻ (x : Parabolic.Vec3), absE f x ^ 2 < ⊤)
:
theorem
CKN.Foundation.Euclidean.integrable_of_lintegral_absE_lt_top
{f : Parabolic.Vec3 → ℝ}
(hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume)
(h : ∫⁻ (x : Parabolic.Vec3), absE f x < ⊤)
: