OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCellProbability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.translated_groupBox_cell_properties line 30

   Source documentation

   Every translated unit Cartan box is Borel and has positive finite measure for the same canonical Haar normalization used by recurrence.

   theorem translated_groupBox_cell_properties
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ x, chartN x = F.ExpN x)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases) (r : ℝ) (k : F.N.carrier) :
       let μ := Measure.map ((F.ExpN ∘ F.N.equiv) ∘ b₀.equivFun.symm) volume
   …

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

2. def OAI.PolycyclicRecognition.CartanWordModel.translatedGroupBoxProbability line 58

   Source documentation

   The normalized restriction to the actual translated unit box.

   def translatedGroupBoxProbability
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ x, chartN x = F.ExpN x)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases) (r : ℝ) (k : F.N.carrier) : ProbabilityMeasure F.N.carrier :=
   …

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