The algebra of an integrated representation

For a strongly continuous, uniformly bounded representation π of any additive group G on a complex Hilbert space and a measure μ that is inner regular for compact sets, such as the Haar measure MeasureTheory.Measure.addHaar, the integrated operators π(f), for f ∈ L¹(G, μ), generate a closed unital star algebra. The algebra and its algebra-valued integrated form do not require unitarity or commutativity of G. For a left-invariant measure, the translates π(g) π(f) belong to this algebra; under the regularity hypotheses of ContRepresentation.continuous_translatedIntegratedOperatorL1, they vary continuously in norm.

If G is abelian, π is unitary, and μ is inversion-invariant, the integrated operators are commuting normal operators, so the algebra is commutative.

This algebra makes the Gelfand representation available to strongly continuous representations. The translated operators are used to recover continuous group characters from algebra characters that do not vanish on all integrated operators. Unitality alone does not exclude characters that vanish on every integrated operator; no such nonvanishing assertion is made here.

Main definitions

• ContRepresentation.integratedAlgebra: the closed star algebra generated by the integrated form.
• ContRepresentation.integratedOperatorL1ToAlgebra: the algebra-valued integrated form.
• ContRepresentation.translatedIntegratedOperatorL1: algebra-valued translates.

Main statements

• ContRepresentation.star_integratedOperatorL1ToAlgebra: the algebra-valued integrated form preserves the involution for unitary representations and inversion-invariant measures.
• ContRepresentation.integratedOperatorL1ToAlgebra_convolution: convolution becomes multiplication in the integrated algebra for abelian groups and right-invariant measures.
• ContRepresentation.translatedIntegratedOperatorL1_convolution: the corresponding product law for translated integrated operators.
• ContRepresentation.integratedAlgebra_le_iff: the universal property among closed star algebras.
• ContRepresentation.translatedIntegratedOperatorL1_eq: translation is integration of a translated weight.
• ContRepresentation.continuous_translatedIntegratedOperatorL1: continuity in the algebra norm.
• ContRepresentation.isMulCommutative_integratedAlgebra: commutativity for unitary representations of abelian groups. With this result installed locally, the IsMulCommutative scope supplies the CommCStarAlgebra instance.

References

• G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC Press (2016), §§3.2 and 4.4.

noncomputable def ContRepresentation.integratedAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] : StarSubalgebra ℂ (H →L[ℂ] H)

The closed unital star algebra generated by the integrated operators of π.

Equations

• π.integratedAlgebra hcont hbdd μ = (StarAlgebra.adjoin ℂ (Set.range ⇑(π.integratedOperatorL1 hcont hbdd μ))).topologicalClosure

theorem ContRepresentation.integratedAlgebra_def {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] : π.integratedAlgebra hcont hbdd μ = (StarAlgebra.adjoin ℂ (Set.range ⇑(π.integratedOperatorL1 hcont hbdd μ))).topologicalClosure

The integrated algebra is the closure of the star algebra generated by the integrated form.

@[simp]

theorem ContRepresentation.integratedOperatorL1_mem_integratedAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : (π.integratedOperatorL1 hcont hbdd μ) f ∈ π.integratedAlgebra hcont hbdd μ

Every integrated operator belongs to the integrated algebra.

noncomputable def ContRepresentation.integratedOperatorL1ToAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] : ↥(MeasureTheory.Lp ℂ 1 μ) →L[ℂ] ↥(π.integratedAlgebra hcont hbdd μ)

The integrated form with values in its closed star algebra.

Equations

• π.integratedOperatorL1ToAlgebra hcont hbdd μ = (π.integratedOperatorL1 hcont hbdd μ).codRestrict (Subalgebra.toSubmodule (π.integratedAlgebra hcont hbdd μ).toSubalgebra) ⋯

@[simp]

theorem ContRepresentation.coe_integratedOperatorL1ToAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : ↑((π.integratedOperatorL1ToAlgebra hcont hbdd μ) f) = (π.integratedOperatorL1 hcont hbdd μ) f

Coercing the algebra-valued integrated form recovers the original integrated operator.

@[simp]

theorem ContRepresentation.star_integratedOperatorL1ToAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableNeg G] [μ.IsNegInvariant] (hπ : π.IsUnitary) (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : star ((π.integratedOperatorL1ToAlgebra hcont hbdd μ) f) = (π.integratedOperatorL1ToAlgebra hcont hbdd μ) (star ((MeasureTheory.Lp.compMeasurePreserving Neg.neg ⋯) f))

The algebra-valued integrated form of a unitary representation takes the involuted weight to the star of the integrated operator.

instance ContRepresentation.isClosed_integratedAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] : IsClosed ↑(π.integratedAlgebra hcont hbdd μ)

The integrated algebra is closed in the operator norm.

theorem ContRepresentation.integratedAlgebra_le_iff {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] (B : StarSubalgebra ℂ (H →L[ℂ] H)) (hB : IsClosed ↑B) : π.integratedAlgebra hcont hbdd μ ≤ B ↔ ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ B

A closed star subalgebra contains the integrated algebra exactly when it contains every integrated operator.

@[simp]

