OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeKernelHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_kernel_invariant_haar line 37

   Source documentation

   The existing published exponential Haar input supplies an intrinsic measure whose image on the actual kernel is Haar and invariant under every ambient nilpotent conjugation.

   theorem exists_cone_kernel_invariant_haar
       (e : M.coneWordIdeal C ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) I)
       (ExpI : GroupLieAlgebra (𝓘(ℝ, E)) I → I) (hExpI : IsGroupExponential ExpI)
       (haar : NilpotentExponentialHaarInput E I)
       (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (π : N →* Q) (ι : I →* N) (hι : Topology.IsClosedEmbedding ι)
       (hrange : Set.range ι = (π.ker : Set N))
       (ExpN : cartanRootIdeal H → N) (hsurj : Function.Surjective ExpN)
       (hcompat : ∀ v : M.coneWordIdeal C, ι (ExpI (e v)) = ExpN v)
       (j : cartanRootIdeal H →ₗ⁅ℝ⁆ A) (ρ : N →* Aˣ) (hρ : Function.Injective ρ)
       (hmatch : ∀ x, ρ (ExpN x) = algebraExpUnit (j x)) :
       ∃ μ : Measure I, μ.IsHaarMeasure ∧
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit