OAI/GroupTheory/PolycyclicRecognition/Analysis/ConeIdealMeasuredTiling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdeal_measured_tiling line 29

   Source documentation

   A single Haar normalization supplies both the ambient-inner invariance and the exact tiling exponent. The radius is independent of the widths, scale, maximizing basis and automorphism.

   theorem exists_coneIdeal_measured_tiling
       (haar : NilpotentExponentialHaarInput E G)
       (dynkin : NilpotentDynkinExpansionInput E G)
       (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C)) :
       ∃ (μ : Measure G) (hbij : Function.Bijective Exp) (R : ℝ),
         μ.IsHaarMeasure ∧ 0 < R ∧
         (∀ x : cartanRootIdeal H,
           MeasurePreserving (exponentialConjugate e Exp hbij (M.coneIdealInnerAutomorphism C x)) μ μ) ∧
         ∀ (s₁ s₂ : Fin M.letterCount → ℝ) (β : M.ConeIdealBases C),
           M.IsMaximizingConeIdealBasis C b₀ s₁ β →
           M.IsMaximizingConeIdealBasis C b₀ s₂ β → ∀ r : ℝ, 0 ≤ r →
           ∀ F : G ≃ₜ* G, MeasurePreserving F μ μ →
   …

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