Haar averaging of real bilinear forms

A continuous representation of a compact group averages each given continuous real bilinear form by pulling both arguments back through the inverse action and integrating against normalized Haar measure. The average is a continuous bilinear form, and the operation is continuous and linear in the starting form. It preserves symmetry and strict positive definiteness on arbitrary real normed spaces, without requiring the representation space to be complete or finite-dimensional.

Main definitions

• ContRepresentation.averageBilinearForm: Haar averaging as an operator on continuous forms.

Main results

• ContRepresentation.averageBilinearForm_apply: the inverse-action integral formula.
• ContRepresentation.isInvariantForm_averageBilinearForm: the averaged form is invariant.
• ContRepresentation.isSymm_averageBilinearForm and ContRepresentation.posDef_averageBilinearForm: symmetry and positivity are preserved.
• ContRepresentation.averageBilinearForm_eq_self and averageBilinearForm_eq_self_iff: averaging fixes exactly invariant forms.
• ContRepresentation.averageBilinearForm_idempotent: averaging is a projection.
• ContRepresentation.averageBilinearForm_bilinearComp: pulling back the input by an action operator does not change its average.

References

• J. Hilgert and K.-H. Neeb, Structure and Geometry of Lie Groups, Springer Monographs in Mathematics (2012), Lemma 10.4.14, for the invariant-inner-product construction.

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

Average a given real continuous bilinear form against normalized Haar measure, using inverse-action pullback. This is a continuous linear operator on the space of forms.

theorem ContRepresentation.averageBilinearForm_apply {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) (v w : V) : (((π.averageBilinearForm hπ) B) v) w = ∫ (g : G), (B ((π g⁻¹) v)) ((π g⁻¹) w) ∂TauCeti.haarProb G

The averaged form is the integral of the inverse-action pullbacks of the starting form.

theorem ContRepresentation.isInvariantForm_averageBilinearForm {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) : TauCeti.Representation.IsInvariantForm (toRepresentation ℝ G V π) ((π.averageBilinearForm hπ) B).toBilinForm

The Haar-averaged form is invariant under the original representation.

theorem ContRepresentation.isSymm_averageBilinearForm {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : B.toBilinForm.IsSymm) : ((π.averageBilinearForm hπ) B).toBilinForm.IsSymm

Averaging preserves symmetry of a continuous real bilinear form.

theorem ContRepresentation.posDef_averageBilinearForm {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : (LinearMap.BilinMap.toQuadraticMap B.toBilinForm).PosDef) : (LinearMap.BilinMap.toQuadraticMap ((π.averageBilinearForm hπ) B).toBilinForm).PosDef

Averaging preserves positive definiteness, without requiring symmetry of the input.

@[simp]

theorem ContRepresentation.averageBilinearForm_eq_self {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : TauCeti.Representation.IsInvariantForm (toRepresentation ℝ G V π) B.toBilinForm) : (π.averageBilinearForm hπ) B = B

Averaging fixes every invariant continuous bilinear form.

theorem ContRepresentation.averageBilinearForm_eq_self_iff {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) : (π.averageBilinearForm hπ) B = B ↔ TauCeti.Representation.IsInvariantForm (toRepresentation ℝ G V π) B.toBilinForm

A continuous bilinear form is fixed by averaging exactly when it is invariant.

@[simp]

theorem ContRepresentation.averageBilinearForm_idempotent {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) : (π.averageBilinearForm hπ) ((π.averageBilinearForm hπ) B) = (π.averageBilinearForm hπ) B

Haar averaging is idempotent on continuous real bilinear forms.

@[simp]

theorem ContRepresentation.averageBilinearForm_bilinearComp {G : Type u_1} {V : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [NormedAddCommGroup V] [NormedSpace ℝ V] (π : ContRepresentation ℝ G V) (hπ : Continuous ⇑π) [CompactSpace G] [MeasurableSpace G] [BorelSpace G] (B : V →L[ℝ] V →L[ℝ] ℝ) (h : G) : (π.averageBilinearForm hπ) (B.bilinearComp (π h) (π h)) = (π.averageBilinearForm hπ) B

Averaging is unchanged if the starting form is pulled back by an action operator.