The Lᵖ integral is bounded by the p-th power of the Lᵖ seminorm

For a finite exponent p ≠ 0, Mathlib's MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral identifies eLpNorm f p μ ^ p with ∫⁻ ‖f‖ₑ ^ p ∂μ for an almost everywhere strongly measurable f. Without measurability the seminorm is ∞ by convention, so the inequality ∫⁻ ‖f‖ₑ ^ p ∂μ ≤ eLpNorm f p μ ^ p holds for every f (TauCeti.lintegral_rpow_enorm_le_rpow_eLpNorm). This is the form in which a bound on the Lᵖ seminorm is used to bound an integral, with no measurability side condition. For a natural exponent n ≠ 0 and measurable f the identity reads ∫⁻ ‖f‖ₑ ^ n ∂μ = eLpNorm f n μ ^ n (TauCeti.lintegral_enorm_pow_eq_eLpNorm_pow).

Consequently a function in Lᵖ for p ≠ 0 is finite almost everywhere (MeasureTheory.MemLp.ae_enorm_lt_top), including for p = ∞.

The same identification gives monotone convergence for the seminorm: the Lᵖ seminorm of the supremum of an increasing sequence of functions with values in [0, ∞] is the supremum of their seminorms (MeasureTheory.eLpNorm_iSup_eq_iSup_eLpNorm), also for p = ∞.

theorem TauCeti.lintegral_rpow_enorm_le_rpow_eLpNorm {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {p : NNReal} (hp : p ≠ 0) (f : α → ε) : ∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ ≤ MeasureTheory.eLpNorm f (↑p) μ ^ ↑p

For p ≠ 0, the integral ∫⁻ ‖f‖ₑ ^ p ∂μ is at most eLpNorm f p μ ^ p, whether or not f is almost everywhere strongly measurable.

theorem TauCeti.lintegral_enorm_pow_eq_eLpNorm_pow {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {n : ℕ} (hn : n ≠ 0) {f : α → ε} (hf : MeasureTheory.AEStronglyMeasurable f μ) : ∫⁻ (x : α), ‖f x‖ₑ ^ n ∂μ = MeasureTheory.eLpNorm f (↑n) μ ^ n

For n ≠ 0, the n-th power of the Lⁿ seminorm of an almost everywhere strongly measurable function is the integral of ‖f‖ₑ ^ n.

theorem MeasureTheory.eLpNorm_iSup_eq_iSup_eLpNorm {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : ℕ → α → ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (hmono : ∀ᵐ (x : α) ∂μ, Monotone fun (n : ℕ) => f n x) {p : ENNReal} : eLpNorm (fun (x : α) => ⨆ (n : ℕ), f n x) p μ = ⨆ (n : ℕ), eLpNorm (f n) p μ

Monotone convergence for the Lᵖ seminorm. The Lᵖ seminorm of the pointwise supremum of an almost everywhere increasing sequence of almost everywhere measurable functions with values in [0, ∞] is the supremum of their Lᵖ seminorms.

theorem MeasureTheory.MemLp.ae_enorm_lt_top {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p : ENNReal} (hf : MemLp f p μ) (hp : p ≠ 0) : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ < ⊤

A function in Lᵖ with p ≠ 0 is finite almost everywhere.