Group characters detected by integrated operators

Let π be a strongly continuous unitary representation of an abelian group and let A be a complete star subalgebra containing its integrated operators. Each character of A that is nonzero on some integrated operator determines a unique continuous group character χ, with

ω (π(g) π(f)) = χ(g) ω (π(f)).

The nonvanishing assumption is necessary: adjoining an identity to a nonunital algebra can introduce a character that annihilates all the integrated operators. On the other characters, the displayed equation identifies the spectral parameter as an element of the Pontryagin dual. It applies to all integrable weights, independently of the weight witnessing nonvanishing. The hypothesis on A is simply containment of the integrated form's range; translation invariance and norm continuity follow from the integrated form's existing translation API.

References

• G. B. Folland, A Course in Abstract Harmonic Analysis, second edition, §§3.2 and 4.4.

theorem ContRepresentation.existsUnique_pontryaginDual_of_integratedOperatorL1 {G : Type u_1} {H : Type u_2} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] (π : ContRepresentation ℂ (Multiplicative G) H) {hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v} (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (hπ : π.IsUnitary) (A : StarSubalgebra ℂ (H →L[ℂ] H)) [CompleteSpace ↥A] (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) (ω : ↑(WeakDual.characterSpace ℂ ↥A)) : (∃ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩ ≠ 0) → ∃! χ : PontryaginDual (Multiplicative G), ∀ (g : G) (f : ↥(MeasureTheory.Lp ℂ 1 μ)), ω ⟨(π.integratedOperatorL1 hcont hbdd μ) ((MeasureTheory.Lp.compMeasurePreserving (fun (t : G) => -g + t) ⋯) f), ⋯⟩ = ↑(χ (Multiplicative.ofAdd g)) * ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩

A nonvanishing character of an algebra containing the integrated form of a strongly continuous unitary representation detects a unique continuous group character. Its value is the multiplier on every integrated operator, independently of the witnessing weight.