OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarseRayQuotientLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Common compact limits for centered coarse rays

  1. theorem OAI.PolycyclicRecognition.centered_coarse_ray_quotient_limits line 17

    Source documentation

    The actual factor bounds and compact-set contraction give a common compact limit set for every ray in a centered coarse family.

    theorem centered_coarse_ray_quotient_limits
    {P S N D G E Q J : Type*} [MetricSpace S] [One S]
    [Group N] [Group D] [Group G] [MetricSpace G] [IsIsometricSMul G G]
    [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [TopologicalSpace Q] [ChartedSpace E Q] [Group Q]
    [LieGroup (𝓘(ℝ, E)) ⊀ Q] [T2Space 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)
    (dynkin : NilpotentDynkinExpansionInput E Q)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) Q ≃ₜ Q) (hchart : ∀ v, chart v = Exp v)



    Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput