Haar averaging projects onto the invariants, and the character integral counts them

For a finite group G whose order is invertible in the scalars, Mathlib averages the action operators of a representation over the group and gets a projection onto the invariant subspace (Representation.averageMap, Representation.isProj_averageMap). This file is the compact-group form of that construction: the finite average is replaced by the Haar integral

haarAverageMap π hπ = ∫ g, π g ∂(haarProb G),

the integrated operator of the constant function 1, and normalized Haar measure plays the role of the factor 1/|G| — it is what makes the average of a constant that constant, so that the operator restricts to the identity on the invariants.

The two invariance properties of the average are the two translation invariances of Haar measure: left invariance gives π h ∘ P = P, and right invariance — unimodularity, automatic on a compact group — gives P ∘ π h = P. Together they make P a self-intertwiner whose image is exactly the invariant subspace ContRepresentation.invariants, and P is idempotent because it fixes that image pointwise.

In finite dimension the trace of a projection is the dimension of its image, and the trace of the integrated operator is the Haar integral of the character (TauCeti.ContRepresentation.trace_integratedOperator). The two readings of the same trace give the counting theorem

dim V^G = ∫ g, χ_π g ∂(haarProb G),

the compact form of the finite-group identity dim V^G = |G|⁻¹ ∑ χ_π g. It is the tool that turns character integrals into dimensions: applied to the symmetric and exterior squares it computes the Frobenius-Schur indicator, and applied to Hom(V, W) it computes the dimension of the space of intertwiners V → W (which for complex scalars and irreducible V is the multiplicity of V in W, but over ℝ counts each copy with the dimension of its endomorphism division algebra).

Main definitions

• ContRepresentation.haarAverageMap: the Haar average ∫ g, π g of the action operators.

Main results

• ContRepresentation.isProj_haarAverageMap: the Haar average is a projection onto the invariant subspace, with ContRepresentation.range_haarAverageMap identifying its range and ContRepresentation.haarAverageMap_comp_self its idempotence.
• ContRepresentation.trace_haarAverageMap: its trace is ∫ g, χ_π g.
• ContRepresentation.integral_character_eq_finrank_invariants: the Haar integral of the character is the dimension of the invariants.
• ContRepresentation.integral_character_eq_zero_iff: that integral vanishes exactly when there is no nonzero invariant vector.

Implementation notes

haarAverageMap is defined as integratedOperator π hπ 1 rather than as a fresh Haar average, so that the trace computation is the one already proved for the integrated operator and no second Bochner-integral bookkeeping is needed. Its two invariance lemmas are proved vectorwise from TauCeti.haarAverage_comp_mulLeft and TauCeti.haarAverage_comp_mulRight, applied to the orbit map g ↦ π g v, and not from the class-function machinery of TauCeti/RepresentationTheory/Compact/Integrated.lean: the constant function 1 is a class function, but that route yields only conjugation invariance, which is strictly weaker than the one-sided invariance used here.

The invariant subspace is Mathlib's ContRepresentation.invariants, not a new definition, and the projection is packaged through Mathlib's LinearMap.IsProj so that LinearMap.IsProj.trace applies verbatim.

The declarations here live in the root ContRepresentation namespace, so that π.haarAverageMap hπ elaborates, rather than in TauCeti.ContRepresentation alongside the integrated operator they are built from; the older namespace is opened to reach that operator. The character and its formulas are methods in ContRepresentation.

References

This projection is the trivial-isotypic case of the character-weighted projections in TauCeti/RepresentationTheory/Compact/Character/Projection.lean. Its multiplicity count is used for the Frobenius-Schur indicator ∫ g, χ_π (g * g), whose trichotomy reads that integral as the difference of the dimensions of the invariants of the symmetric and exterior squares. The mathematical development follows Daniel Bump, Lie Groups, second edition, Chapter 2, and T. Bröcker and T. tom Dieck, Representations of Compact Lie Groups, Springer GTM 98 (1985), Chapter II.

noncomputable def ContRepresentation.haarAverageMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : V →L[𝕜] V

The Haar average of the action operators ∫ g, π g ∂(haarProb G), the integrated operator of the constant function 1.

This is the compact-group form of Mathlib's Representation.averageMap: normalized Haar measure replaces the factor 1/|G|, and the results below show that it is again a projection onto the invariant subspace.

Equations

• π.haarAverageMap hπ = TauCeti.ContRepresentation.integratedOperator π hπ 1

