ChartContraction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Controlled contraction from locally Lipschitz exponential coordinates

This is the elementary metric bridge in the replacement construction. The local metric compatibility of a chosen Lie chart is an explicit premise here; it does not follow from a merely topological exponential chart.

def OAI.PolycyclicRecognition.chartContraction line 22
theorem OAI.PolycyclicRecognition.chartContraction_zero line 25
theorem OAI.PolycyclicRecognition.chartContraction_one line 29

theorem OAI.PolycyclicRecognition.chartContraction_bounds line 34

Source documentation

On a fixed metric ball, radial contraction has a uniform time bound and a spatial bound proportional to the radial parameter.

theorem chartContraction_bounds (φ : E ≃ₜ G) (hφ : φ 0 = 1)
    (hforward : LocallyLipschitz φ) (hbackward : LocallyLipschitz φ.symm)
    {R : ℝ} (hR : 0 ≤ R) :
    ∃ C : ℝ, 1 ≤ C ∧
      (∀ s ∈ Icc (0 : ℝ) 1, ∀ t ∈ Icc (0 : ℝ) 1,
        ∀ z ∈ closedBall (1 : G) R,
        dist (chartContraction φ s z) (chartContraction φ t z) ≤ C * |s - t|) ∧
      (∀ s ∈ Icc (0 : ℝ) 1, ∀ z ∈ closedBall (1 : G) R,
        ∀ w ∈ closedBall (1 : G) R,
        dist (chartContraction φ s z) (chartContraction φ s w) ≤ C * s * dist z w) := by
…

Mentions: OAI.PolycyclicRecognition.chartContraction