OAI/GroupTheory/PolycyclicRecognition/Analysis/NilpotentHaarSymmetry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.nilpotent_haar_isInvInvariant line 20

   Source documentation

   Negation in exponential coordinates and uniqueness of Haar measure prove inversion invariance for every Haar normalization.

   theorem nilpotent_haar_isInvInvariant
       (haar : NilpotentExponentialHaarInput E G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
       (μ : Measure G) [μ.IsHaarMeasure] : μ.IsInvInvariant := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

2. theorem OAI.PolycyclicRecognition.nilpotent_haar_isMulRightInvariant line 53

   Source documentation

   Inversion changes left Haar invariance into right invariance.

   theorem nilpotent_haar_isMulRightInvariant
       (haar : NilpotentExponentialHaarInput E G)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
       (μ : Measure G) [μ.IsHaarMeasure] : μ.IsMulRightInvariant := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput