OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborLawCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Compact containment gives a convergent subsequence of the original translated Haar laws and a supported pair. The law is built from the actual map q ↦ (profile q, profile (q * step)).

   theorem exists_supported_neighbor_law
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (chartN : GroupLieAlgebra (𝓘(ℝ, F.N.modelSpace)) F.N.carrier ≃ₜ F.N.carrier)
       (hchartN : ∀ v, chartN v = F.ExpN v)
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (E : Set W) (β : M.Bases) (scale : ℕ → ℝ) (base step : ℕ → F.N.carrier)
       (S : Set C((Fin (finrank ℝ H) → ℝ), W)) (hS : IsCompact S)
       [MeasurableSpace S] [BorelSpace S]
       (profile : ℕ → F.N.carrier → S) :
       ∃ (ν : ProbabilityMeasure (S × S)) (f : S × S) (u : ℕ → ℕ),
         StrictMono u ∧ f ∈ (ν : Measure (S × S)).support ∧
         Tendsto (fun n => ProbabilityMeasure.map
   …

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