BoundedPathPacking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

From polynomial-volume thickenings to bounded-height path packing

The endpoint set need not be measurable. We pack finite separated subsets using Haar mass and then take a maximal one. Only the enclosing coordinate regions are measured; this is the precise bridge needed from the Lie-coordinate bounds.

def OAI.PolycyclicRecognition.boundedChainEndpoints line 23
Source documentation
Endpoints of at most n bounded-height steps from a fixed starting point.
```
def boundedChainEndpoints (π : G → W) (L M : ℝ) (n : ℕ) (x : G) : Set G :=
…
```

theorem OAI.PolycyclicRecognition.boundedChain_cover_of_volume line 28

Source documentation

A polynomial-volume region containing the half-unit thickening of the bounded-chain endpoints gives the required polynomial covering bound.

theorem boundedChain_cover_of_volume
    (μ : Measure G) [IsMulLeftInvariant μ] (π : G → W)
    (x : G) (L M : ℝ) (C b : ℕ) (region : ℕ → Set G)
    (hq0 : μ (ball (1 : G) (1 / 2)) ≠ 0)
    (hqtop : μ (ball (1 : G) (1 / 2)) ≠ ⊤)
    (hthick : ∀ n y, y ∈ boundedChainEndpoints π L M n x →
      ball y (1 / 2) ⊆ region n)
    (hvol : ∀ n, μ (region n) ≤
      ((C * (1 + n) ^ b : ℕ) : ℝ≥0∞) * μ (ball (1 : G) (1 / 2))) :
    ∃ centers : ℕ → Finset G,
      (∀ n, (centers n).card ≤ C * (1 + n) ^ b) ∧
      ∀ n m, m ≤ n → ∀ y, BoundedHeightChain π L M m x y →
…

Mentions: OAI.PolycyclicRecognition.boundedChainEndpoints, OAI.PolycyclicRecognition.BoundedHeightChain