The L^∞ seminorm as the limit of the Lᵖ seminorms

The L^∞ seminorm eLpNorm f ∞ μ is recovered from the finite-exponent seminorms as p → ∞. When f is almost everywhere strongly measurable, eLpNorm f ∞ μ is the essential supremum of ‖f‖ₑ (MeasureTheory.eLpNorm_exponent_top), so this is the classical limit ‖f‖_p → ‖f‖_∞:

• against an arbitrary measure, eLpNorm f ∞ μ is at most the liminf of eLpNorm f p μ, by Chebyshev's inequality applied on a set of positive measure where ‖f‖ₑ is close to its essential supremum;
• against a finite measure, eLpNorm f p μ converges to eLpNorm f ∞ μ, the missing half being the comparison eLpNorm f p μ ≤ eLpNorm f ∞ μ * μ univ ^ (1 / p).

No measurability hypothesis is needed: if f is not almost everywhere strongly measurable, then eLpNorm f p μ = ∞ for every exponent p, including ∞, and both statements are immediate. In that case eLpNorm f ∞ μ need not agree with the essential supremum of ‖f‖ₑ.

The finite-measure hypothesis cannot be dropped from the convergence statement: for the constant function 1 on ℝ with Lebesgue measure, every finite-exponent seminorm is ∞ while the L^∞ seminorm is 1.

The exponent runs over ℝ≥0, coerced to ℝ≥0∞, so that Filter.atTop is the limit p → ∞; the endpoint ∞ itself is MeasureTheory.eLpNorm_exponent_top.

Main statements

• TauCeti.eLpNorm_exponent_top_le_liminf — eLpNorm f ∞ μ is at most the liminf of the finite-exponent seminorms, for every measure;
• TauCeti.tendsto_eLpNorm_atTop — for a finite measure, the finite-exponent seminorms converge to eLpNorm f ∞ μ.

References

• G. B. Folland, Real Analysis, 2nd ed., Wiley 1999, Chapter 6, Exercise 7: the same limit ‖f‖_q → ‖f‖_∞, stated there for f ∈ Lᵖ ∩ L^∞ with p < ∞ rather than for a finite measure.

theorem TauCeti.eLpNorm_exponent_top_le_liminf {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [TopologicalSpace ε] [ContinuousENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε} : MeasureTheory.eLpNorm f ⊤ μ ≤ Filter.liminf (fun (p : NNReal) => MeasureTheory.eLpNorm f (↑p) μ) Filter.atTop

The L^∞ seminorm is below the limit inferior of the Lᵖ seminorms. For every measure and every f, eLpNorm f ∞ μ is at most the liminf of eLpNorm f p μ as p → ∞. No finiteness of the measure is needed. For almost everywhere strongly measurable f, the left side is the essential supremum of ‖f‖ₑ.

theorem TauCeti.tendsto_eLpNorm_atTop {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [TopologicalSpace ε] [ContinuousENorm ε] {μ : MeasureTheory.Measure α} {f : α → ε} [MeasureTheory.IsFiniteMeasure μ] : Filter.Tendsto (fun (p : NNReal) => MeasureTheory.eLpNorm f (↑p) μ) Filter.atTop (nhds (MeasureTheory.eLpNorm f ⊤ μ))

The Lᵖ seminorms converge to the L^∞ seminorm. Against a finite measure, for every f, eLpNorm f p μ tends to eLpNorm f ∞ μ as p → ∞. For almost everywhere strongly measurable f, the limit is the essential supremum of ‖f‖ₑ.