Translations of bounded uniformly continuous functions

For a topological group G, the left translation of a function f on G by g is (L_g f)(x) = f (g⁻¹ * x), and its right translation is (R_g f)(x) = f (x * g). Both preserve TauCeti.UCB G, and both are linear isometries of the supremum norm, so they give two commuting group homomorphisms

TauCeti.UCB.leftTranslation, TauCeti.UCB.rightTranslation : G →* (UCB G ≃ₗᵢ[ℝ] UCB G).

Left translation is the action against which invariant means are defined. The defining condition of UCB G says exactly that u ↦ L_u f is norm-continuous at 1, so the orbit map g ↦ L_g f is norm-continuous. The orbit map g ↦ R_g f is norm-continuous at 1 only when f (x * u) is uniformly close to f x for all u near 1, which is not part of the definition of UCB G; no continuity statement is made for right translations.

Main definitions

• TauCeti.ucbSubalgebra.leftTranslation 𝕜 G: g ↦ L_g on ucbSubalgebra 𝕜 G, with L_g f = f (g⁻¹ * ·).
• TauCeti.UCB.leftTranslation: its case 𝕜 = ℝ, on UCB G.
• TauCeti.UCB.rightTranslation: g ↦ R_g, with R_g f = f (· * g).

Main results

• TauCeti.compContinuous_mulLeft_mem_ucbSubalgebra, TauCeti.compContinuous_mulRight_mem_ucbSubalgebra: ucbSubalgebra 𝕜 G, and in particular ucb G, is closed under left and right translation.
• TauCeti.UCB.leftTranslation_le_leftTranslation_iff, TauCeti.UCB.leftTranslation_apply_algebraMap: left translation preserves the order and the constant functions; likewise for right translation.
• TauCeti.UCB.continuous_leftTranslation_apply: the orbit map g ↦ L_g f is continuous for the supremum norm.
• TauCeti.UCB.commute_leftTranslation_rightTranslation: left and right translations commute.
• TauCeti.UCB.sum_leftTranslation: on a finite group, the sum of the left translates of f is the constant function ∑ x, f x.

References

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

theorem TauCeti.compContinuous_mulLeft_mem_ucbSubalgebra {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G 𝕜} (hf : f ∈ ucbSubalgebra 𝕜 G) (g : G) : f.compContinuous (ContinuousMap.mulLeft g) ∈ ucbSubalgebra 𝕜 G

A left translate x ↦ f (g * x) of a function in ucbSubalgebra 𝕜 G lies in ucbSubalgebra 𝕜 G.

theorem TauCeti.compContinuous_mulRight_mem_ucbSubalgebra {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G 𝕜} (hf : f ∈ ucbSubalgebra 𝕜 G) (g : G) : f.compContinuous (ContinuousMap.mulRight g) ∈ ucbSubalgebra 𝕜 G

A right translate x ↦ f (x * g) of a function in ucbSubalgebra 𝕜 G lies in ucbSubalgebra 𝕜 G.

theorem TauCeti.compContinuous_mulLeft_mem_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} (hf : f ∈ ucb G) (g : G) : f.compContinuous (ContinuousMap.mulLeft g) ∈ ucb G

A left translate x ↦ f (g * x) of a function in ucb G lies in ucb G.

theorem TauCeti.compContinuous_mulRight_mem_ucb {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {f : BoundedContinuousFunction G ℝ} (hf : f ∈ ucb G) (g : G) : f.compContinuous (ContinuousMap.mulRight g) ∈ ucb G

A right translate x ↦ f (x * g) of a function in ucb G lies in ucb G.

def TauCeti.ucbSubalgebra.leftTranslation (𝕜 : Type u_1) (G : Type u_2) [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G →* ↥(ucbSubalgebra 𝕜 G) ≃ₗᵢ[𝕜] ↥(ucbSubalgebra 𝕜 G)

Left translation g ↦ L_g, where (L_g f)(x) = f (g⁻¹ * x), as a group homomorphism from G to the linear isometry equivalences of ucbSubalgebra 𝕜 G.

theorem TauCeti.ucbSubalgebra.coe_leftTranslation {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : ↥(ucbSubalgebra 𝕜 G)) : ↑(((leftTranslation 𝕜 G) g) f) = (↑f).compContinuous (ContinuousMap.mulLeft g⁻¹)

The left translate L_g f is the precomposition of f with x ↦ g⁻¹ * x.

@[simp]

theorem TauCeti.ucbSubalgebra.leftTranslation_apply {𝕜 : Type u_1} {G : Type u_2} [NormedField 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : ↥(ucbSubalgebra 𝕜 G)) (x : G) : ↑(((leftTranslation 𝕜 G) g) f) x = ↑f (g⁻¹ * x)

noncomputable def TauCeti.UCB.leftTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G →* UCB G ≃ₗᵢ[ℝ] UCB G

Left translation g ↦ L_g, where (L_g f)(x) = f (g⁻¹ * x), as a group homomorphism from G to the linear isometry equivalences of UCB G; the case 𝕜 = ℝ of ucbSubalgebra.leftTranslation.

noncomputable def TauCeti.UCB.rightTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : G →* UCB G ≃ₗᵢ[ℝ] UCB G

Right translation g ↦ R_g, where (R_g f)(x) = f (x * g), as a group homomorphism from G to the linear isometry equivalences of UCB G.

theorem TauCeti.UCB.coe_leftTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : UCB G) : ↑((leftTranslation g) f) = (↑f).compContinuous (ContinuousMap.mulLeft g⁻¹)

The left translate L_g f is the precomposition of f with x ↦ g⁻¹ * x.

theorem TauCeti.UCB.coe_rightTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : UCB G) : ↑((rightTranslation g) f) = (↑f).compContinuous (ContinuousMap.mulRight g)

The right translate R_g f is the precomposition of f with x ↦ x * g.

@[simp]

theorem TauCeti.UCB.leftTranslation_apply {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : UCB G) (x : G) : ↑((leftTranslation g) f) x = ↑f (g⁻¹ * x)

@[simp]

theorem TauCeti.UCB.rightTranslation_apply {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (f : UCB G) (x : G) : ↑((rightTranslation g) f) x = ↑f (x * g)

@[simp]

theorem TauCeti.UCB.leftTranslation_symm {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : (leftTranslation g).symm = leftTranslation g⁻¹

@[simp]

theorem TauCeti.UCB.rightTranslation_symm {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : (rightTranslation g).symm = rightTranslation g⁻¹

@[simp]

theorem TauCeti.UCB.leftTranslation_le_leftTranslation_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G} {f f' : UCB G} : (leftTranslation g) f ≤ (leftTranslation g) f' ↔ f ≤ f'

Left translation preserves and reflects the pointwise order.

@[simp]

theorem TauCeti.UCB.leftTranslation_apply_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : (leftTranslation g) 1 = 1

Left translation fixes the constant function 1.

@[simp]

theorem TauCeti.UCB.leftTranslation_apply_algebraMap {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (c : ℝ) : (leftTranslation g) ((algebraMap ℝ (UCB G)) c) = (algebraMap ℝ (UCB G)) c

Left translation fixes every constant function.

@[simp]

theorem TauCeti.UCB.rightTranslation_le_rightTranslation_iff {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G} {f f' : UCB G} : (rightTranslation g) f ≤ (rightTranslation g) f' ↔ f ≤ f'

Right translation preserves and reflects the pointwise order.

@[simp]

theorem TauCeti.UCB.rightTranslation_apply_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : (rightTranslation g) 1 = 1

Right translation fixes the constant function 1.

@[simp]

theorem TauCeti.UCB.rightTranslation_apply_algebraMap {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (c : ℝ) : (rightTranslation g) ((algebraMap ℝ (UCB G)) c) = (algebraMap ℝ (UCB G)) c

Right translation fixes every constant function.

theorem TauCeti.UCB.tendsto_leftTranslation_apply_nhds_one {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : UCB G) : Filter.Tendsto (fun (u : G) => (leftTranslation u) f) (nhds 1) (nhds f)

The left translates L_u f of a function f in UCB G tend to f in supremum norm as u → 1.

theorem TauCeti.UCB.continuous_leftTranslation_apply {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (f : UCB G) : Continuous fun (g : G) => (leftTranslation g) f

The orbit map g ↦ L_g f of a function f in UCB G is continuous for the supremum norm.

theorem TauCeti.UCB.commute_leftTranslation_rightTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g h : G) : Commute (leftTranslation g) (rightTranslation h)

Left and right translations of UCB G commute.

theorem TauCeti.UCB.leftTranslation_rightTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g h : G) (f : UCB G) : (leftTranslation g) ((rightTranslation h) f) = (rightTranslation h) ((leftTranslation g) f)

Left and right translations of UCB G commute, applied to a function.

theorem TauCeti.UCB.sum_leftTranslation {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Fintype G] (f : UCB G) : ∑ g : G, (leftTranslation g) f = (algebraMap ℝ (UCB G)) (∑ x : G, ↑f x)

On a finite group, the sum of the left translates L_g f of a function f in UCB G is the constant function ∑ x, f x.