Averaging over compact groups

This file bundles integration against normalized Haar measure as a continuous linear map on continuous vector-valued functions. It records the norm bound, constants, and invariance under left and right translation needed for averaging representations.

The implementation reuses Mathlib's Bochner integral, its commutation with continuous linear maps, and the generic left-, right-, and inversion-invariance lemmas for integrals on groups.

The construction is the averaging operator from Layer 0 of the compact-groups roadmap.

theorem TauCeti.integrable_continuousMap (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] (f : C(G, V)) : MeasureTheory.Integrable (⇑f) (haarProb G)

A continuous vector-valued function on a compact group is Bochner integrable against normalized Haar measure: it is continuous on the compact set univ, which carries finite measure.

noncomputable def TauCeti.haarAverage (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] : C(G, V) →L[𝕜] V

Averaging a continuous vector-valued function against normalized Haar measure, as a continuous linear map.

V is not assumed complete, so this is the Bochner integral's junk value 0 unless it is: the definition and its linear structure need no completeness, and the lemmas below that talk about the average's actual value (haarAverage_const, norm_haarAverage_eq_one, and everything reached through haarAverage_comp_comm) ask for [CompleteSpace V] precisely because they do.

Equations

• TauCeti.haarAverage G = { toFun := fun (f : C(G, V)) => ∫ (g : G), f g ∂TauCeti.haarProb G, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem TauCeti.haarAverage_apply (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] (f : C(G, V)) : (haarAverage G) f = ∫ (g : G), f g ∂haarProb G

The Haar average is the Bochner integral against normalized Haar measure.

Not a simp lemma: haarAverage is the normal form here, so that the constant, translation and inversion lemmas below can be simp lemmas. Unfold explicitly with rw/simp when the underlying integral is wanted.

theorem TauCeti.norm_haarAverage_le_one (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] : ‖haarAverage G‖ ≤ 1

The operator norm of Haar averaging is at most one.

theorem TauCeti.norm_haarAverage_apply_le (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] (f : C(G, V)) : ‖(haarAverage G) f‖ ≤ ‖f‖

Haar averaging is norm-nonincreasing for the uniform norm on continuous maps.

@[simp]

theorem TauCeti.haarAverage_const (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] [CompleteSpace V] (v : V) : (haarAverage G) (ContinuousMap.const G v) = v

The Haar average of a constant function is that constant.

theorem TauCeti.norm_haarAverage_eq_one (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] [Nontrivial V] [CompleteSpace V] : ‖haarAverage G‖ = 1

On a nonzero target, Haar averaging has operator norm one.

@[simp]

theorem TauCeti.haarAverage_comp_mulLeft (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] (f : C(G, V)) (g : G) : (haarAverage G) (f.comp (ContinuousMap.mulLeft g)) = (haarAverage G) f

Haar averaging is unchanged by left translation of the argument.

@[simp]

theorem TauCeti.haarAverage_comp_mulRight (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] (f : C(G, V)) (g : G) : (haarAverage G) (f.comp (ContinuousMap.mulRight g)) = (haarAverage G) f

Haar averaging is unchanged by right translation of the argument.

@[simp]

theorem TauCeti.haarAverage_comp_inv (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] (f : C(G, V)) : (haarAverage G) (f.comp ↑(Homeomorph.inv G)) = (haarAverage G) f

Haar averaging is unchanged by inversion of the argument.

@[simp]

theorem ContinuousLinearMap.haarAverage_comp_comm (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G] [BorelSpace G] {V : Type u_2} [NormedAddCommGroup V] {𝕜 : Type u_3} [RCLike 𝕜] [NormedSpace ℝ V] [NormedSpace 𝕜 V] [SMulCommClass ℝ 𝕜 V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] [NormedSpace 𝕜 W] [SMulCommClass ℝ 𝕜 W] [CompleteSpace V] [CompleteSpace W] (L : V →L[𝕜] W) (f : C(G, V)) : (TauCeti.haarAverage G) ((↑L).comp f) = L ((TauCeti.haarAverage G) f)

Continuous linear maps commute with Haar averaging.

The scalars are assumed to be RCLike because Mathlib states ContinuousLinearMap.integral_comp_comm under that hypothesis.