Documentation

TauCeti.Analysis.CStarAlgebra.Action.Convolution.Basic

Twisted convolution of compactly supported coefficient functions #

For a point-norm continuous action α of a topological group G on a C⋆-algebra A and a measure μ on G, the twisted convolution of compactly supported continuous functions f g : C_c(G, A) is

(f ⋆ g) s = ∫ r, f r * α r (g (r⁻¹ * s)) ∂μ.

This is the multiplication of the convolution algebra whose completions are the crossed products of the C⋆-dynamical system (A, G, α). We show that f ⋆ g is again continuous and compactly supported, with support (f ⋆ g) ⊆ support f * support g, and bundle the product as a ℂ-bilinear map. For a left-invariant measure we prove associativity and the L¹ estimate ∫ ‖f ⋆ g‖ ≤ (∫ ‖f‖) * ∫ ‖g‖.

Neither local compactness, separability nor σ-finiteness of μ is assumed: the measure only has to be finite on compact sets. Continuity of the parametric integrals comes from continuousOn_integral_of_compact_support, and the order of integration is exchanged with integral_integral_swap_of_hasCompactSupport, a Fubini theorem for compactly supported continuous functions which needs no σ-finiteness.

The conventions follow Dana Williams, Crossed Products of C-Algebras*, Chapter 2.

Main definitions #

Main statements #

The twisted integrand #

source
theorem TauCeti.CStarAction.integrable_integrand {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] (α : CStarAction G A) (f g : CompactlySupportedContinuousMap G A) [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (s : G) :
MeasureTheory.Integrable (fun (r : G) => f r * (α r) (g (r⁻¹ * s))) μ

The twisted convolution integrand is integrable against any measure finite on compact sets.

The twisted convolution #

source
noncomputable def TauCeti.CStarAction.convolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] :
CompactlySupportedContinuousMap G A →ₗ[ℂ] CompactlySupportedContinuousMap G A →ₗ[ℂ] CompactlySupportedContinuousMap G A

The twisted convolution (f ⋆ g) s = ∫ r, f r * α r (g (r⁻¹ * s)) ∂μ on C_c(G, A), as a ℂ-bilinear map.

Instances For
    source
    @[simp]
    theorem TauCeti.CStarAction.convolution_apply {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g : CompactlySupportedContinuousMap G A) (s : G) :
    (((α.convolution μ) f) g) s = ∫ (r : G), f r * (α r) (g (r⁻¹ * s)) ∂μ
    source
    theorem TauCeti.CStarAction.support_convolution_subset {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g : CompactlySupportedContinuousMap G A) :
    Function.support ⇑(((α.convolution μ) f) g) ⊆ Function.support ⇑f * Function.support ⇑g

    A twisted convolution is supported in the product of the supports.

    source
    theorem TauCeti.CStarAction.smul_convolution {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g : CompactlySupportedContinuousMap G A) (a : A) :
    ((α.convolution μ) (a • f)) g = a • ((α.convolution μ) f) g

    Left multiplication by a coefficient commutes with twisted convolution: (a • f) ⋆ g = a • (f ⋆ g).

    Left-invariant measures #

    source
    theorem TauCeti.CStarAction.convolution_assoc {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g h : CompactlySupportedContinuousMap G A) [MeasurableMul G] [μ.IsMulLeftInvariant] :
    ((α.convolution μ) (((α.convolution μ) f) g)) h = ((α.convolution μ) f) (((α.convolution μ) g) h)

    Twisted convolution with respect to a left-invariant measure is associative.

    source
    theorem TauCeti.CStarAction.integral_norm_convolution_le {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [IsTopologicalGroup G] [MeasurableSpace G] [OpensMeasurableSpace G] (α : CStarAction G A) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f g : CompactlySupportedContinuousMap G A) [MeasurableMul G] [μ.IsMulLeftInvariant] :
    ∫ (s : G), ‖(((α.convolution μ) f) g) s‖ ∂μ ≤ (∫ (s : G), ‖f s‖ ∂μ) * ∫ (s : G), ‖g s‖ ∂μ

    The L¹ norm is submultiplicative for twisted convolution with respect to a left-invariant measure.