CartanRayCompactCollapse.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Compact ambient shadows collapse under the actual negative ray

theorem OAI.PolycyclicRecognition.CartanWordModel.ambient_ray_fixes_one_and_contracts_compact_orbits line 43

Source documentation

The actual ambient ray fixes the quotient basepoint and contracts projected points from every fixed compact ambient set, uniformly for arbitrary choices of those points.

theorem ambient_ray_fixes_one_and_contracts_compact_orbits
    (hExpQ : IsGroupExponential ExpQ) (hπcont : Continuous π)
    (act : G →* Equiv.Perm Q.carrier)
    (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = π u * α d q)
    (v : H) (hv : α₀ v < 0) :
    let ray := fun n : ℕ => ExpG (((n : ℝ) • v : H) : GroupLieAlgebra (𝓘(ℝ, EG)) G)
…