RescaledPackingBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform cardinality of separated centers in a rescaled ball

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaled_separated_card line 16

Source documentation

A finer covering net bounds every separated family in a fixed rescaled ball. In particular it bounds overlap of enlarged patch balls.

theorem NoncollapsedRCD.rescaled_separated_card {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) {R : ℝ} (hR : 0 < R) :
    ∃ N : ℕ, ∀ (p : X) (r : ℝ), 0 < r → -1 ≤ K*r^2 →
      ∀ s : Finset X,
      (s : Set X).Pairwise (fun x y => r ≤ dist x y) →
      (∀ x ∈ s, dist x p ≤ R*r) → s.card ≤ N := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD