MetricQuasiEquivalence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Composing the metric comparisons in a Lie-model reduction

The proper cocompact homomorphism reduction has arrows in both directions. We keep actual coarse inverse maps and their affine bounds, so that the three-arrow zigzag can be composed without assuming a recognition result.

structure OAI.PolycyclicRecognition.MetricQuasiEquivalence line 18
Source documentation
Actual coarse inverse maps with affine metric bounds in both directions.
```
structure MetricQuasiEquivalence (X Y : Type*) [PseudoMetricSpace X] [PseudoMetricSpace Y] where
…
```
def OAI.PolycyclicRecognition.MetricQuasiEquivalence.symm line 33
Source documentation
Reverse a comparison using its specified coarse inverse.
```
def symm (e : MetricQuasiEquivalence X Y) : MetricQuasiEquivalence Y X where
…
```
Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence
def OAI.PolycyclicRecognition.MetricQuasiEquivalence.trans line 43
Source documentation
Compose actual comparisons, including explicit bounds for the errors of their composite inverse maps.
```
def trans (e : MetricQuasiEquivalence X Y) (e' : MetricQuasiEquivalence Y Z) :
    MetricQuasiEquivalence X Z where
…
```
Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence

def OAI.PolycyclicRecognition.MetricQuasiEquivalence.ofQuasiIsometry line 98

Source documentation

Choose a coarse inverse from the coarse-surjectivity part of a quasi-isometry, and prove its affine bound using the lower inequality.

def ofQuasiIsometry (f : X → Y) {K C K' C' E : ℝ}
    (hK : 0 ≤ K) (hC : 0 ≤ C) (hK' : 0 ≤ K') (hC' : 0 ≤ C') (hE : 0 ≤ E)
    (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) : MetricQuasiEquivalence X Y := by
…

Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence

theorem OAI.PolycyclicRecognition.MetricQuasiEquivalence.quasiIsometry_toFun line 123

Source documentation

Recover the usual inequalities from actual coarse inverse maps.

theorem quasiIsometry_toFun (e : MetricQuasiEquivalence X Y) :
    ∃ K C K' C' E : ℝ, 0 ≤ K ∧ 0 ≤ C ∧ 0 ≤ K' ∧ 0 ≤ C' ∧ 0 ≤ E ∧
      (∀ x y, dist (e.toFun x) (e.toFun y) ≤ K * dist x y + C) ∧
      (∀ x y, dist x y ≤ K' * dist (e.toFun x) (e.toFun y) + C') ∧
      (∀ y, ∃ x, dist y (e.toFun x) ≤ E) := by
…

Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence

theorem OAI.PolycyclicRecognition.nonempty_metricQuasiEquivalence_of_proper_cocompact_hom line 147

Source documentation

Coarse inverse maps for a proper cocompact homomorphism, suitable for composition along the model zigzag.

theorem nonempty_metricQuasiEquivalence_of_proper_cocompact_hom
    {G H : Type*} [Group G] [Group H] [MetricSpace G] [MetricSpace H]
    [IsIsometricSMul G G] [IsIsometricSMul H H] [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) :
    Nonempty (MetricQuasiEquivalence G H) := by
…

Mentions: OAI.PolycyclicRecognition.MetricQuasiEquivalence