OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarseMultiplicity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform multiplicity of a coarse embedding

The recognition proof counts points in an intrinsic subgroup word ball using the ambient group's fixed word metric. Its lower quasi-isometry bound gives a uniform bound for the number of points mapping into a fixed-radius target ball. No undistortion of the subgroup is used.

  1. theorem OAI.PolycyclicRecognition.exists_uniform_ball_multiplicity line 17
  2. theorem OAI.PolycyclicRecognition.ball_multiplicity_comp_injective line 52

    Source documentation

    The same multiplicity constant works on any injectively parametrized subset, in particular on a subgroup equipped with its intrinsic word metric.

    theorem ball_multiplicity_comp_injective
    {H J X : Type*} [PseudoMetricSpace X] [DecidableEq H]
    (f : H → X) (ι : J → H) (hι : Function.Injective ι) (M : ℕ) (r : ℝ)
    (hM : ∀ (c : X) (A : Finset H),
      (∀ h ∈ A, dist (f h) c ≤ r) → A.card ≤ M) :
    ∀ (c : X) (A : Finset J), (∀ j ∈ A, dist (f (ι j)) c ≤ r) → A.card ≤ M := by
…