Documentation

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

Inverse function theorem, C^r case #

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

source
noncomputable def ContDiffAt.toOpenPartialHomeomorph {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] (f : E → F) {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
OpenPartialHomeomorph E F

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

Equations
Instances For
    source
    @[simp]
    theorem ContDiffAt.toOpenPartialHomeomorph_coe {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
    ↑(toOpenPartialHomeomorph f hf hf' hn) = f
    source
    theorem ContDiffAt.mem_toOpenPartialHomeomorph_source {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
    a ∈ (toOpenPartialHomeomorph f hf hf' hn).source
    source
    theorem ContDiffAt.image_mem_toOpenPartialHomeomorph_target {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
    f a ∈ (toOpenPartialHomeomorph f hf hf' hn).target
    source
    noncomputable 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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
    F → E

    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
      source
      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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
      hf.localInverse hf' hn (f a) = a
      source
      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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : n ≠ 0) :
      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.toOpenPartialHomeomorph) is also ContDiff.