The integrated form of a strongly continuous representation #
Let π be a representation of an additive topological group G (written multiplicatively, as a
ContRepresentation of Multiplicative G) on a normed space E, which is strongly continuous
(every orbit g ↦ π g v is continuous) and uniformly bounded, and let μ be a measure on G. An
integrable weight f then acts on E by the integrated form
π(f) v = ∫ g, f g • π g v ∂μ,
a bounded operator with ‖π(f)‖ ≤ C * ‖f‖₁ when ‖π g‖ ≤ C. This file builds the map
f ↦ π(f) as a continuous linear map L¹(G, μ) →L E →L E and proves the identities that make it a
representation of the convolution algebra L¹(G): translating the weight composes with π,
convolution of weights becomes composition of operators, and, for a unitary π and an
inversion-invariant μ, adjoints correspond to the involution f^*(g) = conj (f (-g)).
For abelian G, the integrated operators commute for any measure; they are also normal
when π is unitary and μ is inversion-invariant.
The integrated form is how a strongly continuous representation is handled by operator algebra:
the operators π g themselves depend on g only strongly continuously, but the left translates
π h ∘L π(f) depend continuously on h in the operator norm. Applied to the GNS representation of
a continuous positive-definite function on a locally compact abelian group, the commutative
algebra of operators π(f) is the standard source of the representing measure in Bochner's
theorem (Folland, Chapter 4).
Main definitions #
ContRepresentation.integratedOperatorL1: the integrated formf ↦ π(f), as a bounded linear map fromL¹(G, μ)to the bounded operators onE.
Main statements #
ContRepresentation.integratedOperatorL1_apply,ContRepresentation.integratedOperatorL1_toL1: the pointwise formulaπ(f) v = ∫ g, f g • π g v ∂μ.ContRepresentation.norm_integratedOperatorL1_le:‖π(f)‖ ≤ C * ‖f‖₁when‖π g‖ ≤ C.ContRepresentation.comp_integratedOperatorL1:π h ∘L π(f) = π(f (-h + ·))for a left-invariant measure.ContRepresentation.continuous_comp_integratedOperatorL1:h ↦ π h ∘L π(f)is continuous in the operator norm.ContRepresentation.integratedOperatorL1_convolution:π(f₁ ⋆ f₂) = π(f₁) ∘L π(f₂)on an abelian group with a right-invariant measure.ContRepresentation.integratedOperatorL1_commute: integrated operators commute on an abelian group with any measure.ContRepresentation.inner_integratedOperatorL1_apply: the matrix coefficients⟪w, π(f) v⟫ = ∫ g, f g * ⟪w, π g v⟫ ∂μ.ContRepresentation.adjoint_integratedOperatorL1:π(f)† = π(f^*)for a unitaryπ.ContRepresentation.isStarNormal_integratedOperatorL1: integrated operators of a unitary abelian-group representation are normal for an inversion-invariant measure.ContRepresentation.tendsto_integratedOperatorL1_apply: weights of unit integral and boundedL¹norm concentrating at0form an approximate identity,π(f i) v → v.ContRepresentation.mem_closure_range_integratedOperatorL1_apply: the integrated form is nondegenerate, everyvbeing a limit of vectorsπ(f) v.
Implementation notes #
The definition integrates the orbits g ↦ f g • π g v pointwise in v and only then bundles the
result into an operator. The operator-valued map g ↦ π g need not be strongly measurable for the
operator norm: for the regular representation of ℝ on L²(ℝ), distinct translations are at
operator distance 2, so the map is not almost everywhere separably valued, and π(f) cannot be
written as a Bochner integral in E →L E. This is also why
TauCeti.ContRepresentation.integratedOperator, which averages a norm-continuous representation
of a compact group against a continuous weight, does not apply here. The strong continuity and the
uniform bound are hypotheses of the definition: they are exactly what makes the integrand
integrable, and they hold for the unitary representations that are the main application.
Measurability of the integrands g ↦ f g • π g v is read off from the continuity of the orbits and
the inner regularity of μ for compact sets
(MeasureTheory.AEFinStronglyMeasurable.aestronglyMeasurable_smul): an integrable weight lives on a
σ-finite set, which up to a null set is a countable union of compact sets with separable images.
The Haar measure MeasureTheory.Measure.addHaar of a locally compact group is regular, hence has
this property, so no second countability of G or separability of E is needed. Only the
convolution identity, which integrates over G × G, still asks for
SecondCountableTopologyEither G E.
References #
- G. B. Folland, A Course in Abstract Harmonic Analysis, 2nd ed., CRC Press (2016), §3.2.
The integrated form of a strongly continuous, uniformly bounded representation π of an
additive group G (written multiplicatively as Multiplicative G): the bounded operator
π(f) = ∫ g, f g • π g ∂μ attached to an integrable weight f, defined pointwise by the Bochner
integral π(f) v = ∫ g, f g • π g v ∂μ of the continuous orbit g ↦ π g v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The integrated form acts on a vector by integrating its orbit against the weight.
The integrated form of the class of an integrable function.
The integrated form is bounded by the uniform bound of the representation times the L¹
norm of the weight.
Translating the weight on the left by h amounts to composing the integrated form with
π h.
Although π is only strongly continuous, h ↦ π h ∘L π(f) is continuous in the operator norm:
by comp_integratedOperatorL1 it is the integrated form of the left translates of f, which
depend continuously on h in L¹.
Every action operator of a representation of an abelian group commutes with its integrated operators. No invariance hypothesis on the measure is needed.
Integrated operators of an abelian-group representation commute for any measure.
The integrated form turns convolution of weights into composition of operators:
π(f₁ ⋆ f₂) = π(f₁) ∘L π(f₂).
Matrix coefficients of the integrated form are the integrals of the matrix coefficients of the representation against the weight.
The adjoint of the integrated form of a unitary representation is the integrated form of the
involuted weight g ↦ conj (f (-g)).
The integrated operators of a unitary abelian-group representation are normal.
Approximate identities for the integrated form. If the weights f i eventually have unit
integral and L¹ norm at most C, and concentrate at 0 (for every neighbourhood U of 0,
eventually f i vanishes almost everywhere outside U), then π(f i) tends strongly to the
identity: π(f i) v → v for every v.
The integrated form is nondegenerate. For a measure positive on nonempty open sets and
finite on some neighbourhood of each point, such as a Haar measure on a locally compact group, every
vector v is a limit of vectors π(f) v.