UniformLatticeWordMetric.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparing a lattice word metric with its ambient metric

The inclusion of a uniform lattice, equipped with any finite word metric, is continuous and proper. Applying the proved chain argument therefore gives both quasi-isometry inequalities and coarse surjectivity.

theorem OAI.PolycyclicRecognition.IsUniformLattice.wordMetric_quasiIsometry line 27

Source documentation

A uniform lattice with any finite word metric is quasi-isometric to its ambient group, provided that the ambient metric has linear chains.

theorem IsUniformLattice.wordMetric_quasiIsometry {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) (C : LinearMetricChains G)
    {ι : Type*} [Finite ι] (P : Group.Generators Λ ι) :
    ∃ A B A' B' E : ℝ, 0 ≤ A ∧ 0 ≤ B ∧ 0 ≤ A' ∧ 0 ≤ B' ∧ 0 ≤ E ∧
      (∀ x y : Λ, dist (x : G) (y : G) ≤ A * (P.wordLength (x⁻¹ * y) : ℝ) + B) ∧
      (∀ x y : Λ, (P.wordLength (x⁻¹ * y) : ℝ) ≤ A' * dist (x : G) (y : G) + B') ∧
      (∀ g : G, ∃ x : Λ, dist g (x : G) ≤ E) := by
…

theorem OAI.PolycyclicRecognition.IsUniformLattice.exists_wordMetric_quasiIsometry line 62

Source documentation

The finite generating family can itself be obtained from compactness and the ambient chains. No finite generation assumption is needed.

theorem IsUniformLattice.exists_wordMetric_quasiIsometry {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) (C : LinearMetricChains G) :
    ∃ (n : ℕ) (P : Group.Generators Λ (Fin n)),
      ∃ A B A' B' E : ℝ, 0 ≤ A ∧ 0 ≤ B ∧ 0 ≤ A' ∧ 0 ≤ B' ∧ 0 ≤ E ∧
        (∀ x y : Λ, dist (x : G) (y : G) ≤ A * (P.wordLength (x⁻¹ * y) : ℝ) + B) ∧
        (∀ x y : Λ, (P.wordLength (x⁻¹ * y) : ℝ) ≤ A' * dist (x : G) (y : G) + B') ∧
        (∀ g : G, ∃ x : Λ, dist g (x : G) ≤ E) := by
…