GeodesicShortSteps.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.IsGeodesic.short_step_bound line 16
Source documentation
A uniform estimate for short pairs on one geodesic controls its endpoints with the same constant. The proof uses a finite equal-time subdivision.
```
theorem IsGeodesic.short_step_bound {γ : C(Time,X)} (hγ : IsGeodesic γ)
    (f : X → ℝ) {L δ : ℝ} (hδ : 0 < δ)
    (hshort : ∀ s t : Time, dist (γ s) (γ t) ≤ δ →
      |f (γ s)-f (γ t)| ≤ L*dist (γ s) (γ t)) :
    |f (γ 0)-f (γ 1)| ≤ L*dist (γ 0) (γ 1) := by
…
```
Mentions: OAI.RegularPointCoordinates.Time, OAI.RegularPointCoordinates.IsGeodesic