BoundaryShadowDescent.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Descending centered ray limits to boundary maps with compact shadows

theorem OAI.PolycyclicRecognition.boundary_shadow_of_centered_limits line 16

Source documentation

Continuous fixed-element actions transport normalized ray limits. Asymptotic equality on the actual source fibers then gives a well-defined boundary map and the same common compact shadow.

theorem boundary_shadow_of_centered_limits
    {G S Q : Type*} [Group G] [Group Q] [TopologicalSpace Q]
    [T2Space Q] [IsTopologicalGroup Q]
    (act : G →* Equiv.Perm Q) (hact : ∀ g, Continuous (act g))
    (q : G → S) (hq : Function.Surjective q) (F : G → G) (ray : ℕ → G)
    (K : Set Q) (k : G → Q) (hkK : ∀ x, k x ∈ K)
    (hk : ∀ x, Tendsto (fun n => act ((F x)⁻¹ * F (x * ray n)) 1)
      atTop (𝓝 (k x)))
    (hfiber : ∀ x y, q x = q y →
      Tendsto (fun n => (act (F (x * ray n)) 1)⁻¹ * act (F (y * ray n)) 1)
        atTop (𝓝 (1 : Q))) :
    ∃ B : S → Q, ∀ x,
…