Inverse function theorem, the "easy half"

In this file we prove several versions of the following theorem. Consider three functions f : F → G, g : E → F, and h : E → G, together with "candidate derivatives" f' : F →L[𝕜] G, g' : E →L[𝕜] F, and h' : E →L[𝕜] G. Suppose that

• f ∘ g = h in a neighborhood of a;
• h has derivative h' at a;
• f has derivative f' at g a;
• g is continuous at a;
• either f' has a right inverse f'⁻¹ and g' = f'⁻¹ ∘ h', or f' is a topological embedding and h' = f' ∘ g'.

Then g has derivative g' at a. We prove these theorems for different differentiability predicates, then specialize it to the cases when f' is a linear equivalence and/or h = id.

Left inverse

In this section, we prove that g has derivative f'⁻¹ ∘ h' whenever h = f ∘ g has derivative h' and f'⁻¹ is a left inverse to f'.

theorem HasFDerivAtFilter.of_comp_of_leftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G} {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {lE : Filter (E × E)} {lF : Filter (F × F)} (hg : Filter.Tendsto (Prod.map g g) lE lF) (hf : HasFDerivAtFilter f f' lF) (hh : HasFDerivAtFilter h h' lE) (hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h) (hf'symm : Function.LeftInverse ⇑f'symm ⇑f') : HasFDerivAtFilter g (f'symm ∘SL h') lE

theorem HasFDerivWithinAt.of_comp_of_leftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G} {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {a : E} {s : Set E} {t : Set F} (hst : Filter.Tendsto g (nhdsWithin a s) (nhdsWithin (g a) t)) (hf : HasFDerivWithinAt f f' t (g a)) (hh : HasFDerivWithinAt h h' s a) (hcomp : f ∘ g =ᶠ[nhdsWithin a s] h) (hf'symm : Function.LeftInverse ⇑f'symm ⇑f') (ha : a ∈ s) : HasFDerivWithinAt g (f'symm ∘SL h') s a

theorem HasFDerivAt.of_comp_of_leftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G} {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {a : E} (hgc : ContinuousAt g a) (hf : HasFDerivAt f f' (g a)) (hh : HasFDerivAt h h' a) (hcomp : f ∘ g =ᶠ[nhds a] h) (hf'symm : Function.LeftInverse ⇑f'symm ⇑f') : HasFDerivAt g (f'symm ∘SL h') a

theorem HasStrictFDerivAt.of_comp_of_leftInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {f' : F →L[𝕜] G} {h' : E →L[𝕜] G} {f'symm : G →L[𝕜] F} {a : E} (hgc : ContinuousAt g a) (hf : HasStrictFDerivAt f f' (g a)) (hh : HasStrictFDerivAt h h' a) (hcomp : f ∘ g =ᶠ[nhds a] h) (hf'symm : Function.LeftInverse ⇑f'symm ⇑f') : HasStrictFDerivAt g (f'symm ∘SL h') a

Embedding

In this section we show that g has derivative g' provided that h = f ∘ g has derivative f' ∘ g', where f' is a topological embedding.

theorem HasFDerivAtFilter.of_comp_of_isEmbedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F} {f' : F →L[𝕜] G} {lE : Filter (E × E)} {lF : Filter (F × F)} (hg : Filter.Tendsto (Prod.map g g) lE lF) (hf : HasFDerivAtFilter f f' lF) (hf' : Topology.IsEmbedding ⇑f') (hh : HasFDerivAtFilter h (f' ∘SL g') lE) (hcomp : Prod.map (f ∘ g) (f ∘ g) =ᶠ[lE] Prod.map h h) : HasFDerivAtFilter g g' lE

theorem HasFDerivWithinAt.of_comp_of_isEmbedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F} {f' : F →L[𝕜] G} {a : E} {s : Set E} {t : Set F} (hg : Filter.Tendsto g (nhdsWithin a s) (nhdsWithin (g a) t)) (hf : HasFDerivWithinAt f f' t (g a)) (hf' : Topology.IsEmbedding ⇑f') (hh : HasFDerivWithinAt h (f' ∘SL g') s a) (hcomp : f ∘ g =ᶠ[nhdsWithin a s] h) (ha : a ∈ s) : HasFDerivWithinAt g g' s a

theorem HasFDerivAt.of_comp_of_isEmbedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F} {f' : F →L[𝕜] G} {a : E} (hg : ContinuousAt g a) (hf : HasFDerivAt f f' (g a)) (hf' : Topology.IsEmbedding ⇑f') (hh : HasFDerivAt h (f' ∘SL g') a) (hcomp : f ∘ g =ᶠ[nhds a] h) : HasFDerivAt g g' a

theorem HasStrictFDerivAt.of_comp_of_isEmbedding {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F} {f' : F →L[𝕜] G} {a : E} (hg : ContinuousAt g a) (hf : HasStrictFDerivAt f f' (g a)) (hf' : Topology.IsEmbedding ⇑f') (hh : HasStrictFDerivAt h (f' ∘SL g') a) (hcomp : f ∘ g =ᶠ[nhds a] h) : HasStrictFDerivAt g g' a

Local left inverse (equivalence)

theorem HasFDerivAt.of_local_left_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : F → E} {f' : F ≃L[𝕜] E} {a : E} (hg : ContinuousAt g a) (hf : HasFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : E) in nhds a, f (g y) = y) : HasFDerivAt g (↑f'.symm) a

If f (g x) = x for x in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a, then g has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem HasFDerivWithinAt.of_local_left_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {f : F → E} {f' : F ≃L[𝕜] E} {a : E} {s : Set E} {t : Set F} (hg : Filter.Tendsto g (nhdsWithin a s) (nhdsWithin (g a) t)) (hf : HasFDerivWithinAt f (↑f') t (g a)) (ha : a ∈ s) (hfg : ∀ᶠ (x : E) in nhdsWithin a s, f (g x) = x) : HasFDerivWithinAt g (↑f'.symm) s a

If f (g x) = x for x in a neighborhood of a within s, g maps a neighborhood of a within s to a neighborhood of g a within t, and f has an invertible derivative f' at g a within t, then g has the derivative f'⁻¹ at a within s.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem HasStrictFDerivAt.of_local_left_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a) (hf : HasStrictFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) : HasStrictFDerivAt g (↑f'.symm) a

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem OpenPartialHomeomorph.hasStrictFDerivAt_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasStrictFDerivAt (↑f) (↑f') (↑f.symm a)) : HasStrictFDerivAt (↑f.symm) (↑f'.symm) a

If f is an open partial homeomorphism defined on a neighbourhood of f.symm a, and f has an invertible derivative f' in the sense of strict differentiability at f.symm a, then f.symm has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem OpenPartialHomeomorph.hasFDerivAt_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : OpenPartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasFDerivAt (↑f) (↑f') (↑f.symm a)) : HasFDerivAt (↑f.symm) (↑f'.symm) a

If f is an open partial homeomorphism defined on a neighbourhood of f.symm a, and f has an invertible derivative f' at f.symm a, then f.symm has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.