OAI/Geometry/RCD/Metric/HoleSourceBall.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.coordinate_hole_lift line 13

   Source documentation

   Lift the center of a missing target ball from its boundary contact. Only the pointed density clause is needed.

   theorem coordinate_hole_lift {X : Type*} [MetricSpace X] {n : ℕ}
       {u : X → Euclidean n} {z : X} {c : Euclidean n} {r : ℝ} (hr : 0 < r)
       (htouch : dist (u z) c=r)
       (happ : IsPointedApproximation z 0 (64*r) (1/16) (1/128)
         (fun x => (64*r)⁻¹ • (u x-u z))) :
       ∃ x : X, dist x z ≤ 4*r ∧ dist (u x) c ≤ r/2 := by
   …

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

2. theorem OAI.RegularPointCoordinates.source_ball_avoids_good_set line 40

   Source documentation

   A Lipschitz source ball around that lift maps strictly inside the hole, and therefore is disjoint from the original good set.

   theorem source_ball_avoids_good_set {X : Type*} [MetricSpace X] {n : ℕ}
       {u : X → Euclidean n} {U Ω : Set X} {x : X} {c : Euclidean n} {r C : ℝ}
       (hr : 0 < r) (hC : 0 < C)
       (hsub : ball x (r/(4*C)) ⊆ Ω)
       (hlip : ∀ y ∈ Ω, dist (u y) (u x) ≤ C*dist y x)
       (hclose : dist (u x) c ≤ r/2) (hmiss : Disjoint (ball c r) (u '' U)) :
       (∀ y ∈ ball x (r/(4*C)), u y ∈ ball c r) ∧ Disjoint (ball x (r/(4*C))) U := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean