Positive linear functionals dominated by a unit

Let E be a real seminormed space with an order, and let u : E satisfy f ≤ ‖f‖ • u for every f : E. For bounded real functions with the supremum norm, u = 1 has this property, and so does the class of 1 in L∞. A positive real linear functional φ on E is then controlled by its value at u:

|φ f| ≤ φ u * ‖f‖.

Hence φ is automatically Lipschitz and continuous, and when ‖u‖ ≤ 1 its operator norm is exactly φ u. In particular a positive functional normalized by φ u = 1, such as a mean on a space of bounded functions, has operator norm one.

The lemmas are stated for any type of positive linear maps, in the sense of LinearMapClass and OrderHomClass, following the convention of Mathlib.Algebra.Order.Module.PositiveLinearMap. No continuity is assumed. Compare PositiveLinearMap.exists_norm_apply_le, the corresponding automatic continuity for positive maps between C⋆-algebras.

Main results

• PositiveLinearMap.abs_apply_le_mul_norm: the bound |φ f| ≤ φ u * ‖f‖.
• PositiveLinearMap.lipschitzWith_of_forall_le_norm_smul: φ is φ u-Lipschitz.
• ContinuousLinearMap.opNorm_eq_apply_of_monotone: a monotone continuous linear functional has operator norm ψ u when ‖u‖ ≤ 1.
• LinearMap.apply_nonneg_of_abs_apply_le_mul_norm: conversely, a linear functional with |ψ f| ≤ ψ u * ‖f‖ is nonnegative at every f with ‖‖f‖ • u - f‖ ≤ ‖f‖.

theorem PositiveLinearMap.apply_le_mul_norm {F : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [Module ℝ E] [LE E] [FunLike F E ℝ] [LinearMapClass F ℝ E ℝ] [OrderHomClass F E ℝ] (φ : F) {u : E} (hu : ∀ (f : E), f ≤ ‖f‖ • u) (f : E) : φ f ≤ φ u * ‖f‖

A positive linear functional is bounded above by its value at a dominating element u, scaled by the norm.

theorem PositiveLinearMap.abs_apply_le_mul_norm {F : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [Module ℝ E] [LE E] [FunLike F E ℝ] [LinearMapClass F ℝ E ℝ] [OrderHomClass F E ℝ] (φ : F) {u : E} (hu : ∀ (f : E), f ≤ ‖f‖ • u) (f : E) : |φ f| ≤ φ u * ‖f‖

A positive linear functional is controlled in absolute value by its value at a dominating element u, scaled by the norm.

theorem PositiveLinearMap.apply_nonneg_of_forall_le_norm_smul {F : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [Module ℝ E] [LE E] [FunLike F E ℝ] [LinearMapClass F ℝ E ℝ] [OrderHomClass F E ℝ] (φ : F) {u : E} (hu : ∀ (f : E), f ≤ ‖f‖ • u) : 0 ≤ φ u

A positive linear functional is nonnegative at a dominating element u.

theorem PositiveLinearMap.abs_apply_sub_apply_le_mul_norm {F : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [Module ℝ E] [LE E] [FunLike F E ℝ] [LinearMapClass F ℝ E ℝ] [OrderHomClass F E ℝ] (φ : F) {u : E} (hu : ∀ (f : E), f ≤ ‖f‖ • u) (f g : E) : |φ f - φ g| ≤ φ u * ‖f - g‖

A positive linear functional is controlled by its value at a dominating element u, scaled by the norm of the difference of the arguments.

theorem PositiveLinearMap.lipschitzWith_of_forall_le_norm_smul {F : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [Module ℝ E] [LE E] [FunLike F E ℝ] [LinearMapClass F ℝ E ℝ] [OrderHomClass F E ℝ] (φ : F) {u : E} (hu : ∀ (f : E), f ≤ ‖f‖ • u) : LipschitzWith (φ u).toNNReal ⇑φ

A positive linear functional is Lipschitz, with constant its value at a dominating element u.

theorem PositiveLinearMap.continuous_of_forall_le_norm_smul {F : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] [Module ℝ E] [LE E] [FunLike F E ℝ] [LinearMapClass F ℝ E ℝ] [OrderHomClass F E ℝ] (φ : F) {u : E} (hu : ∀ (f : E), f ≤ ‖f‖ • u) : Continuous ⇑φ

A positive linear functional is continuous as soon as some element u dominates every f in the sense f ≤ ‖f‖ • u.

theorem ContinuousLinearMap.opNorm_eq_apply_of_monotone {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [PartialOrder E] {u : E} (ψ : E →L[ℝ] ℝ) (hψ : Monotone ⇑ψ) (hu : ∀ (f : E), f ≤ ‖f‖ • u) (hu₁ : ‖u‖ ≤ 1) : ‖ψ‖ = ψ u

A monotone continuous linear functional has operator norm equal to its value at an element u of norm at most one dominating every f in the sense f ≤ ‖f‖ • u.

theorem LinearMap.apply_nonneg_of_abs_apply_le_mul_norm {E : Type u_1} [SeminormedAddCommGroup E] [Module ℝ E] {u : E} (ψ : E →ₗ[ℝ] ℝ) (hψ : ∀ (g : E), |ψ g| ≤ ψ u * ‖g‖) {f : E} (hf : ‖‖f‖ • u - f‖ ≤ ‖f‖) : 0 ≤ ψ f

A converse to PositiveLinearMap.abs_apply_le_mul_norm: a linear functional ψ with |ψ g| ≤ ψ u * ‖g‖ for all g is nonnegative at every f with ‖‖f‖ • u - f‖ ≤ ‖f‖. For bounded real functions or real L∞ with u = 1, every nonnegative f has this property.