OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorTrajectoryIncrements.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.factor_trajectory_summable_log_increments line 16

   Source documentation

   Uniform negative heights and polynomial Cartan coordinates give the actual logarithmic increments needed by the boundary-limit theorem.

   theorem factor_trajectory_summable_log_increments
       {P N D G E Q J : Type*} [Group N] [Group D] [Group G]
       [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
       [TopologicalSpace Q] [ChartedSpace E Q] [Group Q]
       [LieGroup (𝓘(ℝ, E)) ⊤ Q] [Fintype J]
       (ι : 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)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)
       (b : Basis J ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q))
       (size height : D → ℝ) (K : Set Q)
   …