OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeSourceCellVolumes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.cone_source_cell_volumes line 32

   Source documentation

   In the actual kernel Haar measure, the source box has one fixed positive coefficient and the exact sum-of-word-widths exponent. The quotient factor is fixed and has finite positive measure.

   theorem cone_source_cell_volumes
       (eI : M.coneWordIdeal C ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EI)) I)
       (ExpI : GroupLieAlgebra (𝓘(ℝ, EI)) I → I) (hExpI : IsGroupExponential ExpI)
       (haarI : NilpotentExponentialHaarInput EI I)
       (chartI : GroupLieAlgebra (𝓘(ℝ, EI)) I ≃ₜ I) (hchartI : ∀ v, chartI v = ExpI v)
       (π : N →* Q) (ι : I →* N) (hι : Topology.IsClosedEmbedding ι)
       (hrange : range ι = (π.ker : Set N))
       (μI : Measure I) [μI.IsHaarMeasure]
       (μQ : Measure Q) [μQ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μQ]
       {d : ℕ} (eQ : (Fin d → ℝ) ≃ₜ Q)
       (s : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C) (scale : ℕ → ℝ) :
       let ZQ := eQ '' closedBall (0 : Fin d → ℝ) 1
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput