FiniteCase.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite comparison case

The lower quasi-isometry inequality and finiteness of word-metric balls imply that a group quasi-isometric to a finite group is finite. This treats the zero-dimensional lattice case directly. No recognition theorem is assumed.

theorem OAI.PolycyclicRecognition.finite_of_coarseEmbedding_finite line 21
Source documentation
A coarsely embedded space with finite metric balls is finite when the target is finite. The displayed inequality is the lower quasi-isometry inequality, rearranged to avoid division by its multiplicative constant.
```
theorem finite_of_coarseEmbedding_finite [Finite P]
    (hballs : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    (f : H → P) (K C : ℝ) (hK : 0 ≤ K)
    (hlower : ∀ h k, dist h k ≤ K * dist (f h) (f k) + C) : Finite H := by
…
```

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_coarseEmbedding_finite line 36

Source documentation

The finite-target special case of virtual-polycyclic recognition.

theorem virtuallyPolycyclic_of_coarseEmbedding_finite [Finite P]
    (hballs : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    (f : H → P) (K C : ℝ) (hK : 0 ≤ K)
    (hlower : ∀ h k, dist h k ≤ K * dist (f h) (f k) + C) :
    IsVirtuallyPolycyclic H := by
…