ProperCocompactMetric.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Metric comparison through a proper cocompact homomorphism

Properness bounds preimages of target balls. A coarse section and explicit linear metric chains then give the lower quasi-isometry inequality. Together with the continuous-homomorphism upper bound this is the metric part of the Milnor--Švarc comparison, proved here without a recognition hypothesis.

theorem OAI.PolycyclicRecognition.properHom_bounded_preimage_steps line 26
Source documentation
A proper homomorphism has uniformly bounded preimages of bounded group differences. Compactness of the kernel is included in this argument.
```
theorem properHom_bounded_preimage_steps [ProperSpace H]
    (f : G →* H) (hproper : IsProperMap f) (R : ℝ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ x y, dist (f x) (f y) ≤ R → dist x y ≤ D := by
…
```

theorem OAI.PolycyclicRecognition.compact_image_cover_coarsely_surjective line 43

Source documentation

Cocompactness, expressed as a compact cover of right image cosets, gives the metric coarse-surjectivity radius.

theorem compact_image_cover_coarsely_surjective (f : G →* H)
    (K : Set H) (hK : IsCompact K)
    (hcover : ∀ h : H, ∃ (g : G) (k : H), k ∈ K ∧ f g * k = h) :
    ∃ E : ℝ, 0 ≤ E ∧ ∀ h : H, ∃ g : G, dist h (f g) ≤ E := by
…

theorem OAI.PolycyclicRecognition.properHom_coarse_lower line 58

Source documentation

The lower quasi-isometry inequality is a consequence of properness, coarse surjectivity, and target chains. No injectivity is required.

theorem properHom_coarse_lower [ProperSpace H] (C : LinearMetricChains H)
    (f : G →* H) (hproper : IsProperMap f) {E : ℝ}
    (hsurj : ∀ h, ∃ g, dist h (f g) ≤ E) :
    ∃ A B : ℝ, 0 ≤ A ∧ 0 ≤ B ∧
      ∀ x y, dist x y ≤ A * dist (f x) (f y) + B := by
…

theorem OAI.PolycyclicRecognition.proper_cocompact_hom_quasiIsometry line 89

Source documentation

A continuous proper homomorphism with compact image-coset cover is a metric quasi-isometry when both metrics have the stated linear chains.

theorem proper_cocompact_hom_quasiIsometry [ProperSpace G] [ProperSpace H]
    (CG : LinearMetricChains G) (CH : LinearMetricChains H)
    (f : G →* H) (hf : Continuous f) (hproper : IsProperMap f)
    (K : Set H) (hK : IsCompact K)
    (hcover : ∀ h : H, ∃ (g : G) (k : H), k ∈ K ∧ f g * k = h) :
    ∃ A B A' B' E : ℝ, 0 ≤ A ∧ 0 ≤ B ∧ 0 ≤ A' ∧ 0 ≤ B' ∧ 0 ≤ E ∧
      (∀ x y, dist (f x) (f y) ≤ A * dist x y + B) ∧
      (∀ x y, dist x y ≤ A' * dist (f x) (f y) + B') ∧
      (∀ h, ∃ g, dist h (f g) ≤ E) := by
…