LinearMetricChains.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Linear metric chains and coarse Lipschitz bounds

An explicit large-scale geodesic condition allows one to sum local bounds along a chain. For continuous homomorphisms out of proper metric groups, the local bound comes from compactness. This is the elementary metric step in the proper cocompact homomorphism form of the Milnor--Švarc argument.

structure OAI.PolycyclicRecognition.LinearMetricChains line 23
Source documentation
Chains joining any two points with bounded step size and a linear bound on the number of steps, including their vertices and endpoint identities.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:113 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.LinearMetricChains@path.
```
structure LinearMetricChains (X : Type*) [PseudoMetricSpace X] where
…
```

theorem OAI.PolycyclicRecognition.LinearMetricChains.coarseLipschitz line 38

Source documentation

A uniform bound on single steps becomes an affine metric bound by summing along the actual chains.

theorem LinearMetricChains.coarseLipschitz (C : LinearMetricChains X) (f : X → Y)
    {D : ℝ} (hD : 0 ≤ D)
    (hstep : ∀ x y, dist x y ≤ C.step → dist (f x) (f y) ≤ D) :
    ∀ x y, dist (f x) (f y) ≤ (D * C.slope) * dist x y + D * C.error := by
…

theorem OAI.PolycyclicRecognition.continuousHom_bounded_metric_steps line 63
Source documentation
A continuous homomorphism out of a proper metric group has uniformly bounded image displacement on any bounded source step.
```
theorem continuousHom_bounded_metric_steps [ProperSpace G]
    (f : G →* H) (hf : Continuous f) (R : ℝ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ x y, dist x y ≤ R → dist (f x) (f y) ≤ D := by
…
```

theorem OAI.PolycyclicRecognition.continuousHom_coarseLipschitz line 77

Source documentation

The homomorphism's affine bound requires only compactness and the explicit linear chains; no global differentiability estimate is needed.

theorem continuousHom_coarseLipschitz [ProperSpace G] (C : LinearMetricChains G)
    (f : G →* H) (hf : Continuous f) :
    ∃ K B : ℝ, 0 ≤ K ∧ 0 ≤ B ∧
      ∀ x y, dist (f x) (f y) ≤ K * dist x y + B := by
…