theorem ContRepresentation.haarAverageMap_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) : (π.haarAverageMap hπ) v = ∫ (g : G), (π g) v ∂TauCeti.haarProb G

The Haar average of the action operators, evaluated at a vector.

The two invariances

Left invariance of Haar measure makes the average absorb the action on the left, right invariance — unimodularity, which a compact group has — makes it absorb the action on the right. Both are read off TauCeti.haarAverage_comp_mulLeft and TauCeti.haarAverage_comp_mulRight, once the two translates of the orbit map are identified.

@[simp]

theorem ContRepresentation.comp_haarAverageMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (h : G) : π h ∘SL π.haarAverageMap hπ = π.haarAverageMap hπ

The Haar average absorbs the action on the left: π h ∘ P = P. This is left invariance of normalized Haar measure.

@[simp]

theorem ContRepresentation.comp_haarAverageMap_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (h : G) (v : V) : (π h) ((π.haarAverageMap hπ) v) = (π.haarAverageMap hπ) v

The Haar average absorbs the action on the left, applied to a vector: π h (P v) = P v.

@[simp]

theorem ContRepresentation.haarAverageMap_comp {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (h : G) : π.haarAverageMap hπ ∘SL π h = π.haarAverageMap hπ

The Haar average absorbs the action on the right: P ∘ π h = P. This is right invariance of normalized Haar measure, which holds because a compact group is unimodular.

@[simp]

theorem ContRepresentation.haarAverageMap_comp_apply {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (h : G) (v : V) : (π.haarAverageMap hπ) ((π h) v) = (π.haarAverageMap hπ) v

The Haar average absorbs the action on the right, applied to a vector: P (π h v) = P v.

The projection onto the invariants

theorem ContRepresentation.haarAverageMap_invariant {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) : (π.haarAverageMap hπ) v ∈ π.invariants

The Haar average lands in the invariant subspace. This is not itself a simp lemma — its statement is not in simp normal form, since ContRepresentation.mem_invariants unfolds the membership — but simp proves it from ContRepresentation.comp_haarAverageMap_apply.

@[simp]

theorem ContRepresentation.haarAverageMap_id {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) {v : V} (hv : v ∈ π.invariants) : (π.haarAverageMap hπ) v = v

The Haar average is the identity on the invariant subspace: the integrand is then constant, and normalized Haar measure has total mass one.

theorem ContRepresentation.isProj_haarAverageMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : LinearMap.IsProj π.invariants ↑(π.haarAverageMap hπ)

Haar averaging is a projection onto the invariants.

@[simp]

theorem ContRepresentation.haarAverageMap_comp_self {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : π.haarAverageMap hπ ∘SL π.haarAverageMap hπ = π.haarAverageMap hπ

The Haar average is idempotent.

@[simp]

theorem ContRepresentation.range_haarAverageMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : (↑(π.haarAverageMap hπ)).range = π.invariants

The range of the Haar average is exactly the invariant subspace.

theorem ContRepresentation.instCompleteSpaceInvariants {𝕜 : Type u_1} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] : CompleteSpace V

Completeness of V is not an extra hypothesis on the results below: a finite-dimensional normed space over an RCLike field is already complete. Mathlib keeps FiniteDimensional.complete out of the global instance set, so it is installed here as a local instance instead, exactly as in TauCeti/RepresentationTheory/Compact/Integrated.lean.

theorem ContRepresentation.trace_haarAverageMap {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : (LinearMap.trace 𝕜 V) ↑(π.haarAverageMap hπ) = ∫ (g : G), (π.character hπ) g ∂TauCeti.haarProb G

The trace of the Haar average of the action operators is the Haar integral of the character.

theorem ContRepresentation.integral_character_eq_finrank_invariants {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : ∫ (g : G), (π.character hπ) g ∂TauCeti.haarProb G = ↑(Module.finrank 𝕜 ↥π.invariants)

The Haar integral of the character is the dimension of the invariants, ∫ g, χ_π g ∂(haarProb G) = dim V^G.

Both sides are the trace of the Haar average ∫ g, π g: on the left because the trace of an integrated operator is the integral of the traces, on the right because that average is a projection onto the invariants. This is the compact-group form of the finite-group count dim V^G = |G|⁻¹ ∑ g, χ_π g, and the tool that turns character integrals into dimensions.

theorem ContRepresentation.integral_character_eq_zero_iff {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : ∫ (g : G), (π.character hπ) g ∂TauCeti.haarProb G = 0 ↔ π.invariants = ⊥

The character integral vanishes exactly when there is no nonzero invariant vector.