MovingPointedNets.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Countable samples with moving centers and bounded rescaled curvature

Finite nets are padded by the base point, so their labels do not change with the sequence index. Their distance matrices therefore admit one common convergent subsequence.

theorem OAI.RegularPointCoordinates.enumerate_finite_net line 21
Also declared: OAI/Geometry/RCD/Metric/RescalingNetFamily.lean:21 (same declaration text).
structure OAI.RegularPointCoordinates.MovingRescalingNetFamily line 46
Source documentation
Every radius and accuracy has a fixed finite label type across the whole sequence. The point at infinity is not introduced at this stage.
```
structure MovingRescalingNetFamily (p : ℕ → X) (r : ℕ → ℝ) where
…
```
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.movingRescalingNetFamily line 57
Source documentation
CD supplies the countably many finite nets needed by the pointed compactness construction, with no compactness assumption on rescalings.
```
theorem NoncollapsedRCD.movingRescalingNetFamily {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : ℕ → X)
    (r : ℕ → ℝ) (hr : ∀ i, 0 < r i) (hcurv : ∀ i, -1 ≤ K*(r i)^2) :
    Nonempty (MovingRescalingNetFamily p r) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.MovingRescalingNetFamily
abbrev OAI.RegularPointCoordinates.MovingRescalingNetFamily.Index line 88
Source documentation
The base point and all finite-net labels form one countable index set.
```
abbrev Index := Option (Σ R : ℕ, Σ k : ℕ, Fin (s.size R k))
```
def OAI.RegularPointCoordinates.MovingRescalingNetFamily.sample line 90
def OAI.RegularPointCoordinates.MovingRescalingNetFamily.radius line 94
theorem OAI.RegularPointCoordinates.MovingRescalingNetFamily.sample_bound line 99

theorem OAI.RegularPointCoordinates.MovingRescalingNetFamily.exists_limit line 108

Source documentation

One subsequence makes all distances between these actual sample points converge. The limit pseudometric uses the same countable labels.

theorem exists_limit (hr : ∀ i, 0 < r i) :
    ∃ phi : ℕ → ℕ, StrictMono phi ∧ ∃ d : PseudoMetricSpace s.Index,
      ∀ a b, Tendsto (fun k => dist (s.sample (phi k) a) (s.sample (phi k) b) / r (phi k))
        atTop (𝓝 (@dist s.Index d.toDist a b)) := by
…