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}
[IsROrC 𝕂]
{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 : ℕ∞}
(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
- ContDiffAt.toPartialHomeomorph f hf hf' hn = HasStrictFDerivAt.toPartialHomeomorph f (_ : HasStrictFDerivAt f (↑f') a)
Instances For
@[simp]
theorem
ContDiffAt.toPartialHomeomorph_coe
{𝕂 : Type u_1}
[IsROrC 𝕂]
{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 : ℕ∞}
(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}
[IsROrC 𝕂]
{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 : ℕ∞}
(hf : ContDiffAt 𝕂 n f a)
(hf' : HasFDerivAt f (↑f') a)
(hn : 1 ≤ n)
:
a ∈ (ContDiffAt.toPartialHomeomorph f hf hf' hn).toPartialEquiv.source
theorem
ContDiffAt.image_mem_toPartialHomeomorph_target
{𝕂 : Type u_1}
[IsROrC 𝕂]
{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 : ℕ∞}
(hf : ContDiffAt 𝕂 n f a)
(hf' : HasFDerivAt f (↑f') a)
(hn : 1 ≤ n)
:
f a ∈ (ContDiffAt.toPartialHomeomorph f hf hf' hn).toPartialEquiv.target
def
ContDiffAt.localInverse
{𝕂 : Type u_1}
[IsROrC 𝕂]
{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 : ℕ∞}
(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
- ContDiffAt.localInverse hf hf' hn = HasStrictFDerivAt.localInverse f f' a (_ : HasStrictFDerivAt f (↑f') a)
Instances For
theorem
ContDiffAt.localInverse_apply_image
{𝕂 : Type u_1}
[IsROrC 𝕂]
{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 : ℕ∞}
(hf : ContDiffAt 𝕂 n f a)
(hf' : HasFDerivAt f (↑f') a)
(hn : 1 ≤ n)
:
ContDiffAt.localInverse hf hf' hn (f a) = a
theorem
ContDiffAt.to_localInverse
{𝕂 : Type u_1}
[IsROrC 𝕂]
{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 : ℕ∞}
(hf : ContDiffAt 𝕂 n f a)
(hf' : HasFDerivAt f (↑f') a)
(hn : 1 ≤ n)
:
ContDiffAt 𝕂 n (ContDiffAt.localInverse hf 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.