Finite groups: normalized Haar, the L² pairing, and orthogonality

A finite group carrying the discrete topology is a compact topological group, so the whole compact-group development applies to it. This file identifies the objects it produces with the elementary finite-group ones: normalized Haar measure is |G|⁻¹ • Measure.count, the Haar integral is the group average |G|⁻¹ ∑ g, F g, and the Haar average of the action operators of a representation is the finite group average |G|⁻¹ ∑ g, π g, the Reynolds operator. (Mathlib's algebraic counterpart of that operator is Representation.averageMap; this file does not connect to it, only to the explicit sum.)

Everything the compact theory phrases as an L²(G) inner product then becomes a finite Hermitian sum. Normalized Haar measure has full support on a discrete space and every function on a discrete space is continuous, so a class in Lp 𝕜 p (haarProb G) is a function on G — the coercion is a linear equivalence Lp 𝕜 p (haarProb G) ≃ₗ[𝕜] (G → 𝕜), for any exponent — and at p = 2 the inner product is |G|⁻¹ ∑ x, conj (f x) · g x. Rewriting the compact statements along that identity turns the two Schur orthogonality relations, and both branches — diagonal and off-diagonal — of the first (row) character orthogonality relation, into their classical finite-group forms, and turns the intertwiner count ∫ g, χ_π(g⁻¹) · χ_ρ(g) ∂haarProb G = dim Hom_G(V, W) into |G|⁻¹ ∑ g, χ_π(g⁻¹) · χ_ρ(g) = dim Hom_G(V, W), which is the shape Mathlib proves algebraically as Representation.card_inv_mul_sum_char_mul_char_eq_finrank. (For a unitary π that Haar integral is the L² inner product ⟪χ_π, χ_ρ⟫, but no unitarity is needed for the count.) Each such specialization carries the name of the compact statement it specializes, with the suffix _sum recording that the Haar integral has become a group average.

The measure statement is proved without appealing to the Haar property of the counting measure, and in fact without any topology: left invariance alone forces all singletons of a finite group to have the same measure c, so a left-invariant probability measure is c • Measure.count by MeasureTheory.Measure.ext_of_singleton, and evaluating both sides on Set.univ computes c = |G|⁻¹ from the total mass being 1.

Everything downstream then follows by rewriting: MeasureTheory.integral_fintype turns a Bochner integral against a measure on a finite space into the sum of its singleton weights, which the measure computation has just identified.

Main results

• TauCeti.eq_smul_count_of_isMulLeftInvariant: a left-invariant probability measure on a finite group is the normalized counting measure |G|⁻¹ • Measure.count. Since normalized Haar measure is one, TauCeti.haarProb_eq_smul_count is the special case that identifies it, and it also says that no other Haar probability measure exists; TauCeti.haarProb_singleton and TauCeti.haarProb_apply read off the measure of a singleton and of an arbitrary set.
• TauCeti.haarProb_eq_uniformOn_univ: it is Mathlib's uniform probability measure ProbabilityTheory.uniformOn Set.univ.
• TauCeti.integral_haarProb: the Haar integral is the group average |G|⁻¹ • ∑ g, F g, with TauCeti.integral_haarProb_eq_inv_mul_sum its 𝕜-scalar form; TauCeti.haarAverage_eq_smul_sum says the same for the bundled averaging operator.
• ContRepresentation.haarAverageMap_eq_smul_sum: the Haar average of the action operators is the finite average |G|⁻¹ • ∑ g, π g v.
• TauCeti.ae_haarProb_eq_top: normalized Haar measure on a finite discrete group has full support, so its almost-everywhere filter is ⊤ and, by TauCeti.eq_of_ae_eq_haarProb, two functions agreeing almost everywhere agree everywhere. This is what makes an L² class on a finite group a genuine function; TauCeti.coeFn_toLp_haarProb is the case of it used throughout, that the class of a continuous function is that function.
• TauCeti.lpHaarProbEquivFun: L²(G) is G → 𝕜, by the linear equivalence taking an Lp class to its values; the previous item is its injectivity and finiteness is its surjectivity. Nothing in it depends on the exponent, so it is stated for every p.
• TauCeti.finiteDimensional_lp_haarProb and TauCeti.finrank_lp_haarProb: Lp of a finite discrete group is finite-dimensional, of dimension |G|, being that space of functions.
• TauCeti.inner_Lp_haarProb_eq_inv_mul_sum: the L²(G) inner product is the normalized Hermitian pairing |G|⁻¹ ∑ x, conj (f x) · g x of those values, with TauCeti.inner_toLp_haarProb_eq_inv_mul_sum the form for two continuous functions.
• ContRepresentation.schur_orthogonality_self_sum, ContRepresentation.schur_orthogonality_distinct_sum and ContRepresentation.schur_orthogonality_sum: the two Schur orthogonality relations as finite averages of matrix coefficients, the middle one at the vanishing-intertwiner hypothesis of the compact theory and the last at a pair of inequivalent irreducibles, with ContRepresentation.schur_orthogonality_basis_sum the Kronecker-delta form of the first in an orthonormal basis.
• ContRepresentation.character_orthonormal_distinct_sum: the off-diagonal branch of the first (row) character orthogonality relation as a finite average. (The column sum over the irreducible characters, the second orthogonality relation, is not treated here.)
• ContRepresentation.inner_gramOperator_eq_inv_mul_sum: the invariant form the unitarian trick averages into existence is the finite average |G|⁻¹ ∑ g, ⟪π g v, π g w⟫, with ContRepresentation.gramOperator_eq_smul_sum the same identity at the level of the operator representing it and ContRepresentation.inner_gramOperator_self_eq_inv_mul_sum its diagonal.
• ContRepresentation.exists_isUnitary_congr_of_finite: the unitarian trick for a finite group, every finite-dimensional representation being conjugate to a unitary one.
• ContRepresentation.exists_orthogonal_irreducible_decomposition_of_finite: Maschke's theorem in orthogonal form, the finite shadow of complete reducibility: π itself is an internal direct sum of irreducible subrepresentations, orthogonal for the averaged inner product.

The counting identity |G|⁻¹ ∑ g, χ_π g = dim V^G that the compact-group character integral generalizes then costs one rewrite. It is not given a name: Mathlib already proves it, as Representation.card_inv_mul_sum_char_eq_finrank, and that lemma closes the ContRepresentation statement outright, so only the route through the compact theory is new. The intertwiner count |G|⁻¹ ∑ g, χ_π(g⁻¹) · χ_ρ(g) = dim Hom_G(V, W) is unnamed for the same reason: Mathlib proves it as Representation.card_inv_mul_sum_char_mul_char_eq_finrank, for the algebraic intertwiner space Representation.IntertwiningMap, which in finite dimensions is the continuous one because every linear map out of a finite-dimensional normed space is continuous. Both routes are exhibited by anonymous examples, as are both branches of Mathlib's Representation.char_orthonormal: the diagonal one is ContRepresentation.character_orthonormal_self read through the finite pairing — Mathlib and TauCeti.ClassFunction.characterPairing_ofCharacter_self both already prove that identity, so no name is claimed for it either — and the off-diagonal one is character_orthonormal_distinct_sum with its intertwiner hypothesis discharged, for a pair of inequivalent irreducibles, by the vanishing half of Schur's lemma.

Implementation notes

Finiteness is spelled [Finite G] wherever that suffices — the measure-theoretic statements and the equivalence TauCeti.lpHaarProbEquivFun — and [Fintype G] only where a sum over Finset.univ appears in the statement itself, since a Fintype instance recovered from Finite inside a proof would not be the one indexing that sum. The scalars and the exponent are weakened the same way: TauCeti.lpHaarProbEquivFun needs only [NontriviallyNormedField 𝕜] and an arbitrary exponent — not even [Fact (1 ≤ p)], since MeasureTheory.MemLp.of_discrete produces the class of a function at every exponent, whereas ContinuousMap.toLp, being a continuous linear map, needs a norm on Lp and hence that hypothesis — and [RCLike 𝕜] and p = 2 appear from the inner-product statements on. Cardinalities are written Nat.card G throughout; Nat.card_eq_fintype_card converts.

IsTopologicalGroup G, CompactSpace G, T2Space G and MeasurableSingletonClass G are all found by instance search from [DiscreteTopology G], [Finite G] and [BorelSpace G], so no extra hypotheses are carried. Continuity of a representation is likewise automatic, by continuous_of_discreteTopology, and is asked of the caller only where the statement needs it: the two pairing lemmas are about the L² classes matrixCoeffLp π hπ and characterLp π hπ, which take the continuity proof as an argument, so a caller of them holds one already. The orthogonality relations ask for none: the Schur ones are stated as bare sums ∑ g, ⟪π g v, w⟫ · …, and the character one uses Mathlib's Representation.character, which is by ContRepresentation.coe_character the function underlying character π hπ. Those statements mention no measure either, so they ask for no measurable structure on G: their proofs install borel G themselves, and the caller is left with a bare finite discrete group. The two Maschke statements go one step further: mentioning no topology on G at all, they have their proof install the discrete topology as well, and the caller is left with a bare finite group.

The scalar in the averaged sums is real, not 𝕜: the Bochner integral being specialized is an ℝ-integral, and V is not assumed to be an ℝ-𝕜-scalar tower. The conversion is confined to TauCeti.integral_haarProb_eq_inv_mul_sum, whose integrand is 𝕜-valued and which uses RCLike.real_smul_eq_coe_mul; the character count then goes through that lemma.

References

Each statement below is the finite case of the compact-group theorem named beside it. haarProb G is the normalized counting measure |G|⁻¹ • count, and the counting identity dim V^G = |G|⁻¹ ∑ g, χ_π g is the finite shadow of ContRepresentation.integral_character_eq_finrank_invariants, matching Mathlib's FDRep.average_char_eq_finrank_invariants for the purely algebraic theory. L²(G) is G → 𝕜 by TauCeti.lpHaarProbEquivFun and ⟪·, ·⟫_{L²(G)} becomes the finite Hermitian pairing on it, schur_orthogonality_self, schur_orthogonality_distinct and schur_orthogonality become the classical orthogonality relations for matrix coefficients, and character_orthonormal_self and character_orthonormal_distinct become the two branches of Mathlib's Representation.char_orthonormal, exhibited by two anonymous examples. Finally exists_orthogonal_irreducible_decomposition specializes, through the finite unitarian trick, to ContRepresentation.exists_orthogonal_irreducible_decomposition_of_finite, whose blocks are subrepresentations of the given representation, carried back along the unitarizing equivalence ContRepresentation.congrEquiv. What that specialization adds to Mathlib's Maschke is the orthogonality of the summands, which needs the inner product Mathlib's complements do not see; the purely algebraic conclusion, that π.toRepresentation.asModule is a semisimple MonoidAlgebra 𝕜 G-module whenever |G| is invertible in 𝕜, is Mathlib's own instance and is neither restated nor reproved here. Peter-Weyl for a finite group, that peterWeylBasis is the matrix-coefficient basis of the functions on G, is proved in TauCeti/RepresentationTheory/Compact/DegreeSum.lean, on top of the identification TauCeti.lpHaarProbEquivFun built below.

theorem TauCeti.eq_smul_count_of_isMulLeftInvariant {G : Type u_1} [Group G] [Finite G] [MeasurableSpace G] [MeasurableSingletonClass G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [MeasureTheory.IsProbabilityMeasure μ] : μ = (↑(Nat.card G))⁻¹ • MeasureTheory.Measure.count

A left-invariant probability measure on a finite group is the normalized counting measure.

Left translation by g carries {1} to {g}, so left invariance forces all singletons to have the same mass c and hence μ = c • Measure.count by MeasureTheory.Measure.ext_of_singleton; evaluating both sides on Set.univ computes c = |G|⁻¹ from the total mass being 1. Neither a topology nor the Haar property of the counting measure is needed.

theorem TauCeti.haarProb_eq_smul_count (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] : haarProb G = (↑(Nat.card G))⁻¹ • MeasureTheory.Measure.count

Normalized Haar measure on a finite discrete group is the normalized counting measure. Because TauCeti.eq_smul_count_of_isMulLeftInvariant needs only left invariance and total mass one, this also says that no other Haar probability measure on G exists.

@[simp]

theorem TauCeti.haarProb_singleton (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (g : G) : (haarProb G) {g} = (↑(Nat.card G))⁻¹

The normalized Haar measure of a singleton in a finite discrete group is |G|⁻¹.

theorem TauCeti.haarProb_apply (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (s : Set G) : (haarProb G) s = ↑s.ncard / ↑(Nat.card G)

The normalized Haar measure of a set in a finite discrete group is the fraction of the group it occupies.

@[simp]

theorem TauCeti.haarProb_real_singleton (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (g : G) : (haarProb G).real {g} = (↑(Nat.card G))⁻¹

The real-valued normalized Haar measure of a singleton, in the form MeasureTheory.integral_fintype consumes.

theorem TauCeti.haarProb_real_apply (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (s : Set G) : (haarProb G).real s = ↑s.ncard / ↑(Nat.card G)

The real-valued normalized Haar measure of a set in a finite discrete group.

theorem TauCeti.haarProb_eq_uniformOn_univ (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] : haarProb G = ProbabilityTheory.uniformOn Set.univ

Normalized Haar measure on a finite discrete group is Mathlib's uniform probability measure ProbabilityTheory.uniformOn Set.univ.

theorem TauCeti.integral_haarProb (G : Type u_1) [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (F : G → V) : ∫ (g : G), F g ∂haarProb G = (↑(Nat.card G))⁻¹ • ∑ g : G, F g

The Haar integral over a finite discrete group is the group average. This is what makes every averaging statement of the compact theory specialize to its finite-group counterpart.

theorem TauCeti.integral_haarProb_eq_inv_mul_sum (G : Type u_1) [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_3} [RCLike 𝕜] (F : G → 𝕜) : ∫ (g : G), F g ∂haarProb G = (↑(Nat.card G))⁻¹ * ∑ g : G, F g

The Haar integral of a 𝕜-valued function over a finite discrete group is the group average, in the 𝕜-scalar form the character theory consumes: TauCeti.integral_haarProb states the same identity with the real scalar (|G| : ℝ)⁻¹ acting on a general normed space.

theorem TauCeti.haarAverage_eq_smul_sum (G : Type u_1) [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] (f : C(G, V)) : (haarAverage G) f = (↑(Nat.card G))⁻¹ • ∑ g : G, f g

The bundled Haar averaging operator of a finite discrete group is the group average.

The L² space of a finite group

@[simp]

theorem TauCeti.ae_haarProb_eq_top (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] : MeasureTheory.ae (haarProb G) = ⊤

Normalized Haar measure on a finite discrete group has full support, in the sharp form that its almost-everywhere filter is the whole filter: every singleton has mass |G|⁻¹ ≠ 0, so the empty set is the only null set.

theorem TauCeti.eq_of_ae_eq_haarProb (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {α : Type u_2} {f g : G → α} (h : f =ᵐ[haarProb G] g) : f = g

Functions on a finite discrete group agreeing almost everywhere for normalized Haar measure agree everywhere. This is TauCeti.ae_haarProb_eq_top read as a statement about functions; nothing is asked of the codomain, the fact being one about the measure alone.

In particular an element of Lp 𝕜 p (haarProb G), which is only an almost-everywhere class, is pinned down by its values: this is the sense in which L²(G) "is" G → 𝕜.

theorem TauCeti.coeFn_toLp_haarProb (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] (f : C(G, 𝕜)) : ↑↑((ContinuousMap.toLp p (haarProb G) 𝕜) f) = ⇑f

The Lp class of a continuous function on a finite discrete group is that function, on the nose and not merely almost everywhere, because normalized Haar measure has full support (TauCeti.eq_of_ae_eq_haarProb).

This is not a simp lemma: ContinuousMap.coe_toLp already rewrites the left-hand side to ⇑(f.toAEEqFun (haarProb G)), so tagging it is a simpNF error. The value-level simp form of the round trip through the equivalence below is TauCeti.coeFn_lpHaarProbEquivFun_symm.

noncomputable def TauCeti.lpHaarProbEquivFun (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (p : ENNReal) : ↥(MeasureTheory.Lp 𝕜 p (haarProb G)) ≃ₗ[𝕜] G → 𝕜

Lp of a finite discrete group is the space of all functions on it: taking underlying functions is a 𝕜-linear equivalence Lp 𝕜 p (haarProb G) ≃ₗ[𝕜] (G → 𝕜).

It is injective because normalized Haar measure has full support (TauCeti.eq_of_ae_eq_haarProb), so an Lp class is pinned down by its values, and surjective because G is finite and the measure is finite: every function on G is then p-integrable, by MeasureTheory.MemLp.of_discrete, and MeasureTheory.MemLp.toLp produces its class. Nothing depends on the exponent, not even 1 ≤ p; at p = 2, together with TauCeti.inner_Lp_haarProb_eq_inv_mul_sum, which computes the inner product from exactly the values this equivalence reads off, it is the identification of L²(G) with G → 𝕜 carrying the normalized Hermitian pairing.

@[simp]

theorem TauCeti.lpHaarProbEquivFun_apply (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {p : ENNReal} (f : ↥(MeasureTheory.Lp 𝕜 p (haarProb G))) (x : G) : (lpHaarProbEquivFun G 𝕜 p) f x = ↑↑f x

The equivalence TauCeti.lpHaarProbEquivFun reads off the values of an Lp class.

@[simp]

theorem TauCeti.coeFn_lpHaarProbEquivFun_symm (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {p : ENNReal} (f : G → 𝕜) : ↑↑((lpHaarProbEquivFun G 𝕜 p).symm f) = f

The inverse of TauCeti.lpHaarProbEquivFun has the values it was handed. This is the simp-normal form of the inverse: it is what makes the round trip through the equivalence reduce.

theorem TauCeti.lpHaarProbEquivFun_symm_apply (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {p : ENNReal} [Fact (1 ≤ p)] (f : G → 𝕜) : (lpHaarProbEquivFun G 𝕜 p).symm f = (ContinuousMap.toLp p (haarProb G) 𝕜) { toFun := f, continuous_toFun := ⋯ }

The inverse of TauCeti.lpHaarProbEquivFun is ContinuousMap.toLp, every function on a discrete space being continuous; this is the identification for the exponents at which that map exists. It is not a simp lemma: TauCeti.coeFn_lpHaarProbEquivFun_symm is the value-level form, and rewriting the inner term first would keep a round trip from reducing by LinearEquiv.apply_symm_apply.

instance TauCeti.finiteDimensional_lp_haarProb (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (p : ENNReal) : FiniteDimensional 𝕜 ↥(MeasureTheory.Lp 𝕜 p (haarProb G))

Lp of a finite discrete group is finite-dimensional. It is the space G → 𝕜 of all functions on G, by TauCeti.lpHaarProbEquivFun.

theorem TauCeti.finrank_lp_haarProb (G : Type u_1) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] (p : ENNReal) : Module.finrank 𝕜 ↥(MeasureTheory.Lp 𝕜 p (haarProb G)) = Nat.card G

Lp of a finite discrete group has dimension the order of the group. No exponent condition is needed: the identification with G → 𝕜 of TauCeti.lpHaarProbEquivFun holds for every p.

theorem TauCeti.inner_Lp_haarProb_eq_inv_mul_sum (G : Type u_1) [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_2} [RCLike 𝕜] (f g : ↥(MeasureTheory.Lp 𝕜 2 (haarProb G))) : inner 𝕜 f g = (↑(Nat.card G))⁻¹ * ∑ x : G, (starRingEnd 𝕜) (↑↑f x) * ↑↑g x

The L² inner product of a finite discrete group is the normalized Hermitian pairing |G|⁻¹ ∑ x, conj (f x) * g x.

This is the pairing carried by the identification L²(G) = (G → 𝕜) of TauCeti.lpHaarProbEquivFun, whose underlying map is the coercion appearing on the right: the Haar integral defining the L² inner product is the group average, by TauCeti.integral_haarProb_eq_inv_mul_sum. The conjugation sits on the first argument, matching Mathlib's convention that the inner product is conjugate-linear there.

theorem TauCeti.inner_toLp_haarProb_eq_inv_mul_sum (G : Type u_1) [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] {𝕜 : Type u_2} [RCLike 𝕜] (f g : C(G, 𝕜)) : inner 𝕜 ((ContinuousMap.toLp 2 (haarProb G) 𝕜) f) ((ContinuousMap.toLp 2 (haarProb G) 𝕜) g) = (↑(Nat.card G))⁻¹ * ∑ x : G, (starRingEnd 𝕜) (f x) * g x

The L² inner product of two continuous functions on a finite discrete group, the form in which the matrix coefficients and the characters present themselves.

theorem ContRepresentation.haarAverageMap_eq_smul_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology 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 = (↑(Nat.card G))⁻¹ • ∑ g : G, (π g) v

The Haar average of the action operators of a finite discrete group is the finite group average |G|⁻¹ ∑ g, π g, the Reynolds operator whose role normalized Haar measure plays in ContRepresentation.haarAverageMap. Mathlib's algebraic counterpart of that operator is Representation.averageMap; this lemma relates the Haar average to the explicit sum only.

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

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

Matrix coefficients and the Schur orthogonality relations

theorem ContRepresentation.inner_matrixCoeffLp_eq_inv_mul_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) (v w : V) (v' w' : W) : inner 𝕜 (π.matrixCoeffLp hπ v w) (ρ.matrixCoeffLp hρ v' w') = (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) (inner 𝕜 ((π g) v) w) * inner 𝕜 ((ρ g) v') w'

The L² pairing of two matrix coefficients of a finite group is a group average. This is the identity along which the Schur orthogonality relations become finite sums.

theorem ContRepresentation.schur_orthogonality_self_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) (v₁ w₁ v₂ w₂ : V) : (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) (inner 𝕜 ((π g) v₁) w₁) * inner 𝕜 ((π g) v₂) w₂ = (↑(Module.finrank 𝕜 V))⁻¹ * ((starRingEnd 𝕜) (inner 𝕜 v₁ v₂) * inner 𝕜 w₁ w₂)

The first Schur orthogonality relation for a finite group. For a unitary irreducible representation of dimension d, |G|⁻¹ ∑ g, conj ⟪π g v₁, w₁⟫ * ⟪π g v₂, w₂⟫ = d⁻¹ * (conj ⟪v₁, v₂⟫ * ⟪w₁, w₂⟫).

This is ContRepresentation.schur_orthogonality_self with the Haar integral of the compact theory replaced by the group average; the normalization |G|⁻¹ is exactly the one that makes normalized Haar measure a probability measure. Neither continuity of π nor a measurable structure on G is asked: the statement mentions no measure and no continuity proof, and the proof installs the Borel structure it integrates against, continuous_of_discreteTopology supplying the continuity.

theorem ContRepresentation.schur_orthogonality_basis_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [IsAlgClosed 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedSpace ℝ V] [SMulCommClass ℝ 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) (hunitary : π.IsUnitary) (hirr : (toRepresentation 𝕜 G V π).IsIrreducible) {d : ℕ} (e : OrthonormalBasis (Fin d) 𝕜 V) (i j k l : Fin d) : (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) (inner 𝕜 ((π g) (e j)) (e i)) * inner 𝕜 ((π g) (e l)) (e k) = (↑d)⁻¹ * ((if j = l then 1 else 0) * if i = k then 1 else 0)

The first Schur orthogonality relation for a finite group, in an orthonormal basis. If πᵢⱼ(g) = ⟪π g eⱼ, eᵢ⟫, then |G|⁻¹ ∑ g, conj (πᵢⱼ g) * πₖₗ g = d⁻¹ δⱼₗ δᵢₖ.

This is ContRepresentation.schur_orthogonality_basis with the Haar integral replaced by the group average, and it is the form the matrix coefficients of a finite group present themselves in: the index order and the placement of the conjugation are the ones fixed there, Kronecker deltas being real.

theorem ContRepresentation.schur_orthogonality_distinct_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (hunitary : ρ.IsUnitary) (hdistinct : ∀ (f : ContIntertwiningMap π ρ), f.toContinuousLinearMap = 0) (v w : V) (v' w' : W) : (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) (inner 𝕜 ((π g) v) w) * inner 𝕜 ((ρ g) v') w' = 0

Schur orthogonality for a finite group and a vanishing intertwiner space. If the only continuous intertwiner π → ρ is zero and ρ is unitary, then every matrix coefficient of π has vanishing group average against every matrix coefficient of ρ. This is ContRepresentation.schur_orthogonality_distinct read through the finite Hermitian pairing; Schur's lemma is what supplies the hypothesis for a pair of inequivalent irreducibles, as in ContRepresentation.schur_orthogonality_sum below. No continuity is asked of either representation, for the reason given at ContRepresentation.schur_orthogonality_self_sum.

theorem ContRepresentation.schur_orthogonality_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [NormedSpace ℝ W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (hunitary : ρ.IsUnitary) (hirrπ : (toRepresentation 𝕜 G V π).IsIrreducible) (hirrρ : (toRepresentation 𝕜 G W ρ).IsIrreducible) (hne : IsEmpty (π.Equiv ρ)) (v w : V) (v' w' : W) : (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) (inner 𝕜 ((π g) v) w) * inner 𝕜 ((ρ g) v') w' = 0

The second Schur orthogonality relation for a finite group. Matrix coefficients of inequivalent irreducible representations, the second of them unitary, have vanishing group average, this being ContRepresentation.schur_orthogonality read through the finite Hermitian pairing. No continuity is asked of either representation, for the reason given at ContRepresentation.schur_orthogonality_self_sum.

Characters

theorem ContRepresentation.inner_characterLp_eq_inv_mul_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (ρ : ContRepresentation 𝕜 G W) (hρ : Continuous ⇑ρ) : inner 𝕜 (π.characterLp hπ) (ρ.characterLp hρ) = (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) ((π.character hπ) g) * (ρ.character hρ) g

The L² pairing of two characters of a finite group is a group average.

theorem ContRepresentation.character_orthonormal_distinct_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] [NormedAddCommGroup W] [InnerProductSpace 𝕜 W] [FiniteDimensional 𝕜 W] (π : ContRepresentation 𝕜 G V) (ρ : ContRepresentation 𝕜 G W) (hunitary : π.IsUnitary) (hdistinct : ∀ (f : ContIntertwiningMap ρ π), f.toContinuousLinearMap = 0) : (↑(Nat.card G))⁻¹ * ∑ g : G, (starRingEnd 𝕜) ((toRepresentation 𝕜 G V π).character g) * (toRepresentation 𝕜 G W ρ).character g = 0

The off-diagonal branch of first (row) character orthogonality for a finite group: for a unitary π, the group average of conj χ_π · χ_ρ vanishes when no nonzero continuous intertwiner ρ → π exists, which for a pair of irreducibles is Schur's lemma. Unitarity is asked of π alone, as in the compact source ContRepresentation.character_orthonormal_distinct. (The second orthogonality relation, the column sum over the irreducible characters, is a different statement and is not proved here.)

The characters are written as Mathlib's Representation.character of the underlying representations, which is by ContRepresentation.coe_character the function underlying character π hπ; so no continuity proof is asked of the caller, and no measurable structure on G either, the statement mentioning neither.

The unitarian trick and Maschke

theorem ContRepresentation.inner_gramOperator_eq_inv_mul_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v w : V) : inner 𝕜 v ((π.gramOperator hπ) w) = (↑(Nat.card G))⁻¹ * ∑ g : G, inner 𝕜 ((π g) v) ((π g) w)

The averaged invariant form of a finite group is the group average ⟪v, w⟫_G = |G|⁻¹ ∑ g, ⟪π g v, π g w⟫. This is the form Weyl's unitarian trick averages into existence, read off the Gram operator that represents it (ContRepresentation.inner_gramOperator) through TauCeti.integral_haarProb_eq_inv_mul_sum; for a finite group it is the classical averaging ⟪·, ·⟫ ↦ |G|⁻¹ ∑ g, ⟪π g ·, π g ·⟫ of the finite-group proof, and the normalization |G|⁻¹ is the one that fixes the form on the invariants.

theorem ContRepresentation.inner_gramOperator_self_eq_inv_mul_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) (v : V) : inner 𝕜 ((π.gramOperator hπ) v) v = ↑((↑(Nat.card G))⁻¹ * ∑ g : G, ‖(π g) v‖ ^ 2)

The averaged form of a finite group on the diagonal is the average of ‖π g v‖ ^ 2. This is the finite form of the positive definiteness that makes the unitarian trick work: the average of |G| nonnegative reals, one of which is ‖v‖ ^ 2 at g = 1, is positive for v ≠ 0. Compactness of G enters the general statement ContRepresentation.inner_gramOperator_self only to make g ↦ ‖π g v‖ ^ 2 integrable; it is the strict positivity ContRepresentation.re_inner_gramOperator_self_pos that also needs the compactness bound on the operator norms from below. A finite group needs neither.

theorem ContRepresentation.gramOperator_eq_smul_sum {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Fintype G] [TopologicalSpace G] [DiscreteTopology G] [MeasurableSpace G] [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] (π : ContRepresentation 𝕜 G V) (hπ : Continuous ⇑π) : π.gramOperator hπ = (↑(Nat.card G))⁻¹ • ∑ g : G, ContinuousLinearMap.adjoint (π g) ∘SL π g

The Gram operator of a finite group is the averaged sum of the operators (π g)† ∘ (π g). This is ContRepresentation.inner_gramOperator_eq_inv_mul_sum at the level of operators: each summand is the Gram operator of the pulled-back form (v, w) ↦ ⟪π g v, π g w⟫, and the Haar average of the family is their group average.

theorem ContRepresentation.exists_isUnitary_congr_of_finite {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Finite G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) : ∃ (e : V ≃L[𝕜] V), (e.congr π).IsUnitary

The unitarian trick for a finite group. Every finite-dimensional representation of a finite group on an inner product space is conjugate, by a continuous linear automorphism of the carrier, to one preserving the inner product.

This is ContRepresentation.exists_isUnitary_congr with all of its compact-group hypotheses discharged: the statement mentions no topology on G, so the proof installs the discrete topology — a finite discrete group is compact and every representation of it is continuous by continuous_of_discreteTopology — and the caller is left with a bare finite group. The form being averaged is the explicit |G|⁻¹ ∑ g, ⟪π g ·, π g ·⟫ of ContRepresentation.inner_gramOperator_eq_inv_mul_sum.

theorem ContRepresentation.exists_orthogonal_irreducible_decomposition_of_finite {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Finite G] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V] (π : ContRepresentation 𝕜 G V) : ∃ (e : V ≃L[𝕜] V) (n : ℕ) (U : Fin n → Subrepresentation (toRepresentation 𝕜 G V π)), (e.congr π).IsUnitary ∧ (∀ (i : Fin n), (U i).toRepresentation.IsIrreducible) ∧ (Pairwise fun (i j : Fin n) => ∀ v ∈ (U i).toSubmodule, ∀ w ∈ (U j).toSubmodule, inner 𝕜 (e v) (e w) = 0) ∧ (DirectSum.IsInternal fun (i : Fin n) => (U i).toSubmodule) ∧ Module.finrank 𝕜 V = ∑ i : Fin n, Module.finrank 𝕜 ↥(U i).toSubmodule

Maschke's theorem in orthogonal form. A finite-dimensional representation π of a finite group on an inner product space is an internal direct sum of finitely many irreducible subrepresentations, of dimensions adding up to dim V, which are moreover pairwise orthogonal for an invariant inner product ⟪e ·, e ·⟫ obtained from the given one by a continuous linear automorphism e of the carrier.

This is the finite shadow of complete reducibility, and all that is finite about it is the production of e: unitarity is not assumed but produced, by the finite unitarian trick ContRepresentation.exists_isUnitary_congr_of_finite, and the decomposition of π itself is then ContRepresentation.IsUnitary.exists_orthogonal_irreducible_decomposition_of_congr, which decomposes the unitary model and carries every block back along the equivalence of representations ContRepresentation.congrEquiv : π.Equiv (congr e π) for an arbitrary group. The blocks are therefore subrepresentations of π itself.

Distorting the inner product by e is unavoidable and is what "Maschke" costs here: Lean fixes one inner product on V, and a representation of a finite group need not preserve it, only the average |G|⁻¹ ∑ g, ⟪π g ·, π g ·⟫ of its translates. So the blocks need not be orthogonal for ⟪·, ·⟫, and orthogonality is stated for the invariant form ⟪e ·, e ·⟫ that the unitarian trick produces — equivalently, their images under e are the orthogonal family decomposing the unitary model congr e π. It is that orthogonality which the compact theory contributes over Mathlib's Maschke, which produces complements but no inner product; the plain semisimplicity is not restated here, being already a Mathlib instance for every field in which |G| is invertible.