LimitChart.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From finite-scale Taylor estimates to the limiting chart

Geometric increments, derivative bounds on scale-selected value-space segments, and linear separation give two-sided distance bounds for the limit. Euclidean invariance of domain gives its open image, as in Hatcher, Algebraic Topology (2002), Theorem 2B.3.

theorem OAI.RegularPointCoordinates.quarter_scale_arithmetic line 20

theorem OAI.RegularPointCoordinates.exists_limit_dist_bounds_of_taylor line 34

Source documentation

The all-pairs metric conclusion from scale-selected Taylor estimates and a geometric increment bound. All source distances are ambient ones.

theorem exists_limit_dist_bounds_of_taylor
    {X : Type*} [MetricSpace X] {n : ℕ}
    (u : X → Euclidean n) (h : ℕ → Euclidean n → Euclidean n)
    (dh : ℕ → Euclidean n → Euclidean n →L[ℝ] Euclidean n)
    (ddh : ℕ → Euclidean n → Euclidean n →L[ℝ]
      (Euclidean n →L[ℝ] Euclidean n))
    {q C : ℝ} (hq : 1 ≤ q)
    (hstep : ∀ i x, dist (h i (u x)) (h (i + 1) (u x)) ≤ C * (1 / 2 : ℝ) ^ i)
    (hpairs : ∀ x z : X, x ≠ z → ∃ i M,
      0 ≤ M ∧
      (∀ y ∈ segment ℝ (u x) (u z), HasFDerivAt (h i) (dh i y) y) ∧
      (∀ y ∈ segment ℝ (u x) (u z), HasFDerivAt (dh i) (ddh i y) y) ∧
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.hasOpenBilipschitzChart_of_taylor_data line 85

Source documentation

Scale-selected Taylor bounds and geometric increment estimates give an open bi-Lipschitz chart by Euclidean invariance of domain.

theorem hasOpenBilipschitzChart_of_taylor_data
    {X : Type*} [MetricSpace X] {n : ℕ} {p : X}
    (hIOD : EuclideanInvarianceOfDomain n)
    {U : Set X} (hU : IsOpen U) (hp : p ∈ U)
    {O : Set (Euclidean n)} (hO : IsOpen O) (u : U ≃ₜ O)
    (h : ℕ → Euclidean n → Euclidean n)
    (dh : ℕ → Euclidean n → Euclidean n →L[ℝ] Euclidean n)
    (ddh : ℕ → Euclidean n → Euclidean n →L[ℝ]
      (Euclidean n →L[ℝ] Euclidean n))
    {q C : ℝ} (hq : 1 ≤ q)
    (hstep : ∀ i (x : U),
      dist (h i (u x)) (h (i + 1) (u x)) ≤ C * (1 / 2 : ℝ) ^ i)
…

Mentions: OAI.RegularPointCoordinates.EuclideanInvarianceOfDomain, OAI.RegularPointCoordinates.Euclidean