RescalingLimitApproximation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Pointed approximations from the convergent finite nets

def OAI.RegularPointCoordinates.RescalingNetFamily.netIndex line 18
def OAI.RegularPointCoordinates.RescalingNetFamily.netMap line 24
Source documentation
Send a point in the working ball to the corresponding limiting net point. Outside that ball the map takes the base-point value.
```
def netMap (R k i : ℕ) (x : X) : UniformSpace.Completion s.Index := by
…
```
theorem OAI.RegularPointCoordinates.RescalingNetFamily.netMap_data line 31

theorem OAI.RegularPointCoordinates.RescalingNetFamily.eventually_net_dist line 49

Source documentation

A single tail controls every pair of labels in a finite net and the base-point label simultaneously.

theorem eventually_net_dist (R k : ℕ) {delta : ℝ} (hdelta : 0 < delta) :
    ∀ᶠ i in atTop, ∀ a b : Option (Fin (s.size R k)),
      |dist (s.netIndex R k a) (s.netIndex R k b) -
        dist (s.sample (phi i) (s.netIndex R k a))
          (s.sample (phi i) (s.netIndex R k b)) / r (phi i)| < delta := by
…

theorem OAI.RegularPointCoordinates.RescalingNetFamily.rescalingsConverge line 64
Source documentation
The completed sampled limit is a pointed limit of the original rescalings, using maps constructed directly from the finite nets.
```
theorem rescalingsConverge :
    RescalingsConverge p ((none : s.Index) : UniformSpace.Completion s.Index) (r ∘ phi) := by
…
```
Mentions: OAI.RegularPointCoordinates.RescalingsConverge