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 : E → F) {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 ≤ n) : PartialHomeomorph E F

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

• ContDiffAt.toPartialHomeomorph f hf hf' hn = HasStrictFDerivAt.toPartialHomeomorph f ⋯

@[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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 ≤ n) : ↑(ContDiffAt.toPartialHomeomorph f hf hf' hn) = f

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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (↑f') a) (hn : 1 ≤ n) : 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

• hf.localInverse hf' hn = HasStrictFDerivAt.localInverse f f' a ⋯

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 : 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 : E → F} {f' : E ≃L[𝕂] F} {a : E} {n : WithTop ℕ∞} (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.