The constant one in L∞

This file equips L∞(μ) with the class 1 of the constant function one, for any normed group with a distinguished element 1 and on an arbitrary measure space. Unlike MeasureTheory.Lp.const, the construction needs no finite-measure hypothesis because the essential supremum of a constant is always finite. Its norm is that of 1 unless μ = 0, and its real integral is the total mass of the measure.

Every real L∞ class f satisfies f ≤ ‖f‖ • 1 (MeasureTheory.Lp.le_norm_smul_one), so the constant one is an order unit, and a positive linear functional on L∞ is controlled by its value at one; in particular it is continuous (PositiveLinearMap.continuous_lpTop). Conversely, a nonnegative class f satisfies ‖‖f‖ • 1 - f‖ ≤ ‖f‖ (MeasureTheory.Lp.norm_norm_smul_one_sub_le_of_nonneg), which tests positivity of a functional bounded by its value at one.

@[instance_reducible]

instance MeasureTheory.Lp.inftyOne {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [One E] : One ↥(Lp E ⊤ μ)

The class of the constant function one, as an element of L∞(μ).

theorem MeasureTheory.Lp.one_def {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [One E] : 1 = MemLp.toLp (fun (x : α) => 1) ⋯

theorem MeasureTheory.Lp.coeFn_one {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [One E] : ↑↑1 =ᵐ[μ] 1

The representative of 1 : L∞(μ) is almost everywhere the constant function one.

theorem MeasureTheory.Lp.norm_one_of_ne_zero {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [One E] (hμ : μ ≠ 0) : ‖1‖ = ‖1‖

On a nonzero measure, the norm of 1 : L∞(μ) is that of 1.

@[simp]

theorem MeasureTheory.Lp.integral_one {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} : ∫ (x : α), ↑↑1 x ∂μ = μ.real Set.univ

The integral of the constant one of real L∞ is the total mass.

theorem MeasureTheory.Lp.le_norm_smul_one {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} (f : ↥(Lp ℝ ⊤ μ)) : f ≤ ‖f‖ • 1

Every real L∞ class lies below its norm times the constant one. With the lemmas of TauCeti/Analysis/Normed/Order/PositiveLinearMap.lean, this bounds and makes continuous every positive linear functional on L∞.

theorem MeasureTheory.Lp.norm_norm_smul_one_sub_le_of_nonneg {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : ↥(Lp ℝ ⊤ μ)} (hf : 0 ≤ f) : ‖‖f‖ • 1 - f‖ ≤ ‖f‖

A nonnegative real L∞ class f lies within ‖f‖ of ‖f‖ times the constant one.

theorem PositiveLinearMap.continuous_lpTop {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (M : ↥(MeasureTheory.Lp ℝ ⊤ μ) →ₚ[ℝ] ℝ) : Continuous ⇑M

A positive linear functional on real L∞ is continuous.