HeightLipschitz.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the additive error from a vector-valued homomorphism

A homomorphism to a real normed vector group scales exactly on powers. Distances in a left-invariant source metric grow at most linearly on powers. Consequently an affine upper bound for the homomorphism is already a genuine Lipschitz bound. Compactness and the existing linear-chain argument supply the affine bound for continuous homomorphisms.

theorem OAI.PolycyclicRecognition.height_lipschitz_of_affine_bound line 25

Source documentation

The additive constant disappears by applying the bound to arbitrarily large powers. No commutativity of the source is required.

theorem height_lipschitz_of_affine_bound (π : G →* Multiplicative W)
    {K C : ℝ} (hK : 0 ≤ K)
    (hbound : ∀ g, ‖(π g).toAdd‖ ≤ K * dist (1 : G) g + C) :
    ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y := by
…

theorem OAI.PolycyclicRecognition.continuous_height_lipschitz line 50

Source documentation

A continuous vector-valued homomorphism from a proper group with linear metric chains is globally Lipschitz.

theorem continuous_height_lipschitz [ProperSpace G] (C : LinearMetricChains G)
    (π : G →* Multiplicative W) (hπ : Continuous (fun g => (π g).toAdd)) :
    ∃ K : ℝ, 0 ≤ K ∧
      ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y := by
…