The GNS translation representation of a positive-definite function

A positive-definite function on an additive commutative group has a canonical Hilbert space, obtained from its translation-invariant positive-definite kernel. Translation of the kernel vectors extends uniquely to a unitary operator. These operators form a group representation, and the original function is a matrix coefficient of its vector at zero.

The translation action is part of the GNS/Kolmogorov decomposition of a positive-definite function. Its later use in LCA Bochner theory requires spectral measures and Pontryagin duality.

References

• W. Rudin, Fourier Analysis on Groups (1962), Chapter 1.

@[reducible, inline]

abbrev TauCeti.IsPositiveDefiniteSub.gnsSpace {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : Type u_1

The canonical Hilbert space of the translation-invariant kernel K(a,b) = F(a-b).

Equations

• hF.gnsSpace = ⋯.KolmogorovSpace

noncomputable def TauCeti.IsPositiveDefiniteSub.gnsVector {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a : G) : hF.gnsSpace

The vector in the GNS space corresponding to a group element.

Equations

• hF.gnsVector a = ⋯.kolmogorovFeature a

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.inner_gnsVector {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a b : G) : inner ℂ (hF.gnsVector a) (hF.gnsVector b) = F (a - b)

The inner product of two GNS vectors is the original positive-definite kernel.

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.norm_gnsVector_sub_sq {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (a b : G) : ‖hF.gnsVector a - hF.gnsVector b‖ ^ 2 = 2 * ((F 0).re - (F (a - b)).re)

Squared distances between GNS vectors are controlled by the real part of the function.

theorem TauCeti.IsPositiveDefiniteSub.gnsVector_dense {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : (Submodule.span ℂ (Set.range hF.gnsVector)).topologicalClosure = ⊤

The GNS vectors span a dense subspace.

noncomputable def TauCeti.IsPositiveDefiniteSub.gnsTranslation {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (g : G) : hF.gnsSpace ≃ₗᵢ[ℂ] hF.gnsSpace

Translation by g is a unitary operator on the canonical GNS Hilbert space. Its action on the dense family of kernel vectors is v(a) ↦ v(g+a).

Equations

• hF.gnsTranslation g = ⋯.kolmogorovEquiv (fun (a : G) => hF.gnsVector (g + a)) ⋯ ⋯

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.gnsTranslation_gnsVector {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (g a : G) : (hF.gnsTranslation g) (hF.gnsVector a) = hF.gnsVector (g + a)

Translation acts on the canonical GNS vectors by addition.

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.gnsTranslation_zero {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : hF.gnsTranslation 0 = LinearIsometryEquiv.refl ℂ hF.gnsSpace

The translation at zero is the identity operator.

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.gnsTranslation_add {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (g k : G) : hF.gnsTranslation (g + k) = (hF.gnsTranslation k).trans (hF.gnsTranslation g)

GNS translations compose according to the group law.

noncomputable def TauCeti.IsPositiveDefiniteSub.gnsRepresentation {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) : Multiplicative G →* hF.gnsSpace ≃ₗᵢ[ℂ] hF.gnsSpace

The GNS representation as a homomorphism from the multiplicative copy of G to the unitary operators on its canonical Hilbert space.

Equations

• hF.gnsRepresentation = MonoidHom.mk' (fun (g : Multiplicative G) => hF.gnsTranslation (Multiplicative.toAdd g)) ⋯

@[simp]

theorem TauCeti.IsPositiveDefiniteSub.gnsRepresentation_ofAdd {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (g : G) : hF.gnsRepresentation (Multiplicative.ofAdd g) = hF.gnsTranslation g

The representation operator at g is translation by g.

theorem TauCeti.IsPositiveDefiniteSub.gnsRepresentation_gnsVector {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (g a : G) : (hF.gnsRepresentation (Multiplicative.ofAdd g)) (hF.gnsVector a) = hF.gnsVector (g + a)

The representation translates each GNS vector.

theorem TauCeti.IsPositiveDefiniteSub.eq_inner_gnsRepresentation {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) (g : G) : F g = inner ℂ ((hF.gnsRepresentation (Multiplicative.ofAdd g)) (hF.gnsVector 0)) (hF.gnsVector 0)

A positive-definite function is a matrix coefficient of its canonical unitary representation.

theorem TauCeti.IsPositiveDefiniteSub.continuous_gnsVector {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) [TopologicalSpace G] [IsTopologicalAddGroup G] (hcont : ContinuousAt F 0) : Continuous hF.gnsVector

Continuity of a positive-definite function at zero makes its canonical feature map continuous. This is the regularity needed for a strongly continuous representation.

theorem TauCeti.IsPositiveDefiniteSub.continuous_gnsTranslation_apply {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) [TopologicalSpace G] [IsTopologicalAddGroup G] (hcont : ContinuousAt F 0) (x : hF.gnsSpace) : Continuous fun (g : G) => (hF.gnsTranslation g) x

The GNS translation representation is strongly continuous: every vector has a continuous orbit.

theorem TauCeti.IsPositiveDefiniteSub.continuous_gnsRepresentation_apply {G : Type u_1} [AddCommGroup G] {F : G → ℂ} (hF : IsPositiveDefiniteSub F) [TopologicalSpace G] [IsTopologicalAddGroup G] (hcont : ContinuousAt F 0) (x : hF.gnsSpace) : Continuous fun (g : Multiplicative G) => (hF.gnsRepresentation g) x

The canonical unitary representation has continuous orbits.