Documentation

TauCeti.RepresentationTheory.Continuous.LeftRegular.Basic

The left regular representation on vector-valued Lᵖ #

Let μ be a left-invariant measure on a group G, and E a normed space. The group G acts on Lᵖ(G, E) by left translation, (λ g f) x = f (g⁻¹ * x); the inverse makes this a representation rather than an antirepresentation. Each translation is an isometry, so the action is unitary on L²(G, E) for an inner product space E. For a topological group, 1 ≤ p < ∞, and a locally finite measure that is inner regular with respect to compact sets on sets of finite measure, for instance the Haar measure MeasureTheory.Measure.haar of a locally compact group, the action is strongly continuous: each orbit g ↦ λ g f is continuous. Operator-norm continuity is neither claimed nor true in general.

No σ-finiteness, second countability, or compactness of G is assumed. The left regular representation on L²(G, H) is the group part of the regular covariant representation of a C⋆-dynamical system. For a compact group with normalized Haar measure and scalar coefficients, TauCeti.leftRegularLp is the same action.

Main definitions #

Main statements #

For the counting-measure obstruction, see Bekka–de la Harpe–Valette, Kazhdan's Property (T), Appendix G.5.

source
noncomputable def MeasureTheory.Measure.leftRegular {G : Type u_1} (𝕜 : Type u_2) (E : Type u_3) [Group G] [MeasurableSpace G] [MeasurableMul G] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (μ : Measure G) [μ.IsMulLeftInvariant] (p : ENNReal) [Fact (1 ≤ p)] :
ContRepresentation 𝕜 G ↥(Lp E p μ)

The left regular representation of G on Lᵖ(G, E) for a left-invariant measure μ: the element g acts by f ↦ (x ↦ f (g⁻¹ * x)).

Instances For
    source
    theorem MeasureTheory.Measure.leftRegular_apply {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [MeasurableSpace G] [MeasurableMul G] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (μ : Measure G) [μ.IsMulLeftInvariant] (p : ENNReal) [Fact (1 ≤ p)] (g : G) (f : ↥(Lp E p μ)) :
    ((leftRegular 𝕜 E μ p) g) f = (Lp.compMeasurePreserving (fun (x : G) => g⁻¹ * x) ⋯) f

    Left translation on Lᵖ(G, E), unfolded to the underlying Lp.compMeasurePreserving.

    source
    theorem MeasureTheory.Measure.coeFn_leftRegular {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [MeasurableSpace G] [MeasurableMul G] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (μ : Measure G) [μ.IsMulLeftInvariant] (p : ENNReal) [Fact (1 ≤ p)] (g : G) (f : ↥(Lp E p μ)) :
    ↑↑(((leftRegular 𝕜 E μ p) g) f) =ᵐ[μ] fun (x : G) => ↑↑f (g⁻¹ * x)

    Left translation on Lᵖ(G, E) is represented by left translation of functions.

    source
    @[simp]
    theorem MeasureTheory.Measure.norm_leftRegular_apply {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [MeasurableSpace G] [MeasurableMul G] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (μ : Measure G) [μ.IsMulLeftInvariant] (p : ENNReal) [Fact (1 ≤ p)] (g : G) (f : ↥(Lp E p μ)) :
    ‖((leftRegular 𝕜 E μ p) g) f‖ = ‖f‖

    Left translation preserves the Lᵖ norm.

    source
    theorem MeasureTheory.Measure.isUnitary_leftRegular {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul G] (μ : Measure G) [μ.IsMulLeftInvariant] {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
    (leftRegular 𝕜 E μ 2).IsUnitary

    The left regular representation on L²(G, E) is unitary, because left translation preserves the left-invariant measure.

    source
    theorem MeasureTheory.Measure.continuous_leftRegular_apply {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [MeasurableSpace G] [MeasurableMul G] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (μ : Measure G) [μ.IsMulLeftInvariant] (p : ENNReal) [Fact (1 ≤ p)] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [μ.InnerRegularCompactLTTop] [IsLocallyFiniteMeasure μ] (hp : p ≠ ⊤) (f : ↥(Lp E p μ)) :
    Continuous fun (g : G) => ((leftRegular 𝕜 E μ p) g) f

    The left regular representation is strongly continuous for p < ∞ and a locally finite measure that is inner regular with respect to compact sets on sets of finite measure: every orbit map g ↦ λ g f is continuous.

    source
    @[simp]
    theorem MeasureTheory.Measure.invariants_count_leftRegular {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [MeasurableSpace G] [MeasurableMul G] [NormedRing 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [Infinite G] {p : ENNReal} [Fact (1 ≤ p)] (hp' : p ≠ ⊤) :
    (leftRegular 𝕜 E count p).invariants = ⊥

    For counting measure on an infinite group, the vector-valued regular representation on Lᵖ, 1 ≤ p < ∞, has only the zero invariant vector.