Continuity of the integrated-character parameter

Let π be a strongly continuous unitary representation of an abelian topological group equipped with a regular invariant measure, and let A be a complete star subalgebra containing all integrated operators. A character of A that is nonzero on some integrated operator determines a continuous group character by ContRepresentation.existsUnique_pontryaginDual_of_integratedOperatorL1.

This file packages the characters on which that construction is defined and proves that the resulting map to the Pontryagin dual is continuous. Near a character ω, choose an integrated operator π(f) on which ω is nonzero. The detected group character then has the local formula

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

The numerator is jointly continuous in ω and g: norm continuity of translated integrated operators combines with weak-* continuity of evaluation and the uniform norm bound on characters of a Banach algebra. The denominator remains nonzero in a neighbourhood of ω, so the displayed quotient proves the required local continuity. This continuity is the input needed to push a character-space spectral measure to the Pontryagin dual.

Main declarations

• ContRepresentation.integratedCharacterSet: algebra characters that do not annihilate every integrated operator.
• ContRepresentation.integratedCharacterToPontryaginDual: the group character detected by an integrated-algebra character.
• ContRepresentation.continuous_integratedCharacterToPontryaginDual: continuity of this assignment.

References

• G. B. Folland, A Course in Abstract Harmonic Analysis, second edition, §§3.2 and 4.4.
• The local-quotient continuity proof generalizes Tau Ceti's earlier formalization in TauCeti.StronglyContinuousSpectral.continuousOn_dual (TauCeti.Analysis.Fourier.Pontryagin.StronglyContinuous), which was stated for the integrated algebra of a unitary representation with respect to a Haar measure.

def ContRepresentation.integratedCharacterSet {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} [μ.InnerRegularCompactLTTop] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) : Set ↑(WeakDual.characterSpace ℂ ↥A)

The characters of an algebra containing the integrated form which do not annihilate every integrated operator. When π is unitary, these are exactly the algebra characters from which the representation detects a point of the Pontryagin dual.

Equations

• π.integratedCharacterSet hcont hbdd A hA = {ω : ↑(WeakDual.characterSpace ℂ ↥A) | ∃ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩ ≠ 0}

@[simp]

theorem ContRepresentation.mem_integratedCharacterSet_iff {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} [μ.InnerRegularCompactLTTop] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) (ω : ↑(WeakDual.characterSpace ℂ ↥A)) : ω ∈ π.integratedCharacterSet hcont hbdd A hA ↔ ∃ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩ ≠ 0

Membership in the integrated-character set means nonvanishing on some integrated operator.

theorem ContRepresentation.isOpen_integratedCharacterSet {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} [μ.InnerRegularCompactLTTop] (π : ContRepresentation ℂ (Multiplicative G) H) (hcont : ∀ (v : H), Continuous fun (g : G) => (π (Multiplicative.ofAdd g)) v) (hbdd : ∃ (C : ℝ), ∀ (g : Multiplicative G), ‖π g‖ ≤ C) (A : StarSubalgebra ℂ (H →L[ℂ] H)) (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) : IsOpen (π.integratedCharacterSet hcont hbdd A hA)

The integrated-character set is open in the character space.

noncomputable def ContRepresentation.integratedCharacterToPontryaginDual {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) (A : StarSubalgebra ℂ (H →L[ℂ] H)) [CompleteSpace ↥A] (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) (hπ : π.IsUnitary) (ω : ↑(π.integratedCharacterSet hcont hbdd A hA)) : PontryaginDual (Multiplicative G)

The continuous group character detected by an algebra character that does not annihilate the integrated form.

Equations

• π.integratedCharacterToPontryaginDual hcont hbdd A hA hπ ω = Classical.choose ⋯

theorem ContRepresentation.integratedCharacterToPontryaginDual_spec {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) (A : StarSubalgebra ℂ (H →L[ℂ] H)) [CompleteSpace ↥A] (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) (hπ : π.IsUnitary) (ω : ↑(π.integratedCharacterSet hcont hbdd A hA)) (g : G) (f : ↥(MeasureTheory.Lp ℂ 1 μ)) : ↑ω ⟨(π.integratedOperatorL1 hcont hbdd μ) ((MeasureTheory.Lp.compMeasurePreserving (fun (t : G) => -g + t) ⋯) f), ⋯⟩ = ↑((π.integratedCharacterToPontryaginDual hcont hbdd A hA hπ ω) (Multiplicative.ofAdd g)) * ↑ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩

The defining multiplier identity for the group character detected by an integrated character.

theorem ContRepresentation.coe_integratedCharacterToPontryaginDual_apply_eq_div {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) (A : StarSubalgebra ℂ (H →L[ℂ] H)) [CompleteSpace ↥A] (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) (hπ : π.IsUnitary) (ω : ↑(π.integratedCharacterSet hcont hbdd A hA)) (g : G) (f : ↥(MeasureTheory.Lp ℂ 1 μ)) (hf : ↑ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩ ≠ 0) : ↑((π.integratedCharacterToPontryaginDual hcont hbdd A hA hπ ω) (Multiplicative.ofAdd g)) = ↑ω ⟨(π.integratedOperatorL1 hcont hbdd μ) ((MeasureTheory.Lp.compMeasurePreserving (fun (t : G) => -g + t) ⋯) f), ⋯⟩ / ↑ω ⟨(π.integratedOperatorL1 hcont hbdd μ) f, ⋯⟩

Local quotient formula for the group character detected by an integrated character.

theorem ContRepresentation.continuous_integratedCharacterToPontryaginDual {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) (A : StarSubalgebra ℂ (H →L[ℂ] H)) [CompleteSpace ↥A] (hA : ∀ (f : ↥(MeasureTheory.Lp ℂ 1 μ)), (π.integratedOperatorL1 hcont hbdd μ) f ∈ A) (hπ : π.IsUnitary) : Continuous (π.integratedCharacterToPontryaginDual hcont hbdd A hA hπ)

The group character detected by a nonvanishing integrated character depends continuously on the algebra character.