OAI/GroupTheory/PolycyclicRecognition/Geometry/BoundaryCompactSandwich.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.compact_boundary_image_upper line 20

   Source documentation

   A compact set in the source boundary has one common compact image shadow under a family with common coarse Lipschitz and shadow bounds.

   theorem compact_boundary_image_upper
       {P G S T : Type*} [Group G] [MetricSpace G] [IsTopologicalGroup G]
       [IsIsometricSMul G G] [ProperSpace G]
       [One S] [TopologicalSpace S] [One T]
       (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
       (B : P → S → T) (f : P → G → G)
       {L error : ℝ} (hL : 0 ≤ L)
       (hf : ∀ p x y, dist (f p x) (f p y) ≤ L * dist x y + error)
       (σ : S → G) (hσ : Continuous σ) (hsection : ∀ q, actS (σ q) 1 = q)
       (KT : Set G) (hKT : IsCompact KT)
       (hB : ∀ p x, ∃ v ∈ KT, B p (actS x 1) = actT (f p x) (actT v 1))
       (U : Set S) (hU : IsCompact U) :
   …

2. theorem OAI.PolycyclicRecognition.boundary_image_compact_sandwich line 65

   Source documentation

   Both compact inclusions needed for volume comparison follow from coarse inverses and the already constructed boundary shadows.

   theorem boundary_image_compact_sandwich
       {P G S T : Type*} [Group G] [MetricSpace G] [IsTopologicalGroup G]
       [IsIsometricSMul G G] [ProperSpace G]
       [One S] [TopologicalSpace S] [One T] [TopologicalSpace T]
       (actS : G →* Equiv.Perm S) (actT : G →* Equiv.Perm T)
       (hcontS : Continuous (fun g => actS g 1))
       (hcontT : Continuous (fun g => actT g 1))
       (B : P → S → T) (C : P → T → S) (f g : P → G → G)
       {Lf Lg ef eg E : ℝ} (hLf : 0 ≤ Lf) (hLg : 0 ≤ Lg)
       (hf : ∀ p x y, dist (f p x) (f p y) ≤ Lf * dist x y + ef)
       (hg : ∀ p x y, dist (g p x) (g p y) ≤ Lg * dist x y + eg)
       (hinv : ∀ p x, dist (g p (f p x)) x ≤ E)
   …