RescaledFiniteNets.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite nets for pointed RCD rescalings

The cardinality bound is independent of the rescaling radius and base point. It is obtained from disjoint half-radius balls and the actual CD comparison, so it supplies the finite-net hypothesis of pointed metric compactness.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.rescaled_finite_nets line 23

Source documentation

Every fixed rescaled ball admits a uniformly bounded finite net once the rescaled lower curvature is bounded.

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

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD