Bounded functions uniformly continuous under small left multiplication

For a topological group G, TauCeti.ucb G is the subalgebra of real bounded continuous functions f such that f (u * x) is uniformly close to f x for all u near 1:

∀ ε > 0,  ∀ᶠ u in 𝓝 1,  ∀ x,  |f (u * x) - f x| < ε.

TauCeti.UCB G is the corresponding type. It inherits the supremum norm, the unital algebra structure and the pointwise order of G →ᵇ ℝ, and it is a lattice for the pointwise maximum and minimum. This is the function space on which invariant means of a topological group are defined.

No separation, local compactness or countability hypothesis on G is used. Bekka, de la Harpe and Valette call this condition left uniform continuity, while it is uniform continuity for Mathlib's right uniformity IsTopologicalGroup.rightUniformSpace, whose entourages compare (x, y) through y * x⁻¹; the formula, not the label, is authoritative. The left and right uniformities of a general group can differ, so no IsUniformGroup structure is used.

Main definitions

• TauCeti.ucbSubalgebra 𝕜 G: the subalgebra of G →ᵇ 𝕜 defined by the same condition with ‖·‖ in place of |·|, for a normed field 𝕜.
• TauCeti.ucb G: the subalgebra of G →ᵇ ℝ defined by the condition above, the case 𝕜 = ℝ.
• TauCeti.UCB G: its carrier type, a real Banach algebra and lattice.

Main results

• TauCeti.compLeftContinuousBounded_mem_ucbSubalgebra: postcomposition with a continuous linear map 𝕜 → 𝕜' sends ucbSubalgebra 𝕜 G to ucbSubalgebra 𝕜' G.
• TauCeti.mem_ucb_iff_tendsto: the condition says that the left-multiplication orbit u ↦ f (u * ·) tends to f in supremum norm as u → 1.
• TauCeti.mem_ucb_iff_uniformContinuous: the condition is uniform continuity for the right uniformity of G.
• TauCeti.mem_ucbSubalgebra_of_hasCompactSupport, TauCeti.mem_ucb_of_hasCompactSupport: bounded continuous functions with compact support satisfy the condition.
• TauCeti.isClosed_ucb: ucb G is closed under uniform limits, so UCB G is complete.
• TauCeti.sup_mem_ucb, TauCeti.inf_mem_ucb, TauCeti.abs_mem_ucb: closure under the lattice operations.

References

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

theorem BoundedContinuousFunction.tendsto_compContinuous_mulLeft_iff {M : Type u_1} {β : Type u_2} [MulOneClass M] [TopologicalSpace M] [SeparatelyContinuousMul M] [PseudoMetricSpace β] (f : BoundedContinuousFunction M β) : Filter.Tendsto (fun (u : M) => f.compContinuous (ContinuousMap.mulLeft u)) (nhds 1) (nhds f) ↔ ∀ ε > 0, ∀ᶠ (u : M) in nhds 1, ∀ (x : M), dist (f (u * x)) (f x) < ε

The left-multiplication orbit u ↦ f (u * ·) of a bounded continuous function tends to f in supremum distance as u → 1 exactly when f (u * x) is uniformly close to f x for all u near 1.

theorem BoundedContinuousFunction.tendsto_compContinuous_addLeft_iff {M : Type u_1} {β : Type u_2} [AddZeroClass M] [TopologicalSpace M] [SeparatelyContinuousAdd M] [PseudoMetricSpace β] (f : BoundedContinuousFunction M β) : Filter.Tendsto (fun (u : M) => f.compContinuous (ContinuousMap.addLeft u)) (nhds 0) (nhds f) ↔ ∀ ε > 0, ∀ᶠ (u : M) in nhds 0, ∀ (x : M), dist (f (u + x)) (f x) < ε

The left-addition orbit u ↦ f (u + ·) of a bounded continuous function tends to f in supremum distance as u → 0 exactly when f (u + x) is uniformly close to f x for all u near 0.

theorem TauCeti.uniformContinuous_rightUniformSpace_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {β : Type u_3} [PseudoMetricSpace β] (f : G → β) : UniformContinuous f ↔ ∀ ε > 0, ∀ᶠ (u : G) in nhds 1, ∀ (x : G), dist (f (u * x)) (f x) < ε

