OAI/GroupTheory/PolycyclicRecognition/Analysis/ContinuousCoarseRayLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous limits for coarse families with bounded initial points

  1. theorem OAI.PolycyclicRecognition.continuous_bounded_coarse_ray_quotient_limits line 17

    Source documentation

    The common logarithmic increment estimate gives a continuous limit for each continuous coarse family whose initial points are uniformly bounded.

    theorem continuous_bounded_coarse_ray_quotient_limits
    {P S N D G E Q J : Type*} [TopologicalSpace P] [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