Functions continuous on a compact set are essentially bounded

A function continuous on a compact set K is bounded there, so it lies in L^∞(μ.restrict s) for every measurable s ⊆ K (ContinuousOn.memLp_top_restrict_of_subset_isCompact). Allowing s ⊊ K covers the usual case of an open interval (a, b) inside the compact interval [a, b]. This is the continuous counterpart of Mathlib's MonotoneOn.memLp_top, and the restricted-measure counterpart of Continuous.memLp_top_of_hasCompactSupport.

On a compact space with a measure that is finite on compact sets, every continuous function lies in every Lᵖ, so for a finite exponent p ≠ 0 its Lᵖ seminorm is the integral (∫ ‖f‖ ^ p dμ) ^ (1 / p) (Continuous.eLpNorm_eq_integral_rpow_norm).

theorem ContinuousOn.memLp_top_restrict_of_subset_isCompact {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [SeminormedAddGroup E] {f : X → E} {K s : Set X} {μ : MeasureTheory.Measure X} (hf : ContinuousOn f K) (hK : IsCompact K) (hs : MeasurableSet s) (hsK : s ⊆ K) : MeasureTheory.MemLp f ⊤ (μ.restrict s)

A function continuous on a compact set K is essentially bounded on every measurable s ⊆ K.

theorem Continuous.eLpNorm_eq_integral_rpow_norm {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {F : Type u_3} [NormedAddCommGroup F] [CompactSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : X → F} (hf : Continuous f) {p : ENNReal} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) : MeasureTheory.eLpNorm f p μ = ENNReal.ofReal ((∫ (x : X), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹)

The Lᵖ seminorm of a continuous function on a compact space, for a finite exponent p ≠ 0 and a measure finite on compact sets, as an integral: ‖f‖_{Lᵖ} = (∫ ‖f‖ ^ p dμ) ^ (1 / p).