OAI/Geometry/RCD/Metric/HoleBallSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.hole_source_ball_selection line 13

   Source documentation

   The source balls have disjoint images inside disjoint target holes. Thus their disjointness does not require injectivity of the coordinate map.

   theorem hole_source_ball_selection {X ι : Type*} [MetricSpace X] {n : ℕ}
       {u : X → Euclidean n} {U Ω : Set X} {C : ℝ} (hC : 0 < C)
       {z : ι → X} {c : ι → Euclidean n} {r : ι → ℝ} (hr : ∀ i, 0 < r i)
       (htouch : ∀ i, dist (u (z i)) (c i)=r i)
       (happ : ∀ i, IsPointedApproximation (z i) 0 (64*r i) (1/16) (1/128)
         (fun x => (64*r i)⁻¹ • (u x-u (z i))))
       (hroom : ∀ i, ∀ x, dist x (z i) ≤ 4*r i → ball x (r i/(4*C)) ⊆ Ω)
       (hlip : ∀ x ∈ Ω, ∀ y ∈ Ω, dist (u x) (u y) ≤ C*dist x y)
       (hmiss : ∀ i, Disjoint (ball (c i) (r i)) (u '' U))
       (hdisj : Pairwise (fun i j => Disjoint (ball (c i) (r i)) (ball (c j) (r j)))) :
       ∃ x : ι → X,
         (∀ i, dist (x i) (z i) ≤ 4*r i) ∧
   …

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