OAI/GroupTheory/PolycyclicRecognition/Geometry/CanonicalExponentialMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exponential_basis_measure_isHaar line 23

   Source documentation

   The published input gives Haar invariance to this specific coordinate measure, so recurrence and the determinant formula use the same normalization.

   theorem exponential_basis_measure_isHaar
       (haar : NilpotentExponentialHaarInput E G)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (hnil : LieRing.IsNilpotent L)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       {n : ℕ} (b : Basis (Fin n) ℝ L) :
       (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume).IsHaarMeasure := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

2. theorem OAI.PolycyclicRecognition.exponential_basis_measure_isRightInvariant line 40

   Source documentation

   Inversion corresponds to coordinate negation. Thus the same measure is also right invariant, as required by backward recurrence.

   theorem exponential_basis_measure_isRightInvariant
       (haar : NilpotentExponentialHaarInput E G)
       (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
       (hnil : LieRing.IsNilpotent L)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
       {n : ℕ} (b : Basis (Fin n) ℝ L) :
       (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume).IsMulRightInvariant := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput