RecognitionFromHeight.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Recognition from a geometric height estimate

Corrected height bounds control intrinsic word growth of finitely generated subgroups of its kernel. Polynomial bounded-height chain packing gives elementary amenability, to which the finiteness and duality theorems apply.

theorem OAI.PolycyclicRecognition.virtuallyNilpotent_of_injective_boundedHeight line 26

Source documentation

Intrinsic polynomial growth for an injectively parametrized subgroup of the ambient coarse source. All metric estimates use the ambient source metric.

theorem virtuallyNilpotent_of_injective_boundedHeight
    {J : Type u} [Group J] [Group.FG J] [DecidableEq J] [DecidableEq X]
    (gromov : GromovPolynomialGrowthInput J)
    (ι : J →* H) (hι : Function.Injective ι)
    (f : H → X) (π : X → W) (packing : PolynomialBoundedChainPacking π)
    (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) 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

theorem OAI.PolycyclicRecognition.elementaryAmenable_of_corrected_height line 57

Source documentation

The height-kernel and finite-extension argument, including potentially infinitely generated kernels and nondiscrete height images.

theorem elementaryAmenable_of_corrected_height [DecidableEq X]
    (H₀ : Subgroup H) [H₀.FiniteIndex] (τ : H₀ →* Multiplicative W)
    (gromov : ∀ (J : Subgroup τ.ker) [DecidableEq J], GromovPolynomialGrowthInput J)
    (f : H → X) (π : X → W) (packing : PolynomialBoundedChainPacking π)
    (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    {K C K' C' D : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hK' : 0 ≤ K') (hD : 0 ≤ D)
    (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 : ∀ h : H₀, ‖(τ h).toAdd - π (f h)‖ ≤ D) :
    IsElementaryAmenable H := by
…

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

theorem OAI.PolycyclicRecognition.elementaryAmenable_of_transferred_height line 89

Source documentation

The transferred quasi-action, mean correction, intrinsic subgroup growth, and finite-extension step form one complete argument after the two geometric obligations have been supplied.

theorem elementaryAmenable_of_transferred_height [DecidableEq X]
    (gromov : ∀ (J : Type u) [Group J] [DecidableEq J], GromovPolynomialGrowthInput J)
    (f : H → X) (r : X → H) (π : X → W)
    (packing : PolynomialBoundedChainPacking π)
    (A : H → W ≃L[ℝ] W) (hπsurj : Function.Surjective π)
    (L K C E B K' C' : ℝ) (hL : 0 ≤ L) (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hE : 0 ≤ E) (hB : 0 ≤ B) (hK' : 0 ≤ K')
    (hπ : ∀ x y, ‖π x - π y‖ ≤ L * dist x y)
    (hupper : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (hlower : ∀ a b, dist a b ≤ K' * dist (f a) (f b) + C')
    (hrf : ∀ a, dist (r (f a)) a ≤ E)
    (haffine : ∀ h x,
…

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

theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_corrected_height line 116

Source documentation

The corrected geometric height and bounded-height chain packing imply virtual polycyclicity through the algebraic recognition theorem.

theorem virtuallyPolycyclic_of_corrected_height
    (liFP : LiFinitenessInput) (eaFP : ElementaryAmenableFinitenessInput)
    (liPD : LiDualityInput) (bieri : BieriDualityInput)
    (Γ H : Type) [Group Γ] [Group H] [MetricSpace H] [IsIsometricSMul H H]
    [Group.FG Γ] [Group.FG H]
    {X W : Type} [PseudoMetricSpace X] [DecidableEq X] [NormedAddCommGroup W]
    (H₀ : Subgroup H) [H₀.FiniteIndex] (τ : H₀ →* Multiplicative W)
    (gromov : ∀ (J : Subgroup τ.ker) [DecidableEq J], GromovPolynomialGrowthInput J)
    (f : H → X) (π : X → W) (packing : PolynomialBoundedChainPacking π)
    (hfinite : ∀ R : ℝ, (Metric.closedBall (1 : H) R).Finite)
    {K C K' C' D : ℝ} (hK : 0 ≤ K) (hC : 0 ≤ C) (hK' : 0 ≤ K') (hD : 0 ≤ D)
    (hupper : ∀ x y, dist (f x) (f y) ≤ K * dist x y + C)
…

Mentions: OAI.PolycyclicRecognition.LiFinitenessInput, OAI.PolycyclicRecognition.ElementaryAmenableFinitenessInput, OAI.PolycyclicRecognition.LiDualityInput, OAI.PolycyclicRecognition.BieriDualityInput, OAI.PolycyclicRecognition.GromovPolynomialGrowthInput, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking