OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryInverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.boundary_left_inverse_of_actual_compact_shadows line 42

   Source documentation

   Coarse inverse maps and the actual compact shadows force the boundary composition to be the identity. No inverse property of the boundary maps is assumed.

   theorem boundary_left_inverse_of_actual_compact_shadows
       (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)
       {R : Type*} [One R] [TopologicalSpace R] (actR : G →* Equiv.Perm R)
       (B : Q.carrier → R) (C : R → Q.carrier) (f g : G → G)
       {Lg error E : ℝ} (hLg : 0 ≤ Lg)
       (hg : ∀ x y, dist (g x) (g y) ≤ Lg * dist x y + error)
       (hinv : ∀ x, dist (g (f x)) x ≤ E)
       (σ : Q.carrier → G) (hσ : Continuous σ) (hsection : ∀ q, act (σ q) 1 = q)
       (σR : R → G) (hσR : Continuous σR) (hsectionR : ∀ q, actR (σR q) 1 = q)
   …