MetricCoarseBridge.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Metric quasi-isometries and the discrete group coarse structure

The finiteness and duality endgame uses finite sets of group differences. Here an actual metric quasi-isometry supplies that data. The metrics are left invariant and their bounded identity balls are finite, as for word metrics on finitely generated groups. No recognition theorem is assumed.

theorem OAI.PolycyclicRecognition.dist_one_groupDifference line 28
Source documentation
Left invariance measures a group difference by the distance between its two endpoints.
```
theorem dist_one_groupDifference (x y : G) : dist 1 (x⁻¹ * y) = dist x y := by
…
```
theorem OAI.PolycyclicRecognition.groupBornologous_of_metric_bound line 33
Source documentation
An upper coarse Lipschitz inequality sends each finite set of group differences into a finite identity ball.
```
theorem groupBornologous_of_metric_bound (f : G → H)
    (hfinite : ∀ R : ℝ, (closedBall (1 : H) R).Finite)
    {K C : ℝ} (hK : 0 ≤ K)
    (hupper : ∀ x y, dist (f x) (f y) ≤ K * dist x y + C) :
    GroupBornologous f := by
…
```
Mentions: OAI.PolycyclicRecognition.GroupBornologous

theorem OAI.PolycyclicRecognition.finite_groupDifference_range_of_metric_bound line 50

Source documentation

Uniformly bounded metric displacement is a finite set of group errors.

theorem finite_groupDifference_range_of_metric_bound (r : G → G)
    (hfinite : ∀ R : ℝ, (closedBall (1 : G) R).Finite)
    {E : ℝ} (herror : ∀ x, dist x (r x) ≤ E) :
    (Set.range fun x => x⁻¹ * r x).Finite := by
…

def OAI.PolycyclicRecognition.groupCoarseEquivalenceOfMetricInverse line 61

Source documentation

Coarse inverse metric maps produce the concrete equivalence used by Li's group-cohomological invariance theorems.

def groupCoarseEquivalenceOfMetricInverse (f : G → H) (r : H → G)
    (hfiniteG : ∀ R : ℝ, (closedBall (1 : G) R).Finite)
    (hfiniteH : ∀ R : ℝ, (closedBall (1 : H) R).Finite)
    {K C K' C' E E' : ℝ} (hK : 0 ≤ K) (hK' : 0 ≤ K')
    (hf : ∀ x y, dist (f x) (f y) ≤ K * dist x y + C)
    (hr : ∀ x y, dist (r x) (r y) ≤ K' * dist x y + C')
    (hleft : ∀ x, dist x (r (f x)) ≤ E)
    (hright : ∀ y, dist y (f (r y)) ≤ E') :
    GroupCoarseEquivalence G H where
…

Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence

def OAI.PolycyclicRecognition.groupCoarseEquivalenceOfQuasiIsometry line 80

Source documentation

A metric quasi-isometry yields an actual discrete-group coarse equivalence. The inverse is chosen from coarse surjectivity, and all its control estimates are derived from the lower inequality.

def groupCoarseEquivalenceOfQuasiIsometry (f : G → H)
    (hfiniteG : ∀ R : ℝ, (closedBall (1 : G) R).Finite)
    (hfiniteH : ∀ R : ℝ, (closedBall (1 : H) R).Finite)
    {K C K' C' E : ℝ} (hK : 0 ≤ K) (hK' : 0 ≤ K')
    (hupper : ∀ x y, dist (f x) (f y) ≤ K * dist x y + C)
    (hlower : ∀ x y, dist x y ≤ K' * dist (f x) (f y) + C')
    (hsurj : ∀ y, ∃ x, dist y (f x) ≤ E) : GroupCoarseEquivalence G H := by
…

Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence