OAI/GroupTheory/PolycyclicRecognition/Analysis/OrbitFiberAsymptotics.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.relative_limit_trans line 18

   Source documentation

   Asymptotic equality in a topological group is transitive.

   theorem relative_limit_trans {f g h : ℕ → Q}
       (hfg : Tendsto (fun n => (f n)⁻¹ * g n) atTop (𝓝 1))
       (hgh : Tendsto (fun n => (g n)⁻¹ * h n) atTop (𝓝 1)) :
       Tendsto (fun n => (f n)⁻¹ * h n) atTop (𝓝 1) := by
   …

2. theorem OAI.PolycyclicRecognition.orbit_fiber_asymptotic_of_stabilizer line 28

   Source documentation

   The two actual stabilizer invariances imply asymptotic equality on every fiber of the orbit map. No boundary limit is assumed.

   theorem orbit_fiber_asymptotic_of_stabilizer
       {G S Q I D : Type*} [Group G] [One S]
       [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
       (act : G →* Equiv.Perm S) (ι : I → G) (κ : D → G)
       (hstab : ∀ g, act g 1 = 1 ↔ ∃ i d, ι i * κ d = g)
       (f : G → ℕ → Q)
       (hI : ∀ g i, Tendsto (fun n => (f g n)⁻¹ * f (g * ι i) n) atTop (𝓝 1))
       (hD : ∀ g d, Tendsto (fun n => (f g n)⁻¹ * f (g * κ d) n) atTop (𝓝 1)) :
       ∀ g g', act g 1 = act g' 1 →
         Tendsto (fun n => (f g n)⁻¹ * f g' n) atTop (𝓝 1) := by
   …