The regular representations of a compact group on L²(G)

A compact group G acts on L²(G) by right translation, (π g f) x = f (x * g), and by left translation, (π g f) x = f (g⁻¹ * x); the inverse in the latter is what makes it a representation rather than an antirepresentation. Both translations preserve normalized Haar measure, so both actions are unitary, and both are strongly continuous: for each fixed f the orbit map g ↦ π g f is continuous. Continuity of g ↦ π g for the operator norm is neither proved nor needed here; the uses of L²(G) that do need it obtain it only after restricting to a finite-dimensional invariant subspace.

The two actions commute, and TauCeti.RepresentationTheory.Compact.BiregularRepresentation bundles them into a single action of G × G.

Main definitions

• TauCeti.rightRegularLp: the right regular representation of G on L²(G).
• TauCeti.leftRegularLp: the left regular representation of G on L²(G).

Main statements

• TauCeti.rightRegularLp_apply and TauCeti.leftRegularLp_apply: π g is Lp.compMeasurePreserving (· * g), respectively Lp.compMeasurePreserving (g⁻¹ * ·), the form in which Mathlib and TauCeti.RepresentationTheory.Compact.Convolution phrase translation.
• TauCeti.coeFn_rightRegularLp and TauCeti.coeFn_leftRegularLp: π g f is represented by the function x ↦ f (x * g), respectively x ↦ f (g⁻¹ * x).
• TauCeti.rightRegularLp_toLp and TauCeti.leftRegularLp_toLp: on the class of a continuous function, π g is translation of that function.
• TauCeti.isUnitary_rightRegularLp and TauCeti.isUnitary_leftRegularLp: both translations preserve the L² inner product.
• TauCeti.continuous_rightRegularLp_apply and TauCeti.continuous_leftRegularLp_apply: both actions are strongly continuous.

Implementation notes

Right translation on Lp is definitionally Mathlib's DomMulAct action of Gᵐᵒᵖ, that is, DomMulAct.mk (MulOpposite.op g) • f, so rightRegularLp's identity law is one_smul for that action; its multiplicativity law is proved instead via Mathlib's compMeasurePreserving_comp_apply and right-multiplication associativity, since the two composed Lp.compMeasurePreservingₗᵢ do not unify with the DomMulAct action definitionally. Left translation is written with an inverse, so no such DomMulAct action is available for it and its identity law goes through Lp.compMeasurePreserving_id_apply after normalizing fun x => (1 : G)⁻¹ * x to the identity. Strong continuity of both is Mathlib's Continuous.compMeasurePreservingLp.

The bodies of both representations are not exposed: TauCeti.rightRegularLp_apply and TauCeti.leftRegularLp_apply are the interface through which a downstream file transfers a statement phrased in raw Lp.compMeasurePreserving form to the representation and back.

noncomputable def TauCeti.rightRegularLp (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : ContRepresentation 𝕜 G ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The right regular representation of a compact group on L²(G): the element g acts by f ↦ (x ↦ f (x * g)), which preserves normalized Haar measure and hence the L² norm.

Mathlib's ContRepresentation does not require g ↦ π g to be continuous for the operator norm, and no such continuity is proved here; it is an extra hypothesis, established downstream after restricting to a convolution eigenspace. What is proved in general is the strong continuity TauCeti.continuous_rightRegularLp_apply.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.rightRegularLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (g : G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : ((rightRegularLp 𝕜 G) g) f = (MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => x * g) ⋯) f

Right translation on L²(G), unfolded to the underlying Lp.compMeasurePreserving. The body of rightRegularLp is not exposed, so this is the lemma that lets a downstream file transfer a statement phrased in raw Lp.compMeasurePreserving form to the representation and back.

theorem TauCeti.coeFn_rightRegularLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (g : G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : ↑↑(((rightRegularLp 𝕜 G) g) f) =ᵐ[haarProb G] fun (x : G) => ↑↑f (x * g)

Right translation on L²(G) is represented by right translation of functions.

@[simp]

theorem TauCeti.rightRegularLp_toLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (F : C(G, 𝕜)) (g : G) : ((rightRegularLp 𝕜 G) g) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) F) = (ContinuousMap.toLp 2 (haarProb G) 𝕜) (F.comp (ContinuousMap.mulRight g))

On a continuous function, the right regular representation is right translation. The class of F is sent to the class of x ↦ F (x * g), with no almost-everywhere qualification on the representatives.

theorem TauCeti.isUnitary_rightRegularLp (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : (rightRegularLp 𝕜 G).IsUnitary

The right regular representation is unitary, because right translation preserves normalized Haar measure.

theorem TauCeti.continuous_rightRegularLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : Continuous fun (g : G) => ((rightRegularLp 𝕜 G) g) f

The right regular representation is strongly continuous: each orbit map g ↦ π g f is continuous. This is Mathlib's continuity of Lp.compMeasurePreserving in both arguments, applied to the family of right multiplications, which depends continuously on the multiplier because (g, x) ↦ x * g curries.

noncomputable def TauCeti.leftRegularLp (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : ContRepresentation 𝕜 G ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))

The left regular representation of a compact group on L²(G): the element g acts by f ↦ (x ↦ f (g⁻¹ * x)). The inverse makes this a representation rather than an antirepresentation.

As for TauCeti.rightRegularLp, only strong continuity is asserted; operator-norm continuity is not needed and generally fails for infinite compact groups.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.leftRegularLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (g : G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : ((leftRegularLp 𝕜 G) g) f = (MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => g⁻¹ * x) ⋯) f

Left translation on L²(G), unfolded to the underlying Lp.compMeasurePreserving. As for TauCeti.rightRegularLp_apply, the body of leftRegularLp is not exposed, so this is the lemma that moves a statement between the representation and its raw Lp.compMeasurePreserving form.

theorem TauCeti.coeFn_leftRegularLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (g : G) (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : ↑↑(((leftRegularLp 𝕜 G) g) f) =ᵐ[haarProb G] fun (x : G) => ↑↑f (g⁻¹ * x)

Left translation on L²(G) is represented by left translation of functions.

@[simp]

theorem TauCeti.leftRegularLp_toLp {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (F : C(G, 𝕜)) (g : G) : ((leftRegularLp 𝕜 G) g) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) F) = (ContinuousMap.toLp 2 (haarProb G) 𝕜) (F.comp (ContinuousMap.mulLeft g⁻¹))

On a continuous function, the left regular representation is left translation by the inverse.

theorem TauCeti.isUnitary_leftRegularLp (𝕜 : Type u_1) (G : Type u_2) [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] : (leftRegularLp 𝕜 G).IsUnitary

The left regular representation is unitary, because left translation preserves normalized Haar measure.

theorem TauCeti.continuous_leftRegularLp_apply {𝕜 : Type u_1} {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (f : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : Continuous fun (g : G) => ((leftRegularLp 𝕜 G) g) f

The left regular representation is strongly continuous: every orbit map g ↦ g · f is continuous.