BoundedPathGrowth.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

From bounded-height word paths to polynomial growth

Word chains and a uniform metric multiplicity bound turn polynomial packing of bounded-height chains into polynomial growth. Gromov's theorem then gives virtual nilpotence of the subgroup.

inductive OAI.PolycyclicRecognition.BoundedHeightChain line 20

Source documentation

A finite chain whose steps and heights are uniformly bounded.

inductive BoundedHeightChain (π : X → W) (L M : ℝ) : ℕ → X → X → Prop
  | nil (x : X) (hheight : ‖π x‖ ≤ M) : BoundedHeightChain π L M 0 x x
  | cons {n : ℕ} {x y z : X} (hheight : ‖π x‖ ≤ M) (hstep : dist x y ≤ L)
      (tail : BoundedHeightChain π L M n y z) : BoundedHeightChain π L M (n + 1) x z

/-- A pointwise height domination transfers every bounded-height chain. -/

theorem OAI.PolycyclicRecognition.BoundedHeightChain.change_height line 26

Source documentation

A pointwise height domination transfers every bounded-height chain.

theorem BoundedHeightChain.change_height
    {V : Type*} [NormedAddCommGroup V] {π : X → W} {π' : X → V}
    {L M M' : ℝ} {n : ℕ} {x y : X}
    (h : BoundedHeightChain π L M n x y)
    (hheight : ∀ z, ‖π z‖ ≤ M → ‖π' z‖ ≤ M') :
    BoundedHeightChain π' L M' n x y := by
…

Mentions: OAI.PolycyclicRecognition.BoundedHeightChain

def OAI.PolycyclicRecognition.PolynomialBoundedChainPacking line 37
Source documentation
Polynomial packing of bounded-height chains in the Lie model.
```
def PolynomialBoundedChainPacking [DecidableEq X] (π : X → W) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_height_domination line 47
Source documentation
It suffices to pack chains for a height dominated by the height in the application, as when all representation characters factor through the canonical quotient.
```
theorem polynomialBoundedChainPacking_of_height_domination
    {V : Type*} [NormedAddCommGroup V] [DecidableEq X]
    (π : X → W) (π' : X → V) (C : ℝ) (hC : 0 ≤ C)
    (hdom : ∀ x, ‖π' x‖ ≤ C * ‖π x‖)
    (packing : PolynomialBoundedChainPacking π') : PolynomialBoundedChainPacking π := by
…
```
Mentions: OAI.PolycyclicRecognition.PolynomialBoundedChainPacking
theorem OAI.PolycyclicRecognition.boundedHeightChain_of_word line 59
theorem OAI.PolycyclicRecognition.boundedHeightChain_of_mem_wordBall line 73

theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_boundedHeight_steps line 85

Source documentation

A generating set, bounded steps and bounded multiplicity suffice for the intrinsic growth argument. No metric or undistortion hypothesis on the domain is required.

theorem virtuallyNilpotent_of_boundedHeight_steps
    {J : Type*} [Group J] [DecidableEq J] [DecidableEq X]
    (gromov : GromovPolynomialGrowthInput J)
    (f : J → X) (π : X → W) (packing : PolynomialBoundedChainPacking π)
    (T : Finset J) (hsymm : ∀ t ∈ T, t⁻¹ ∈ T)
    (hgen : Subgroup.closure (T : Set J) = ⊤)
    {L M : ℝ} (hL : 0 ≤ L) (hM : 0 ≤ M)
    (hheight : ∀ j, ‖π (f j)‖ ≤ M)
    (hstep : ∀ j t, t ∈ T → dist (f j) (f (j * t)) ≤ L)
    (N : ℕ) (hN : ∀ (c : X) (A : Finset J),
      (∀ j ∈ A, dist (f j) c ≤ 1) → A.card ≤ N) :
    Group.IsVirtuallyNilpotent J := by
…

Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking

theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_boundedHeight line 107

Source documentation

Intrinsic word growth follows from bounded height and the geometric chain packing property, even when the chosen proper group metric is distorted with respect to the intrinsic word metric.

theorem virtuallyNilpotent_of_boundedHeight
    {J : Type*} [Group J] [MetricSpace J] [IsIsometricSMul J J]
    [Group.FG J] [DecidableEq J] [DecidableEq X]
    (gromov : GromovPolynomialGrowthInput J)
    (f : J → X) (π : X → W) (packing : PolynomialBoundedChainPacking π)
    (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : J) R).Finite)
    {K C K' C' M : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hK' : 0 ≤ K') (hM : 0 ≤ M)
    (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')
    (hheight : ∀ j, ‖π (f j)‖ ≤ M) : Group.IsVirtuallyNilpotent J := by
…

Mentions: OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking