OAI/GroupTheory/PolycyclicRecognition/Analysis/FactorQuotientChainDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.factor_quotient_chain_difference_tendsto_one line 22

   Source documentation

   The nilpotent parts of the point lifts cancel. Polynomial bounds on the Cartan parts and negative height turn the compact increment estimate into a vanishing ordered quotient product.

   theorem factor_quotient_chain_difference_tendsto_one
       (ι : N →* G) (κ : D →* G) (π : N →* Q)
       (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
       (hact : ∀ n d q, act (ι n * κ d) q = π n * α d q)
       (dynkin : NilpotentDynkinExpansionInput E Q)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)
       {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q)
         (GroupLieAlgebra (𝓘(ℝ, E)) Q) c = ⊥)
       (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q))
       (size height : D → ℝ) (K : Set Q)
       {A rate : ℝ} (hA : 0 ≤ A) (hrate : 0 < rate) (p : ℕ)
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput