CoerciveOpenMapping.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A quantitative open-image lemma for the finite coordinate maps

Minimizing distance to the target plus a smooth distance penalty proves local surjectivity from a uniform lower differential bound. This is the finite-dimensional special case needed to pass openness to the limit.

theorem OAI.RegularPointCoordinates.ball_subset_image_of_differential_bound line 27

Source documentation

A lower bound on every differential forces a definite ball in the image. No injectivity or global inverse is required.

theorem ball_subset_image_of_differential_bound {f : E → E} {x : E} {r M : ℝ}
    (hr : 0 < r) (hM : 0 < M)
    (hf : ContinuousOn f (closedBall x r))
    (hd : ∀ z ∈ ball x r, DifferentiableAt ℝ f z)
    (hb : ∀ z ∈ ball x r, ∀ v, ‖v‖ ≤ M * ‖fderiv ℝ f z v‖) :
    ball (f x) (r / (8*M)) ⊆ f '' closedBall x r := by
…

theorem OAI.RegularPointCoordinates.isOpen_image_of_uniform_limit_differential_bound line 122

Source documentation

A uniform limit of maps with a uniform lower differential bound has open image, provided the limit is continuous.

theorem isOpen_image_of_uniform_limit_differential_bound
    {O : Set E} (hO : IsOpen O) {f : ℕ → E → E} {H : E → E}
    (hH : ContinuousOn H O) {M : ℝ} (hM : 0 < M)
    (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 z, z ∈ O → dist (f i z) (H z) ≤ e i) :
    IsOpen (H '' O) := by
…