UniformLatticeMetric.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform lattice metric comparison

A discrete subgroup with a compact set of right-coset representatives is a uniform lattice. Its inclusion has a uniformly close section. This gives the discrete-group coarse comparison required in the duality endgame from a metric quasi-isometry to the ambient Lie group. Neither finite generation nor a recognition conclusion is built into the lattice definition.

def OAI.PolycyclicRecognition.IsUniformLattice line 28
Source documentation
A uniform lattice, expressed by discreteness and a compact fundamental cover. Over a locally compact group this is equivalent to compactness of the coset quotient.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:75 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.IsUniformLattice@path.
```
def IsUniformLattice [TopologicalSpace G] (Λ : Subgroup G) : Prop :=
…
```

theorem OAI.PolycyclicRecognition.IsUniformLattice.exists_covering_radius line 37

Source documentation

Compactness of a fundamental cover gives a uniform distance to the lattice.

theorem IsUniformLattice.exists_covering_radius {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) :
    ∃ R : ℝ, 0 ≤ R ∧ ∀ g : G, ∃ γ : Λ, dist g (γ : G) ≤ R := by
…

theorem OAI.PolycyclicRecognition.IsUniformLattice.finite_closedBall line 53

Source documentation

A discrete subgroup has finite metric balls in a proper ambient group.

theorem IsUniformLattice.finite_closedBall [ProperSpace G] {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) (R : ℝ) :
    (closedBall (1 : Λ) R).Finite := by
…

theorem OAI.PolycyclicRecognition.IsUniformLattice.exists_metric_section line 64

Source documentation

A uniformly close lattice section has explicit coarse Lipschitz bounds.

theorem IsUniformLattice.exists_metric_section {Λ : Subgroup G}
    (hΛ : IsUniformLattice Λ) :
    ∃ (r : G → Λ) (R : ℝ), 0 ≤ R ∧
      (∀ g, dist g (r g : G) ≤ R) ∧
      (∀ x y, dist (r x) (r y) ≤ dist x y + (R + R)) := by
…

theorem OAI.PolycyclicRecognition.IsUniformLattice.nonempty_coarseEquivalence line 87

Source documentation

A metric quasi-isometry to a group containing a uniform lattice gives the actual coarse equivalence with that lattice used by the algebraic duality comparison. All inverse and finite-difference estimates are proved.

theorem IsUniformLattice.nonempty_coarseEquivalence [ProperSpace G]
    {Λ : Subgroup G} (hΛ : IsUniformLattice Λ) (f : H → G)
    (hfinite : ∀ 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 : ∀ g, ∃ x, dist g (f x) ≤ E) :
    Nonempty (GroupCoarseEquivalence H Λ) := by
…

Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence