MovingPointedLimitApproximation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Pointed approximations with moving physical centers

def OAI.RegularPointCoordinates.PointedSequenceConverges line 15
Source documentation
Pointed metric convergence allowing the physical centers to move.
```
def PointedSequenceConverges {X Y : Type*} [MetricSpace X] [MetricSpace Y]
    (p : ℕ → X) (q : Y) (r : ℕ → ℝ) : Prop :=
…
```
def OAI.RegularPointCoordinates.MovingRescalingNetFamily.netIndex line 26
def OAI.RegularPointCoordinates.MovingRescalingNetFamily.netMap line 32
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.MovingRescalingNetFamily.netMap_data line 39

theorem OAI.RegularPointCoordinates.MovingRescalingNetFamily.eventually_net_dist line 57

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.MovingRescalingNetFamily.pointedSequenceConverges line 72
Source documentation
The completed sampled limit is a pointed limit of the original rescalings, using maps constructed directly from the finite nets.
```
theorem pointedSequenceConverges :
    PointedSequenceConverges (p ∘ phi) ((none : s.Index) : UniformSpace.Completion s.Index) (r ∘ phi) := by
…
```
Mentions: OAI.RegularPointCoordinates.PointedSequenceConverges