theorem ContRepresentation.comp_integratedOperatorL1_mem_integratedAlgebra {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableAdd G] [μ.IsAddLeftInvariant] (g : G) (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : π (Multiplicative.ofAdd g) ∘SL (π.integratedOperatorL1 hcont hbdd μ) f ∈ π.integratedAlgebra hcont hbdd μ

A group translate of an integrated operator still belongs to the integrated algebra.

noncomputable def ContRepresentation.translatedIntegratedOperatorL1 {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableAdd G] [μ.IsAddLeftInvariant] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) (g : G) : ↥(π.integratedAlgebra hcont hbdd μ)

Translated integrated operators, as elements of the integrated algebra.

Equations

• π.translatedIntegratedOperatorL1 hcont hbdd μ f g = ⟨π (Multiplicative.ofAdd g) ∘SL (π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩

@[simp]

theorem ContRepresentation.coe_translatedIntegratedOperatorL1 {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableAdd G] [μ.IsAddLeftInvariant] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) (g : G) : ↑(π.translatedIntegratedOperatorL1 hcont hbdd μ f g) = π (Multiplicative.ofAdd g) ∘SL (π.integratedOperatorL1 hcont hbdd μ) f

The underlying operator of a translated integrated operator is π(g) π(f).

theorem ContRepresentation.translatedIntegratedOperatorL1_eq {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableAdd G] [μ.IsAddLeftInvariant] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) (g : G) : π.translatedIntegratedOperatorL1 hcont hbdd μ f g = (π.integratedOperatorL1ToAlgebra hcont hbdd μ) ((MeasureTheory.Lp.compMeasurePreserving (fun (x : G) => -g + x) ⋯) f)

A translated integrated operator is the algebra-valued integrated form of the translated weight.

@[simp]

theorem ContRepresentation.translatedIntegratedOperatorL1_zero {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableAdd G] [μ.IsAddLeftInvariant] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : π.translatedIntegratedOperatorL1 hcont hbdd μ f 0 = (π.integratedOperatorL1ToAlgebra hcont hbdd μ) f

Translation by zero recovers the algebra-valued integrated form.

theorem ContRepresentation.continuous_translatedIntegratedOperatorL1 {G : Type u_1} {H : Type u_2} [AddGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] [MeasurableAdd G] [μ.IsAddLeftInvariant] [IsTopologicalAddGroup G] [MeasureTheory.IsLocallyFiniteMeasure μ] (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : Continuous (π.translatedIntegratedOperatorL1 hcont hbdd μ f)

Translated integrated operators depend continuously on the group element in the norm of the integrated algebra.

theorem ContRepresentation.integratedOperatorL1ToAlgebra_convolution {G : Type u_1} {H : Type u_2} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [SecondCountableTopologyEither G H] {π : ContRepresentation ℂ (Multiplicative G) H} {hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v} {hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C} {μ : MeasureTheory.Measure G} [μ.InnerRegularCompactLTTop] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] {f₁ f₂ : G → ℂ} (hf₁ : MeasureTheory.Integrable f₁ μ) (hf₂ : MeasureTheory.Integrable f₂ μ) : (π.integratedOperatorL1ToAlgebra hcont hbdd μ) (MeasureTheory.Integrable.toL1 (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.mul ℂ ℂ) μ) ⋯) = (π.integratedOperatorL1ToAlgebra hcont hbdd μ) (MeasureTheory.Integrable.toL1 f₁ hf₁) * (π.integratedOperatorL1ToAlgebra hcont hbdd μ) (MeasureTheory.Integrable.toL1 f₂ hf₂)

The algebra-valued integrated form takes convolution of weights to multiplication.

theorem ContRepresentation.translatedIntegratedOperatorL1_convolution {G : Type u_1} {H : Type u_2} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [SecondCountableTopologyEither G H] {π : ContRepresentation ℂ (Multiplicative G) H} {hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v} {hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C} {μ : MeasureTheory.Measure G} [μ.InnerRegularCompactLTTop] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] [μ.IsAddLeftInvariant] {f₁ f₂ : G → ℂ} (hf₁ : MeasureTheory.Integrable f₁ μ) (hf₂ : MeasureTheory.Integrable f₂ μ) (g : G) : π.translatedIntegratedOperatorL1 hcont hbdd μ (MeasureTheory.Integrable.toL1 (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.mul ℂ ℂ) μ) ⋯) g = π.translatedIntegratedOperatorL1 hcont hbdd μ (MeasureTheory.Integrable.toL1 f₁ hf₁) g * (π.integratedOperatorL1ToAlgebra hcont hbdd μ) (MeasureTheory.Integrable.toL1 f₂ hf₂)

Translating the integrated form of a convolution translates the first factor in its product.

theorem ContRepresentation.isMulCommutative_integratedAlgebra {G : Type u_1} {H : Type u_2} [AddCommGroup G] [TopologicalSpace G] [MeasurableSpace G] [R1Space G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : ContRepresentation ℂ (Multiplicative G) H} {hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v} {hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C} {μ : MeasureTheory.Measure G} [μ.InnerRegularCompactLTTop] [MeasurableNeg G] [μ.IsNegInvariant] (hπ : π.IsUnitary) : IsMulCommutative ↥(π.integratedAlgebra hcont hbdd μ)

For a unitary abelian-group representation, the closed algebra of integrated operators is commutative.