ProductVerticalDeviation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Horizontal deviation of an almost vertical product geodesic

theorem OAI.RegularPointCoordinates.product_vertical_deviation line 13

Source documentation

A small triangle defect between two points of the zero Euclidean fiber controls the horizontal square. No geodesic structure on the second factor is used.

theorem product_vertical_deviation {Z : Type*} [MetricSpace Z] {n : ℕ}
    (w : WithLp 2 (Euclidean n × Z)) (z₀ z₁ : Z) {δ : ℝ} (hδ : 0 ≤ δ)
    (hdef : dist w (WithLp.toLp 2 (0,z₀))+dist w (WithLp.toLp 2 (0,z₁)) ≤
      dist z₀ z₁+δ) :
    ‖w.fst‖^2 ≤ 2*δ*(dist z₀ z₁+δ) := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean