ControlledContraction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.PolycyclicRecognition.ControlledContraction line 18
Source documentation
The quantitative contraction data used by the interpolation algorithm. It is constructed from coordinates below, rather than assumed to supply a quasi-isometry representative.
```
structure ControlledContraction where
…
```
theorem OAI.PolycyclicRecognition.ControlledContraction.dist_center_le line 32
def OAI.PolycyclicRecognition.ControlledContraction.ofChart line 48
Source documentation
Left translation of radial contraction makes the same constants work about every center of a left-invariant metric.
```
def ofChart (φ : E ≃ₜ G) (hφ : φ 0 = 1)
    (hf : LocallyLipschitz φ) (hb : LocallyLipschitz φ.symm) : ControlledContraction G where
…
```
Mentions: OAI.PolycyclicRecognition.ControlledContraction