OAI/Geometry/RCD/Metric/ScaledImageHoleVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.image_hole_volume_at_radius_le line 15

   Source documentation

   The finite hole cover and actual RCD source-ball masses give the image-volume estimate. All coordinate hypotheses are local and explicit.

   theorem NoncollapsedRCD.image_hole_volume_at_radius_le {K : ℝ} {n : ℕ}
       (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) {p : X} {R C ρ : ℝ}
       (hρ : 0 < ρ) (hR : ρ ≤ R) (hC : 1 ≤ C) (hcurv : -1 ≤ K*(2*R)^2)
       {u : X → Euclidean n} {U Ω : Set X} (himage : IsClosed (u '' U))
       (hpoint : ∃ q ∈ ball (0 : Euclidean n) ρ, q ∈ u '' U)
       (hfin : hausdorff n X (Ω \ U) ≠ ⊤)
       (hnear : ∀ z ∈ U, u z ∈ ball 0 ρ → dist z p+4*ρ ≤ R)
       (happ : ∀ z ∈ U, ∀ r : ℝ, 0 < r → r < ρ →
         IsPointedApproximation z 0 (64*r) (1/16) (1/128)
           (fun x => (64*r)⁻¹ • (u x-u z)))
       (hroom : ∀ z ∈ U, u z ∈ ball 0 ρ → ∀ x, dist x z ≤ 4*ρ → ball x (ρ/(4*C)) ⊆ Ω)
       (hlip : ∀ x ∈ Ω, ∀ y ∈ Ω, dist (u x) (u y) ≤ C*dist x y) :
   …

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