TransferredHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A height homomorphism from the transferred translation action

Coarse maps and a Lipschitz height map define a height quasi-action. An affine height bound permits invariant-mean correction to a genuine homomorphism.

theorem OAI.PolycyclicRecognition.TransferredHeight.composition_close line 27

Source documentation

The Lipschitz height map turns the metric action defect into a uniform height defect with the stated constant.

theorem composition_close (f : H → X) (r : X → H) (π : X → W)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (L K C E : ℝ) (hL : 0 ≤ L) (hK : 0 ≤ K)
    (hπ : ∀ x y, ‖π x - π y‖ ≤ L * dist x y)
    (hf : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (hrf : ∀ a, dist (r (f a)) a ≤ E) (h k : H) (x : X) :
    ‖π (transferredMap f r h (transferredMap f r k x)) -
      π (transferredMap f r (h * k) x)‖ ≤ L * (K * E + C) := by
…

Mentions: OAI.PolycyclicRecognition.transferredMap

def OAI.PolycyclicRecognition.TransferredHeight.quasiAction line 43

Source documentation

The concrete quasi-action induced by f ∘ L_h ∘ r, with shifts π (f h). Surjectivity belongs to the height map; no exact action law is assumed.

def quasiAction (f : H → X) (r : X → H) (π : X → W)
    (A : H → W ≃L[ℝ] W) (hπsurj : Function.Surjective π)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (L K C E B : ℝ) (hL : 0 ≤ L) (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hE : 0 ≤ E) (hB : 0 ≤ B)
    (hπ : ∀ x y, ‖π x - π y‖ ≤ L * dist x y)
    (hf : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (hrf : ∀ a, dist (r (f a)) a ≤ E)
    (haffine : ∀ h x, ‖π (transferredMap f r h x) - (π (f h) + A h (π x))‖ ≤ B) :
    HeightQuasiAction H X W where
…

Mentions: OAI.PolycyclicRecognition.transferredMap, OAI.PolycyclicRecognition.HeightQuasiAction

theorem OAI.PolycyclicRecognition.TransferredHeight.exists_normal_finiteIndex_height line 68

Source documentation

Amenability and finitely many affine linear parts produce a normal subgroup of finite index and a genuine height homomorphism. Its kernel has uniformly bounded original height. The geometric affine estimate is still a hypothesis.

theorem exists_normal_finiteIndex_height [FiniteDimensional ℝ W]
    (f : H → X) (r : X → H) (π : X → W)
    (A : H → W ≃L[ℝ] W) (hπsurj : Function.Surjective π)
    (hleft : ∀ h a b : H, dist (h * a) (h * b) = dist a b)
    (L K C E B : ℝ) (hL : 0 ≤ L) (hK : 0 ≤ K) (hC : 0 ≤ C)
    (hE : 0 ≤ E) (hB : 0 ≤ B)
    (hπ : ∀ x y, ‖π x - π y‖ ≤ L * dist x y)
    (hf : ∀ a b, dist (f a) (f b) ≤ K * dist a b + C)
    (hrf : ∀ a, dist (r (f a)) a ≤ E)
    (haffine : ∀ h x, ‖π (transferredMap f r h x) - (π (f h) + A h (π x))‖ ≤ B)
    (M : InvariantMean H) (hfinite : Set.Finite (Set.range A)) :
    ∃ (H₀ : Subgroup H), H₀.Normal ∧ H₀.FiniteIndex ∧
…

Mentions: OAI.PolycyclicRecognition.transferredMap