OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPolarSourceBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.source_count_volume_bounds line 41

   Source documentation

   The actual source cell volume and counted partition use precisely the source-minus-target exponent required by the offset comparison.

   theorem PolarTiledSamplerData.source_count_volume_bounds
       (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)
       (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal C))
       (πQ : F.N.carrier →* Q.carrier) (ι : I →* F.N.carrier)
       (hι : Topology.IsClosedEmbedding ι) (hrange : range ι = (πQ.ker : Set F.N.carrier))
       (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       {ε : ℝ} (hε : 0 < ε) (β : M.ConeIdealBases C)
       (hβ : M.IsMaximizingConeIdealBasis C bI (M.polarProbeWidths T hunimod eW K) β)
   …

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