MetricLimit.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Metric estimates for limiting regular-point coordinates

These lemmas isolate the elementary metric part of the passage to a limiting chart. An approximating map may be selected separately for each pair of points; no global injectivity of an approximating map is required.

theorem OAI.RegularPointCoordinates.exists_dyadic_scale line 23
Source documentation
The dyadic scale used for a pair of points in the limiting-chart argument.
```
theorem exists_dyadic_scale {t : ℝ} (ht : 0 < t) (htone : t ≤ 1) :
    ∃ i : ℕ, t ≤ (1 / 2 : ℝ) ^ i ∧ (1 / 2 : ℝ) ^ i < 2 * t := by
…
```

theorem OAI.RegularPointCoordinates.dist_bounds_of_pointwise_limit line 37

Source documentation

Two-sided distance estimates are preserved under pointwise convergence.

theorem dist_bounds_of_pointwise_limit {l : Filter ι} [l.NeBot]
    {f : ι → X → Y} {F : X → Y} {a b : ℝ}
    (hlim : ∀ x, Tendsto (fun i => f i x) l (𝓝 (F x)))
    (hbound : ∀ᶠ i in l, ∀ x z,
      a * dist x z ≤ dist (f i x) (f i z) ∧
      dist (f i x) (f i z) ≤ b * dist x z) (x z : X) :
    a * dist x z ≤ dist (F x) (F z) ∧
      dist (F x) (F z) ≤ b * dist x z := by
…

theorem OAI.RegularPointCoordinates.dist_bounds_of_approximation line 50

Source documentation

A pairwise bound loses only the sum of the two endpoint errors.

theorem dist_bounds_of_approximation {F f : X → Y} {a b e : ℝ} (x z : X)
    (hlower : a * dist x z ≤ dist (f x) (f z))
    (hupper : dist (f x) (f z) ≤ b * dist x z)
    (herror : dist (F x) (f x) + dist (F z) (f z) ≤ e * dist x z) :
    (a - e) * dist x z ≤ dist (F x) (F z) ∧
      dist (F x) (F z) ≤ (b + e) * dist x z := by
…

theorem OAI.RegularPointCoordinates.dist_bounds_of_pairwise_approximants line 63

Source documentation

The scale of an approximating map is allowed to depend on both points.

theorem dist_bounds_of_pairwise_approximants
    {f : ι → X → Y} {F : X → Y} {a b e : ℝ}
    (happrox : ∀ x z, ∃ i,
      a * dist x z ≤ dist (f i x) (f i z) ∧
      dist (f i x) (f i z) ≤ b * dist x z ∧
      dist (F x) (f i x) + dist (F z) (f i z) ≤ e * dist x z)
    (x z : X) :
    (a - e) * dist x z ≤ dist (F x) (F z) ∧
      dist (F x) (F z) ≤ (b + e) * dist x z := by
…

theorem OAI.RegularPointCoordinates.continuous_of_dist_upper_bound line 76
Source documentation
The upper metric estimate supplies the continuity needed for a chart.
```
theorem continuous_of_dist_upper_bound {F : X → Y} {b : ℝ}
    (hupper : ∀ x z, dist (F x) (F z) ≤ b * dist x z) : Continuous F :=
…
```

theorem OAI.RegularPointCoordinates.exists_limit_of_geometric_step line 83

Source documentation

Geometric step bounds construct the limiting map and a uniform quantitative tail bound. This is applied to the renormalized maps on their common domain.

theorem exists_limit_of_geometric_step [CompleteSpace Y]
    {f : ℕ → X → Y} {r C : ℝ} (hr : r < 1)
    (hstep : ∀ i x, dist (f i x) (f (i + 1) x) ≤ C * r ^ i) :
    ∃ F : X → Y,
      (∀ x, Tendsto (fun i => f i x) atTop (𝓝 (F x))) ∧
      ∀ i x, dist (f i x) (F x) ≤ C * r ^ i / (1 - r) := by
…

theorem OAI.RegularPointCoordinates.injective_of_dist_lower_bound line 106

Source documentation

A positive lower distance bound separates every pair of source points.

theorem injective_of_dist_lower_bound {F : X → Y} {a : ℝ} (ha : 0 < a)
    (hlower : ∀ x z, a * dist x z ≤ dist (F x) (F z)) : Function.Injective F := by
…

theorem OAI.RegularPointCoordinates.lipschitz_antilipschitz_of_dist_bounds line 117

Source documentation

A two-sided distance estimate gives the standard Lipschitz and antilipschitz predicates with reciprocal constants.

theorem lipschitz_antilipschitz_of_dist_bounds {F : X → Y} {a b : ℝ}
    (ha : 0 < a) (hb : 0 ≤ b)
    (hbound : ∀ x z,
      a * dist x z ≤ dist (F x) (F z) ∧
      dist (F x) (F z) ≤ b * dist x z) :
    LipschitzWith ⟨b, hb⟩ F ∧ AntilipschitzWith ⟨a⁻¹, inv_nonneg.mpr ha.le⟩ F := by
…