Means on bounded uniformly continuous functions

For a topological group G, a mean on TauCeti.UCB G is a real linear functional m which is positive, 0 ≤ f → 0 ≤ m f, and normalized, m 1 = 1. A left-invariant mean is the object whose existence defines amenability of G.

This file develops the basic theory of means. Continuity is not part of the definition: since every f lies below the constant ‖f‖, positivity and normalization give |m f| ≤ ‖f‖, so a mean is 1-Lipschitz for the supremum norm, and in particular compatible with uniform limits. The derived continuous linear functional has operator norm one. The means form a convex subset of the continuous dual of UCB G, and evaluation at a point of G is a mean, so this set is nonempty.

Main definitions

• TauCeti.Mean G: a positive normalized linear functional on UCB G.
• TauCeti.Mean.toContinuousLinearMap: the continuous linear functional underlying a mean.
• TauCeti.Mean.eval: evaluation at a point, as a mean.

Main results

• TauCeti.Mean.map_algebraMap: a mean takes the value c at the constant function c.
• TauCeti.Mean.ciInf_le_apply, TauCeti.Mean.apply_le_ciSup: ⨅ x, f x ≤ m f ≤ ⨆ x, f x.
• TauCeti.Mean.abs_apply_le_norm, TauCeti.Mean.abs_apply_sub_apply_le: |m f| ≤ ‖f‖ and |m f - m g| ≤ ‖f - g‖.
• TauCeti.Mean.lipschitzWith: a mean is 1-Lipschitz; it is therefore a ContinuousLinearMapClass.
• TauCeti.Mean.norm_toContinuousLinearMap: a mean has operator norm one.
• TauCeti.Mean.mem_range_toContinuousLinearMap_iff: the continuous linear functionals coming from means are exactly the positive ones taking the value 1 at 1.
• TauCeti.Mean.convex_range_toContinuousLinearMap: the means form a convex set.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Appendix G.1.

structure TauCeti.Mean (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] extends TauCeti.UCB G →ₚ[ℝ] ℝ : Type u_1

A mean on UCB G: a positive real linear functional taking the value 1 at the constant function 1.

• toFun : TauCeti.UCB G → ℝ
• map_add' (x y : TauCeti.UCB G) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : ℝ) (x : TauCeti.UCB G) : self.toFun (m • x) = (RingHom.id ℝ) m • self.toFun x
• monotone' : Monotone self.toFun
• map_one' : self.toFun 1 = 1

  A mean takes the value 1 at the constant function 1.

@[instance_reducible]

instance TauCeti.Mean.instFunLikeUCBReal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : FunLike (Mean G) (UCB G) ℝ

instance TauCeti.Mean.instLinearMapClassRealUCB {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : LinearMapClass (Mean G) ℝ (UCB G) ℝ

instance TauCeti.Mean.instOrderHomClassUCBReal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : OrderHomClass (Mean G) (UCB G) ℝ

theorem TauCeti.Mean.ext {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m n : Mean G} (h : ∀ (f : UCB G), m f = n f) : m = n

Two means are equal when they agree on every function.

theorem TauCeti.Mean.ext_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m n : Mean G} : m = n ↔ ∀ (f : UCB G), m f = n f

@[simp]

theorem TauCeti.Mean.coe_toPositiveLinearMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : ⇑m.toPositiveLinearMap = ⇑m

theorem TauCeti.Mean.toPositiveLinearMap_injective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Function.Injective toPositiveLinearMap

@[simp]

theorem TauCeti.Mean.map_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : m 1 = 1

A mean takes the value 1 at the constant function 1.

noncomputable def TauCeti.Mean.mk₀ {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : UCB G →ₗ[ℝ] ℝ) (hφ : ∀ (f : UCB G), 0 ≤ f → 0 ≤ φ f) (h₁ : φ 1 = 1) : Mean G

A mean built from a linear functional which is nonnegative on nonnegative functions and takes the value 1 at 1.

@[simp]

theorem TauCeti.Mean.mk₀_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (φ : UCB G →ₗ[ℝ] ℝ) (hφ : ∀ (f : UCB G), 0 ≤ f → 0 ≤ φ f) (h₁ : φ 1 = 1) (f : UCB G) : (mk₀ φ hφ h₁) f = φ f

@[simp]

theorem TauCeti.Mean.map_algebraMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) (c : ℝ) : m ((algebraMap ℝ (UCB G)) c) = c

A mean takes the value c at the constant function c.

theorem TauCeti.Mean.apply_le_of_forall_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) {f : UCB G} {c : ℝ} (h : ∀ (x : G), ↑f x ≤ c) : m f ≤ c

A mean of a function bounded above by c is at most c.

theorem TauCeti.Mean.le_apply_of_forall_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) {f : UCB G} {c : ℝ} (h : ∀ (x : G), c ≤ ↑f x) : c ≤ m f

A mean of a function bounded below by c is at least c.

theorem TauCeti.Mean.ciInf_le_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) (f : UCB G) : ⨅ (x : G), ↑f x ≤ m f

A mean of a function is at least the infimum of its values.

theorem TauCeti.Mean.apply_le_ciSup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) (f : UCB G) : m f ≤ ⨆ (x : G), ↑f x

A mean of a function is at most the supremum of its values.

theorem TauCeti.Mean.abs_apply_le_norm {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) (f : UCB G) : |m f| ≤ ‖f‖

A mean of a function is bounded in absolute value by its supremum norm.

theorem TauCeti.Mean.abs_apply_sub_apply_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) (f g : UCB G) : |m f - m g| ≤ ‖f - g‖

A mean changes by at most the supremum distance between its arguments.

theorem TauCeti.Mean.lipschitzWith {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : LipschitzWith 1 ⇑m

A mean is 1-Lipschitz for the supremum norm.

instance TauCeti.Mean.instContinuousLinearMapClassRealUCB {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousLinearMapClass (Mean G) ℝ (UCB G) ℝ

A mean is continuous for the supremum norm.

def TauCeti.Mean.toContinuousLinearMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : UCB G →L[ℝ] ℝ

The continuous linear functional underlying a mean.

@[simp]

theorem TauCeti.Mean.coe_toContinuousLinearMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : ⇑m.toContinuousLinearMap = ⇑m

theorem TauCeti.Mean.toContinuousLinearMap_injective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Function.Injective toContinuousLinearMap

@[simp]

theorem TauCeti.Mean.norm_toContinuousLinearMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : Mean G) : ‖m.toContinuousLinearMap‖ = 1

A mean has operator norm one.

theorem TauCeti.Mean.mem_range_toContinuousLinearMap_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {φ : UCB G →L[ℝ] ℝ} : φ ∈ Set.range toContinuousLinearMap ↔ (∀ (f : UCB G), 0 ≤ f → 0 ≤ φ f) ∧ φ 1 = 1

A continuous linear functional on UCB G comes from a mean exactly when it is nonnegative on nonnegative functions and takes the value 1 at 1.

theorem TauCeti.Mean.convex_range_toContinuousLinearMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Convex ℝ (Set.range toContinuousLinearMap)

The means on UCB G form a convex set of continuous linear functionals.

noncomputable def TauCeti.Mean.eval (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) : Mean G

Evaluation at a point of G is a mean on UCB G.

@[simp]

theorem TauCeti.Mean.eval_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : G) (f : UCB G) : (eval G x) f = ↑f x

instance TauCeti.Mean.instNonempty {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Nonempty (Mean G)