PointedVerticalGeodesic.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Actual geodesics under a pointed product approximation

theorem OAI.RegularPointCoordinates.pointed_vertical_geodesic line 15

Source documentation

The geodesic from the base point to a lift of a vertical target stays quantitatively near the vertical fiber. The factor need not be geodesic.

theorem pointed_vertical_geodesic {p x : X} {z₀ z₁ : Z} {ρ ε : ℝ}
    (hρ : 0 < ρ) (he : 0 ≤ ε)
    {f : X → WithLp 2 (Euclidean n × Z)}
    (hf : IsPointedApproximation p (WithLp.toLp 2 (0,z₀)) ρ 1 ε f)
    (hx : dist x p ≤ ρ) (hfx : dist (f x) (WithLp.toLp 2 (0,z₁)) ≤ ε)
    {γ : C(Time,X)} (hγ : IsGeodesic γ) (h0 : γ 0=p) (h1 : γ 1=x) :
    (∀ t, dist (γ t) p ≤ ρ) ∧
    (∀ t, ‖(f (γ t)).fst‖ ≤ Real.sqrt (14*ε*(dist z₀ z₁+7*ε))) ∧
    (∀ t, dist (f (γ t)).snd z₀ ≤ dist z₀ z₁+5*ε) ∧
    dist z₀ z₁-3*ε ≤ dist p x/ρ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsPointedApproximation, OAI.RegularPointCoordinates.Time, OAI.RegularPointCoordinates.IsGeodesic