Packing.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Packing estimates and intrinsic word balls

This is the finite counting step in Lemma height-kernel-growth of Quasi-isometric recognition of virtually polycyclic groups. A metric cover of orbit points and a bound on the number of source points in a small target ball give a cardinal bound on the original finite set. Applying this to intrinsic word balls does not require the subgroup to be undistorted in an ambient group.

theorem OAI.PolycyclicRecognition.card_le_cover_mul line 27

Source documentation

Count a finite set using a finite metric-ball cover and bounds on each fiber of the cover. The balls may overlap.

theorem card_le_cover_mul [DecidableEq H] [DecidableEq X]
    (S : Finset H) (f : H → X) (centers : Finset X) (radius : ℝ) (M : ℕ)
    (hcover : ∀ h ∈ S, ∃ c ∈ centers, dist (f h) c ≤ radius)
    (hfiber : ∀ c ∈ centers, (S.filter fun h => dist (f h) c ≤ radius).card ≤ M) :
    S.card ≤ centers.card * M := by
…

theorem OAI.PolycyclicRecognition.card_le_cover_mul_of_bounded_multiplicity line 42

Source documentation

A uniform bound on all finite subsets lying over a target ball can be used for every finite source set.

theorem card_le_cover_mul_of_bounded_multiplicity [DecidableEq H] [DecidableEq X]
    (S : Finset H) (f : H → X) (centers : Finset X) (radius : ℝ) (M : ℕ)
    (hcover : ∀ h ∈ S, ∃ c ∈ centers, dist (f h) c ≤ radius)
    (hmultiplicity : ∀ (c : X) (A : Finset H),
      (∀ h ∈ A, dist (f h) c ≤ radius) → A.card ≤ M) :
    S.card ≤ centers.card * M := by
…

theorem OAI.PolycyclicRecognition.boundedMultiplicity_comp_of_injective line 56

Source documentation

Passing to an injectively embedded subgroup preserves the same multiplicity bound, independently of distortion of word metrics.

theorem boundedMultiplicity_comp_of_injective {J : Type*}
    [DecidableEq J] [DecidableEq H]
    (embedding : J → H) (hinjective : Function.Injective embedding)
    (f : H → X) (radius : ℝ) (M : ℕ)
    (hmultiplicity : ∀ (c : X) (A : Finset H),
      (∀ h ∈ A, dist (f h) c ≤ radius) → A.card ≤ M) :
    ∀ (c : X) (A : Finset J),
      (∀ j ∈ A, dist (f (embedding j)) c ≤ radius) → A.card ≤ M := by
…

def OAI.PolycyclicRecognition.wordBall line 78
Source documentation
Products of at most n letters from T. Choosing T symmetric gives the usual intrinsic word ball of radius n in the subgroup generated by T.
```
def wordBall (T : Finset H) : ℕ → Finset H
  | 0 => {1}
  | n + 1 => wordBall T n ∪ T.biUnion (fun t => (wordBall T n).image (t * ·))

@[simp]
```
theorem OAI.PolycyclicRecognition.wordBall_zero line 83
theorem OAI.PolycyclicRecognition.one_mem_wordBall line 86
Source documentation
The identity is represented by the empty word at every radius.
```
theorem one_mem_wordBall (T : Finset H) (n : ℕ) : 1 ∈ wordBall T n := by
…
```
Mentions: OAI.PolycyclicRecognition.wordBall
theorem OAI.PolycyclicRecognition.mem_wordBall_iff line 93
Source documentation
This explicit list characterization identifies the recursive finite sets with intrinsic word balls, rather than with ambient metric balls.
```
theorem mem_wordBall_iff (T : Finset H) (n : ℕ) (h : H) :
    h ∈ wordBall T n ↔ ∃ l : List H,
      l.length ≤ n ∧ (∀ t ∈ l, t ∈ T) ∧ l.prod = h := by
…
```
Mentions: OAI.PolycyclicRecognition.wordBall
theorem OAI.PolycyclicRecognition.wordBall_subset_succ line 139
Source documentation
Every shorter intrinsic word ball is contained in the next one.
```
theorem wordBall_subset_succ (T : Finset H) (n : ℕ) :
    wordBall T n ⊆ wordBall T (n + 1) :=
…
```
Mentions: OAI.PolycyclicRecognition.wordBall

theorem OAI.PolycyclicRecognition.wordBall_card_le_cover_mul line 147

Source documentation

A cover of an intrinsic word ball bounds its cardinality with no hypothesis relating intrinsic word length to an ambient word length.

theorem wordBall_card_le_cover_mul (T : Finset H) (f : H → X) (n : ℕ)
    (centers : Finset X) (M : ℕ)
    (hcover : ∀ h ∈ wordBall T n, ∃ c ∈ centers, dist (f h) c ≤ 1)
    (hmultiplicity : ∀ (c : X) (A : Finset H),
      (∀ h ∈ A, dist (f h) c ≤ 1) → A.card ≤ M) :
    (wordBall T n).card ≤ centers.card * M :=
…

Mentions: OAI.PolycyclicRecognition.wordBall

theorem OAI.PolycyclicRecognition.wordBall_polynomial_card_bound line 157

Source documentation

Polynomially many covering balls and bounded multiplicity give polynomial intrinsic word growth. All constants are independent of the word radius.

theorem wordBall_polynomial_card_bound (T : Finset H) (f : H → X)
    (C b M : ℕ) (centers : ℕ → Finset X)
    (hcenters : ∀ n, (centers n).card ≤ C * (1 + n) ^ b)
    (hcover : ∀ n h, h ∈ wordBall T n → ∃ c ∈ centers n, dist (f h) c ≤ 1)
    (hmultiplicity : ∀ (c : X) (A : Finset H),
      (∀ h ∈ A, dist (f h) c ≤ 1) → A.card ≤ M) :
    ∀ n, (wordBall T n).card ≤ (C * M) * (1 + n) ^ b := by
…

Mentions: OAI.PolycyclicRecognition.wordBall