Inverse function theorem, C^r case

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

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.

@[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

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

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

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.

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

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.