A function on a topological group is uniformly continuous for the right uniformity exactly when f (u * x) is uniformly close to f x for all u near 1.

theorem TauCeti.continuous_of_forall_eventually_dist_mul_lt {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {β : Type u_3} [PseudoMetricSpace β] {f : G → β} (h : ∀ ε > 0, ∀ᶠ (u : G) in nhds 1, ∀ (x : G), dist (f (u * x)) (f x) < ε) : Continuous f

A function on a topological group whose values f (u * x) are uniformly close to f x for all u near 1 is continuous.

def TauCeti.ucbSubalgebra (𝕜 : Type u_1) (G : Type u_2) [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subalgebra 𝕜 (BoundedContinuousFunction G 𝕜)

The bounded continuous functions f : G →ᵇ 𝕜 such that f (u * x) is uniformly close to f x for all u near 1, as a subalgebra of G →ᵇ 𝕜. The real space ucb G is the case 𝕜 = ℝ.

theorem TauCeti.mem_ucbSubalgebra_iff {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G 𝕜} : f ∈ ucbSubalgebra 𝕜 G ↔ ∀ ε > 0, ∀ᶠ (u : G) in nhds 1, ∀ (x : G), ‖f (u * x) - f x‖ < ε

The defining condition of ucbSubalgebra 𝕜 G.

theorem TauCeti.mem_ucbSubalgebra_iff_tendsto {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G 𝕜} : f ∈ ucbSubalgebra 𝕜 G ↔ Filter.Tendsto (fun (u : G) => f.compContinuous (ContinuousMap.mulLeft u)) (nhds 1) (nhds f)

Membership in ucbSubalgebra 𝕜 G says that u ↦ f (u * ·) tends to f in supremum norm as u → 1.

theorem TauCeti.compLeftContinuousBounded_mem_ucbSubalgebra {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {𝕜' : Type u_3} {𝕜'' : Type u_4} [NormedField 𝕜'] [NontriviallyNormedField 𝕜''] [NormedSpace 𝕜'' 𝕜] [NormedSpace 𝕜'' 𝕜'] (L : 𝕜 →L[𝕜''] 𝕜') {f : BoundedContinuousFunction G 𝕜} (hf : f ∈ ucbSubalgebra 𝕜 G) : (ContinuousLinearMap.compLeftContinuousBounded G L) f ∈ ucbSubalgebra 𝕜' G

Postcomposing a function in ucbSubalgebra 𝕜 G with a continuous linear map L : 𝕜 → 𝕜', such as the real or imaginary part ℂ → ℝ or the inclusion ℝ → ℂ, gives a function in ucbSubalgebra 𝕜' G.

theorem TauCeti.mem_ucbSubalgebra_of_hasCompactSupport {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G 𝕜} (hf : HasCompactSupport ⇑f) : f ∈ ucbSubalgebra 𝕜 G

A bounded continuous function with compact support belongs to ucbSubalgebra 𝕜 G: by the Heine–Cantor theorem it is uniformly continuous for the right uniformity of G.

noncomputable def TauCeti.ucb (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Subalgebra ℝ (BoundedContinuousFunction G ℝ)

The real bounded continuous functions f on G such that f (u * x) is uniformly close to f x for all u near 1, as a subalgebra of G →ᵇ ℝ.

@[reducible, inline]

abbrev TauCeti.UCB (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Type u_2

The real Banach algebra of bounded functions on G that are uniformly continuous under small left multiplication, with the supremum norm, algebra operations and order of G →ᵇ ℝ.

theorem TauCeti.ucb_eq_ucbSubalgebra (G : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ucb G = ucbSubalgebra ℝ G

ucb G is the case 𝕜 = ℝ of ucbSubalgebra 𝕜 G.

theorem TauCeti.mem_ucb_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} : f ∈ ucb G ↔ ∀ ε > 0, ∀ᶠ (u : G) in nhds 1, ∀ (x : G), |f (u * x) - f x| < ε

The defining condition of ucb G.

theorem TauCeti.mem_ucb_iff_tendsto {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} : f ∈ ucb G ↔ Filter.Tendsto (fun (u : G) => f.compContinuous (ContinuousMap.mulLeft u)) (nhds 1) (nhds f)

Membership in ucb G says that u ↦ f (u * ·) tends to f in supremum norm as u → 1.

theorem TauCeti.mem_ucb_iff_uniformContinuous {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} : f ∈ ucb G ↔ UniformContinuous ⇑f

Membership in ucb G is uniform continuity for the right uniformity of G.

theorem TauCeti.mem_ucb_of_hasCompactSupport {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} (hf : HasCompactSupport ⇑f) : f ∈ ucb G

A bounded continuous function with compact support belongs to ucb G.

theorem TauCeti.isClosed_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : IsClosed ↑(ucb G)

ucb G is closed in G →ᵇ ℝ: a uniform limit of functions in ucb G lies in ucb G.

@[instance_reducible]

noncomputable instance TauCeti.instNormedAddCommGroupUCB {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : NormedAddCommGroup (UCB G)

UCB G is a real normed group for the supremum norm of G →ᵇ ℝ. This inherited instance is restated so that typeclass search finds it directly when UCB G occurs inside another type, such as the continuous dual UCB G →L[ℝ] ℝ; the search through Subalgebra and G →ᵇ ℝ fails there.

instance TauCeti.instCompleteSpaceUCB {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CompleteSpace (UCB G)

UCB G is a real Banach space.

instance TauCeti.instNormSMulClassRealUCB {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : NormSMulClass ℝ (UCB G)

Scalar multiplication on UCB G scales the supremum norm: ‖c • f‖ = ‖c‖ * ‖f‖. Typeclass search does not derive this from the inherited normed space structure, because the norm on UCB G is found through the normed ring structure of the subalgebra.

@[simp]

theorem TauCeti.const_mem_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (c : ℝ) : BoundedContinuousFunction.const G c ∈ ucb G

Constant functions belong to ucb G.

theorem TauCeti.sup_mem_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f g : BoundedContinuousFunction G ℝ} (hf : f ∈ ucb G) (hg : g ∈ ucb G) : f ⊔ g ∈ ucb G

ucb G is closed under the pointwise maximum.

theorem TauCeti.inf_mem_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f g : BoundedContinuousFunction G ℝ} (hf : f ∈ ucb G) (hg : g ∈ ucb G) : f ⊓ g ∈ ucb G

ucb G is closed under the pointwise minimum.

theorem TauCeti.abs_mem_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} (hf : f ∈ ucb G) : |f| ∈ ucb G

ucb G is closed under the pointwise absolute value.

@[instance_reducible]

instance TauCeti.instLatticeUCB {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Lattice (UCB G)

UCB G is a lattice for the pointwise maximum and minimum.

instance TauCeti.instHasSolidNormUCB {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : HasSolidNorm (UCB G)

The supremum norm of UCB G is solid for its pointwise order, as in G →ᵇ ℝ.

@[simp]

theorem TauCeti.UCB.coe_sup {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f g : UCB G) : ↑(f ⊔ g) = ↑f ⊔ ↑g

@[simp]

theorem TauCeti.UCB.coe_inf {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f g : UCB G) : ↑(f ⊓ g) = ↑f ⊓ ↑g

@[simp]

theorem TauCeti.UCB.coe_abs {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : UCB G) : ↑|f| = |↑f|

theorem TauCeti.UCB.ext {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f g : UCB G} (h : ∀ (x : G), ↑f x = ↑g x) : f = g

Two elements of UCB G are equal when they agree at every point.

theorem TauCeti.UCB.ext_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f g : UCB G} : f = g ↔ ∀ (x : G), ↑f x = ↑g x

theorem TauCeti.UCB.le_def {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f g : UCB G} : f ≤ g ↔ ∀ (x : G), ↑f x ≤ ↑g x

The order on UCB G is the pointwise order.

theorem TauCeti.UCB.abs_apply_le_norm {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : UCB G) (x : G) : |↑f x| ≤ ‖f‖

Each value of an element of UCB G is bounded by its supremum norm.

theorem TauCeti.UCB.le_norm_smul_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : UCB G) : f ≤ ‖f‖ • 1

Every element of UCB G lies below the constant function with value its supremum norm.