Theorems · Theorem · global analysis

exists_continuousLinearEquiv_fderivWithin_symm_eq

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace E]
  {f : E → F} {s : Set E} {x : E},
  ContDiffWithinAt 𝕜 2 f s x →
    (fderivWithin 𝕜 f s x).IsInvertible →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ∃ N,
            ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) s x ∧
              ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) s x ∧
                (∀ᶠ (y : E) in nhdsWithin x s, ↑(N y) = fderivWithin 𝕜 f s y) ∧
                  ∀ (v : E),
                    (fderivWithin 𝕜 (fun y => ↑(N y).symm) s x) v =
                      -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm

If a C^2 map has an invertible derivative within a set at a point, then nearby derivatives can be written as continuous linear equivs, which depend in a C^1 way on the point, as well as their inverse, and moreover one can compute the derivative of the inverse.

Defined in

Mathlib.Analysis.Calculus.VectorField

Cited by

3 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpace