OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorQuotientIncrementBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.factor_quotient_increment_polynomial_exp_bound line 14

   Source documentation

   Polynomial Cartan coordinates and negative linear height turn the compact-set contraction into the summable bound used for ray trajectories.

   theorem factor_quotient_increment_polynomial_exp_bound
       {N D G Q V : Type*} [Group N] [Group D] [Group G] [Group Q]
       [SeminormedAddCommGroup V]
       (ι : N →* G) (κ : D →* G) (π : N →* Q)
       (α : D →* MulAut Q) (act : G →* Equiv.Perm Q)
       (hact : ∀ u d q, act (ι u * κ d) q = π u * α d q)
       (log : Q → V) (size height : D → ℝ) (K : Set Q)
       {A rate B gap : ℝ} (hA : 0 ≤ A) (hrate : 0 < rate) (hB : 0 ≤ B) (hgap : 0 < gap)
       (p degree : ℕ)
       (hcontract : ∀ d, height d ≤ 0 → ∀ q ∈ K,
         ‖log (α d q)‖ ≤ A * (1 + size d) ^ p * Real.exp (rate * height d))
       (n : ℕ) (x y : G) (u : N) (d : D) (hlift : ι u * κ d = x)
   …