Bounded continuous functions in L∞

Every bounded continuous function is essentially bounded, for any measure. Mathlib's BoundedContinuousFunction.toLp sends bounded continuous functions to Lp E p μ only for a finite measure; for p = ∞ no finiteness is needed, and BoundedContinuousFunction.toLpTop is the corresponding continuous linear map (α →ᵇ E) →L[𝕜] Lp E ∞ μ, of norm at most one.

When μ is positive on nonempty open sets, the essential supremum of a continuous function is its supremum, so toLpTop preserves norms and is injective. For real-valued functions it is monotone, an order embedding when μ is positive on open sets, and sends the constant function one to the constant class 1. This is the comparison between supremum and essential-supremum norms used, for instance, to compare means on bounded uniformly continuous functions on a locally compact group with means on Haar L∞.

On a discrete space, if μ charges every point, the only null set is empty, so every essentially bounded function is bounded and toLpTop is onto: it identifies bounded functions with L∞ as normed spaces and, for real values, as ordered spaces. For instance, L∞ of a counting measure, or of a Haar measure on a discrete group, consists of all bounded functions.

Main definitions

• BoundedContinuousFunction.toLpTop μ 𝕜: the class of a bounded continuous function in Lp E ∞ μ, as a continuous linear map.
• BoundedContinuousFunction.toLpTopLinearIsometryEquiv μ 𝕜: on a discrete space, for a measure charging every point, toLpTop as a linear isometry equivalence.

Main results

• BoundedContinuousFunction.coeFn_toLpTop: the class of f is almost everywhere f.
• BoundedContinuousFunction.toLp_top_eq_toLpTop: for a finite measure it agrees with BoundedContinuousFunction.toLp.
• BoundedContinuousFunction.norm_toLpTop_le: ‖[f]‖ ≤ ‖f‖ for every measure.
• BoundedContinuousFunction.norm_toLpTop: ‖[f]‖ = ‖f‖ when μ is positive on open sets.
• BoundedContinuousFunction.toLpTop_le_toLpTop_iff: for such μ, the map is an order embedding on real-valued functions.
• BoundedContinuousFunction.toLpTop_surjective: on a discrete space, for a measure charging every point, every class in L∞ is the class of a bounded function.
• BoundedContinuousFunction.toLpTop_one: the constant function one goes to the constant one.

theorem BoundedContinuousFunction.mem_Lp_top {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) (f : BoundedContinuousFunction α E) : ContinuousMap.toAEEqFun μ f.toContinuousMap ∈ MeasureTheory.Lp E ⊤ μ

The almost-everywhere class of a bounded continuous function lies in L∞, whatever the measure.

noncomputable def BoundedContinuousFunction.toLpTop {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : BoundedContinuousFunction α E →L[𝕜] ↥(MeasureTheory.Lp E ⊤ μ)

The class in L∞ of a bounded continuous function, as a continuous linear map. Unlike BoundedContinuousFunction.toLp, no finiteness of the measure is required.

theorem BoundedContinuousFunction.coeFn_toLpTop {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : BoundedContinuousFunction α E) : ↑↑((toLpTop μ 𝕜) f) =ᵐ[μ] ⇑f

The class of f in L∞ is almost everywhere equal to f.

theorem BoundedContinuousFunction.toLp_top_eq_toLpTop {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [MeasureTheory.IsFiniteMeasure μ] : toLp ⊤ μ 𝕜 = toLpTop μ 𝕜

For a finite measure, toLpTop is Mathlib's BoundedContinuousFunction.toLp with exponent ∞.

theorem BoundedContinuousFunction.norm_toLpTop_le {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : BoundedContinuousFunction α E) : ‖(toLpTop μ 𝕜) f‖ ≤ ‖f‖

The essential supremum norm of a bounded continuous function is at most its supremum norm.

@[simp]

theorem BoundedContinuousFunction.norm_toLpTop {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] (f : BoundedContinuousFunction α E) : ‖(toLpTop μ 𝕜) f‖ = ‖f‖

If μ is positive on nonempty open sets, the essential supremum norm of a bounded continuous function is its supremum norm.

theorem BoundedContinuousFunction.toLpTop_injective {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] : Function.Injective ⇑(toLpTop μ 𝕜)

If μ is positive on nonempty open sets, a bounded continuous function is determined by its class in L∞.

theorem BoundedContinuousFunction.toLpTop_surjective {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] [DiscreteTopology α] : Function.Surjective ⇑(toLpTop μ 𝕜)

On a discrete space, if μ charges every point, every class in L∞ is the class of a bounded function.

noncomputable def BoundedContinuousFunction.toLpTopLinearIsometryEquiv {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) (𝕜 : Type u_3) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] [DiscreteTopology α] : BoundedContinuousFunction α E ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp E ⊤ μ)

On a discrete space, if μ charges every point, taking classes identifies bounded functions with L∞, isometrically.

@[simp]

theorem BoundedContinuousFunction.coe_toLpTopLinearIsometryEquiv {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] [DiscreteTopology α] : ⇑(toLpTopLinearIsometryEquiv μ 𝕜) = ⇑(toLpTop μ 𝕜)

@[simp]

theorem BoundedContinuousFunction.toLpTop_toLpTopLinearIsometryEquiv_symm {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] [DiscreteTopology α] (φ : ↥(MeasureTheory.Lp E ⊤ μ)) : (toLpTop μ 𝕜) ((toLpTopLinearIsometryEquiv μ 𝕜).symm φ) = φ

@[simp]

theorem BoundedContinuousFunction.coe_toLpTopLinearIsometryEquiv_symm {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] [DiscreteTopology α] (φ : ↥(MeasureTheory.Lp E ⊤ μ)) : ⇑((toLpTopLinearIsometryEquiv μ 𝕜).symm φ) = ↑↑φ

The bounded function representing a class in L∞ is its coercion to a function.

@[simp]

theorem BoundedContinuousFunction.toLpTopLinearIsometryEquiv_symm_toLpTop {α : Type u_1} {E : Type u_2} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [NormedAddCommGroup E] [SecondCountableTopologyEither α E] (μ : MeasureTheory.Measure α) {𝕜 : Type u_3} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [μ.IsOpenPosMeasure] [DiscreteTopology α] (f : BoundedContinuousFunction α E) : (toLpTopLinearIsometryEquiv μ 𝕜).symm ((toLpTop μ 𝕜) f) = f

Real-valued functions

theorem BoundedContinuousFunction.toLpTop_mono {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) {f g : BoundedContinuousFunction α ℝ} (h : f ≤ g) : (toLpTop μ ℝ) f ≤ (toLpTop μ ℝ) g

The class in L∞ of a pointwise smaller bounded continuous function is smaller.

@[simp]

theorem BoundedContinuousFunction.toLpTop_le_toLpTop_iff {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [μ.IsOpenPosMeasure] {f g : BoundedContinuousFunction α ℝ} : (toLpTop μ ℝ) f ≤ (toLpTop μ ℝ) g ↔ f ≤ g

If μ is positive on nonempty open sets, comparing classes in L∞ compares bounded continuous functions pointwise.

@[simp]

theorem BoundedContinuousFunction.toLpTopLinearIsometryEquiv_symm_le_symm_iff {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [DiscreteTopology α] [μ.IsOpenPosMeasure] {φ ψ : ↥(MeasureTheory.Lp ℝ ⊤ μ)} : (toLpTopLinearIsometryEquiv μ ℝ).symm φ ≤ (toLpTopLinearIsometryEquiv μ ℝ).symm ψ ↔ φ ≤ ψ

On a discrete space, if μ charges every point, the inverse identification of L∞ with bounded functions preserves and reflects the order.

@[simp]

theorem BoundedContinuousFunction.toLpTop_one {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) : (toLpTop μ ℝ) 1 = 1

The constant function one goes to the constant class one in L∞.

@[simp]

theorem BoundedContinuousFunction.toLpTopLinearIsometryEquiv_symm_one {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α) [DiscreteTopology α] [μ.IsOpenPosMeasure] : (toLpTopLinearIsometryEquiv μ ℝ).symm 1 = 1

On a discrete space, if μ charges every point, the constant class one in L∞ is represented by the constant function one.