OpenLimitChart.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Openness of the coordinate limit from its actual approximating maps

theorem OAI.RegularPointCoordinates.hasOpenBilipschitzChart_of_coercive_limit line 16

Source documentation

Only the actual smooth approximants and their uniform lower differential bound are needed for openness of the final bi-Lipschitz chart.

theorem hasOpenBilipschitzChart_of_coercive_limit
    {X : Type*} [MetricSpace X] {n : ℕ} {p : X}
    {U : Set X} (hU : IsOpen U) (hp : p ∈ U)
    {O : Set (Euclidean n)} (hO : IsOpen O) (u : U ≃ₜ O)
    {f : ℕ → Euclidean n → Euclidean n} {H : U → Euclidean n}
    {M L : ℝ} (hM : 0 < M) (hL : 1 ≤ L)
    (hd : ∀ i z, z ∈ O → DifferentiableAt ℝ (f i) z)
    (hb : ∀ i z, z ∈ O → ∀ v, ‖v‖ ≤ M*‖fderiv ℝ (f i) z v‖)
    {e : ℕ → ℝ} (he : Tendsto e atTop (𝓝 0))
    (herr : ∀ i x, dist (f i (u x)) (H x) ≤ e i)
    (hbound : ∀ x z : U, L⁻¹*dist (x:X) (z:X) ≤ dist (H x) (H z) ∧
      dist (H x) (H z) ≤ L*dist (x:X) (z:X)) :
…

Mentions: OAI.RegularPointCoordinates.Euclidean