CoarseFineCoordinateDistance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Global distance control from a coarse chart and fine local charts

theorem OAI.RegularPointCoordinates.coarse_fine_coordinate_distance line 13

Source documentation

The coarse approximation controls widely separated points. The all-scale charts control the remaining pairs, with the same small error.

theorem coarse_fine_coordinate_distance {X : Type*} [MetricSpace X] {n : ℕ}
    {p : X} {v : X → Euclidean n} {U : Set X} {r S T ε η : ℝ}
    (hr : 0 < r) (hη : 0 ≤ η) (herror : ε*r ≤ η*T)
    (hU : ∀ x ∈ U, dist x p ≤ S*r)
    (hcoarse : IsPointedApproximation p 0 r S ε (fun z => r⁻¹ • (v z-v p)))
    (hfine : ∀ x ∈ U, ∀ s : ℝ, 0 < s → s < T →
      IsPointedApproximation x 0 s (1/16) η (fun z => s⁻¹ • (v z-v x))) :
    ∀ x ∈ U, ∀ y ∈ U,
      (1-32*η)*dist x y ≤ dist (v x) (v y) ∧
        dist (v x) (v y) ≤ (1+32*η)*dist x y := by
…

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

theorem OAI.RegularPointCoordinates.coarse_fine_coordinate_lipschitz line 55