Vector-valued integrated forms of covariant pairs

For a compactly supported continuous coefficient function f, the integrated form is the bounded operator v ↦ ∫ g, π (f g) (U g v). Integration is in the Hilbert space, not in the operator-norm space: strong continuity of U does not imply norm continuity. The operator depends linearly on f and has norm at most ∫ g, ‖f g‖. No separability, second countability, or σ-finiteness is needed. For the definition, the norm bound and the covariance identity the measure need only be finite on compact sets; left invariance enters only for multiplicativity under twisted convolution.

Covariance moves a coefficient on the right of an integrated operator inside its integral with the action twist, while a coefficient on the left comes from the pointwise left multiplier, (π ⋊ U)(a • f) = π(a) (π ⋊ U)(f). For scalar multiples of a fixed coefficient, the construction agrees with ContRepresentation.integratedOperatorL1, after pulling the group representation back along MulEquiv.multiplicativeAdditive.

For a left-invariant measure the integrated form is multiplicative for twisted convolution, (π ⋊ U) (f ⋆ g) = (π ⋊ U) f * (π ⋊ U) g, and turns the twisted left translation CStarAction.translate into the group representation, (π ⋊ U)(r • f) = U_r (π ⋊ U)(f). The order of integration is exchanged by Fubini's theorem for compactly supported continuous functions, so σ-finiteness is still not needed. Extension to coefficient-valued L¹ and the involution identity require additional arguments.

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

theorem TauCeti.CStarAction.CovariantRepresentation.continuous_integrand {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (f : CompactlySupportedContinuousMap G A) (v : H) : Continuous fun (g : G) => (P.coefficient (f g)) ((P.group g) v)

The vector integrand of the integrated form is continuous.

theorem TauCeti.CStarAction.CovariantRepresentation.hasCompactSupport_integrand {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (f : CompactlySupportedContinuousMap G A) (v : H) : HasCompactSupport fun (g : G) => (P.coefficient (f g)) ((P.group g) v)

The vector integrand vanishes outside the support of the coefficient function.

theorem TauCeti.CStarAction.CovariantRepresentation.integrable_integrand {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap G A) (v : H) : MeasureTheory.Integrable (fun (g : G) => (P.coefficient (f g)) ((P.group g) v)) μ

Compact support makes every vector integrand integrable.

noncomputable def TauCeti.CStarAction.CovariantRepresentation.integratedOperator {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] : CompactlySupportedContinuousMap G A →ₗ[ℂ] H →L[ℂ] H

The integrated form on compactly supported coefficient functions, defined by vector integration rather than operator-valued Bochner integration.

theorem TauCeti.CStarAction.CovariantRepresentation.integratedOperator_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap G A) (v : H) : ((P.integratedOperator μ) f) v = ∫ (g : G), (P.coefficient (f g)) ((P.group g) v) ∂μ

The defining vector formula for the integrated form.

theorem TauCeti.CStarAction.CovariantRepresentation.norm_integratedOperator_le {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap G A) : ‖(P.integratedOperator μ) f‖ ≤ ∫ (g : G), ‖f g‖ ∂μ

The integrated form is bounded by the coefficient function's L¹ norm.

theorem TauCeti.CStarAction.CovariantRepresentation.inner_integratedOperator_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap G A) (w v : H) : inner ℂ w (((P.integratedOperator μ) f) v) = ∫ (g : G), inner ℂ w ((P.coefficient (f g)) ((P.group g) v)) ∂μ

Matrix coefficients can be computed by integrating vector matrix coefficients.

theorem TauCeti.CStarAction.CovariantRepresentation.integratedOperator_coefficient_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (f : CompactlySupportedContinuousMap G A) (a : A) (v : H) : ((P.integratedOperator μ) f) ((P.coefficient a) v) = ∫ (g : G), (P.coefficient (f g * (α g) a)) ((P.group g) v) ∂μ

A coefficient on the right moves inside the integral with the action twist.

@[simp]

theorem TauCeti.CStarAction.CovariantRepresentation.integratedOperator_smul {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] (a : A) (f : CompactlySupportedContinuousMap G A) : (P.integratedOperator μ) (a • f) = P.coefficient a * (P.integratedOperator μ) f

The integrated form turns left multiplication by a coefficient into the coefficient representation: (π ⋊ U)(a • f) = π(a) (π ⋊ U)(f).

theorem TauCeti.CStarAction.CovariantRepresentation.integral_coefficient_apply {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) {X : Type u_4} [MeasurableSpace X] {ν : MeasureTheory.Measure X} {F : X → A} (hF : MeasureTheory.Integrable F ν) (w : H) : ∫ (x : X), (P.coefficient (F x)) w ∂ν = (P.coefficient (∫ (x : X), F x ∂ν)) w

Vector evaluation of the coefficient representation commutes with Bochner integration.

@[simp]

theorem TauCeti.CStarAction.CovariantRepresentation.integratedOperator_convolution {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [IsTopologicalGroup G] [MeasurableMul G] [μ.IsMulLeftInvariant] (f g : CompactlySupportedContinuousMap G A) : (P.integratedOperator μ) (((α.convolution μ) f) g) = (P.integratedOperator μ) f * (P.integratedOperator μ) g

The integrated form of a covariant pair is multiplicative for twisted convolution with respect to a left-invariant measure: (π ⋊ U) (f ⋆ g) = (π ⋊ U) f * (π ⋊ U) g.

@[simp]

theorem TauCeti.CStarAction.CovariantRepresentation.integratedOperator_translate {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [IsTopologicalGroup G] [MeasurableMul G] [μ.IsMulLeftInvariant] (r : G) (f : CompactlySupportedContinuousMap G A) : (P.integratedOperator μ) ((α.translate r) f) = P.group r * (P.integratedOperator μ) f

The integrated form turns the twisted left translation into the group representation: (π ⋊ U)(r • f) = U_r (π ⋊ U)(f).

@[reducible]

def TauCeti.CStarAction.CovariantRepresentation.instMeasurableSpaceAdditive {G : Type u_1} [MeasurableSpace G] : MeasurableSpace (Additive G)

Use the original measurable structure on the additive tag for the scalar comparison. Reducibility keeps the measure and its L¹ space unchanged.

theorem TauCeti.CStarAction.CovariantRepresentation.instR1SpaceAdditive {G : Type u_1} [TopologicalSpace G] [R1Space G] : R1Space (Additive G)

theorem TauCeti.CStarAction.CovariantRepresentation.instBorelSpaceAdditive {G : Type u_1} [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] : BorelSpace (Additive G)

theorem TauCeti.CStarAction.CovariantRepresentation.instInnerRegularCompactLTTopAdditive {G : Type u_1} [TopologicalSpace G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) [μ.InnerRegularCompactLTTop] : μ.InnerRegularCompactLTTop

theorem TauCeti.CStarAction.CovariantRepresentation.integratedOperator_eq_coefficient_mul_integratedOperatorL1 {G : Type u_1} {A : Type u_2} {H : Type u_3} [Group G] [TopologicalSpace G] [MeasurableSpace G] [OpensMeasurableSpace G] [NonUnitalCStarAlgebra A] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {α : CStarAction G A} (P : α.CovariantRepresentation H) (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasureOnCompacts μ] [R1Space G] [BorelSpace G] [μ.InnerRegularCompactLTTop] (f : CompactlySupportedContinuousMap G A) (φ : CompactlySupportedContinuousMap G ℂ) (a : A) (hf : ∀ (g : G), f g = φ g • a) : (P.integratedOperator μ) f = P.coefficient a * ((P.group.restrict (MulEquiv.multiplicativeAdditive G).toMonoidHom).integratedOperatorL1 ⋯ ⋯ μ) (MeasureTheory.Integrable.toL1 ⇑φ ⋯)

On scalar multiples of a fixed coefficient, the integrated form factors through the existing scalar L¹ integrated form. The tagging equivalence permits an arbitrary multiplicative group. In particular, for the canonical scalar coefficient representation this recovers precisely the scalar integrated operator.