Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

Inverse function theorem, smooth case #

In this file we specialize the inverse function theorem to C^r-smooth functions.

def ContDiffAt.toPartialHomeomorph {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] (f : EF) {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :

Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, returns a PartialHomeomorph with to_fun = f and a ∈ source.

Equations
Instances For
    @[simp]
    theorem ContDiffAt.toPartialHomeomorph_coe {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
    theorem ContDiffAt.mem_toPartialHomeomorph_source {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
    a (ContDiffAt.toPartialHomeomorph f hf hf' hn).source
    theorem ContDiffAt.image_mem_toPartialHomeomorph_target {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
    f a (ContDiffAt.toPartialHomeomorph f hf hf' hn).target
    def ContDiffAt.localInverse {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
    FE

    Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, returns a function that is locally inverse to f.

    Equations
    Instances For
      theorem ContDiffAt.localInverse_apply_image {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      hf.localInverse hf' hn (f a) = a
      theorem ContDiffAt.to_localInverse {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : EF} {f' : E ≃L[𝕂] F} {a : E} {n : ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 n) :
      ContDiffAt 𝕂 n (hf.localInverse hf' hn) (f a)

      Given a ContDiff function over 𝕂 (which is or ) with an invertible derivative at a, the inverse function (produced by ContDiff.toPartialHomeomorph) is also ContDiff.