The analytic inverse and implicit function theorems

Let f : E → F be analytic at a, with E complete, and suppose its derivative at a is a continuous linear equivalence. Then f restricts to an OpenPartialHomeomorph around a which is analytic on its source and whose inverse is analytic on its whole target (AnalyticAt.exists_openPartialHomeomorph). Mathlib's OpenPartialHomeomorph.analyticAt_symm gives analyticity of an inverse at one point where the derivative is known to be invertible. Invertibility at the base point alone suffices here because it persists throughout the source of the inverse function theorem's homeomorphism (HasStrictFDerivAt.isInvertible_of_mem_toOpenPartialHomeomorph_source).

Applying the inverse function theorem to (w, z) ↦ (f (w, z), w) gives the analytic implicit function theorem: the implicit functions of Mathlib's ImplicitFunctionData and HasStrictFDerivAt.implicitFunctionOfProdDomain are analytic when the defining equation is. For a scalar equation f (w, z) = 0 with ∂f/∂z ≠ 0 this is the implicit root theorem: near a simple zero, the zeros of f form the graph of an analytic function of w (AnalyticAt.exists_analyticAt_eventually_eq_zero_iff).

Everything holds over an arbitrary nontrivially normed field 𝕜, in particular over ℝ and ℂ; the implicit root theorem asks 𝕜 to be complete.

Main results

• HasStrictFDerivAt.analyticOnNhd_toOpenPartialHomeomorph_symm: the local inverse built by the inverse function theorem is analytic on its target wherever f is analytic on its source.
• HasStrictFDerivAt.analyticAt_localInverse: the local inverse is analytic at f a.
• AnalyticAt.exists_openPartialHomeomorph: the analytic inverse function theorem.
• ImplicitFunctionData.analyticAt_implicitFunction and HasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain: the analytic implicit function theorem.
• AnalyticAt.exists_analyticAt_eventually_eq_zero_iff: the analytic implicit root theorem.

References

• S. G. Krantz, H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser (2002), Chapter 2 (the real analytic inverse and implicit function theorems).
• R. C. Gunning, H. Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall (1965), Chapter I (the holomorphic inverse and implicit function theorems).

theorem HasStrictFDerivAt.analyticAt_toOpenPartialHomeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {L : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑L) a) {y : F} (hy : y ∈ (toOpenPartialHomeomorph f hf).target) (hfy : AnalyticAt 𝕜 f (↑(toOpenPartialHomeomorph f hf).symm y)) : AnalyticAt 𝕜 (↑(toOpenPartialHomeomorph f hf).symm) y

The local inverse built by the inverse function theorem is analytic at every point y of its target at whose preimage f is analytic. Invertibility of the derivative is assumed only at the base point a.

theorem HasStrictFDerivAt.analyticOnNhd_toOpenPartialHomeomorph_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {L : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑L) a) (hfs : AnalyticOnNhd 𝕜 f (toOpenPartialHomeomorph f hf).source) : AnalyticOnNhd 𝕜 (↑(toOpenPartialHomeomorph f hf).symm) (toOpenPartialHomeomorph f hf).target

If f is analytic on the source of the homeomorphism built by the inverse function theorem, then its inverse is analytic on the whole target.

theorem HasStrictFDerivAt.analyticAt_localInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {L : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑L) a) (ha : AnalyticAt 𝕜 f a) : AnalyticAt 𝕜 (localInverse f L a hf) (f a)

The local inverse of a map analytic at a, with invertible derivative there, is analytic at f a. This is the several-variable form of Mathlib's AnalyticAt.analyticAt_localInverse.

theorem AnalyticAt.exists_openPartialHomeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {a : E} (hf : AnalyticAt 𝕜 f a) {L : E ≃L[𝕜] F} (hL : fderiv 𝕜 f a = ↑L) {s : Set E} (hs : s ∈ nhds a) : ∃ (Θ : OpenPartialHomeomorph E F), ↑Θ = f ∧ a ∈ Θ.source ∧ Θ.source ⊆ s ∧ AnalyticOnNhd 𝕜 f Θ.source ∧ AnalyticOnNhd 𝕜 (↑Θ.symm) Θ.target

The analytic inverse function theorem. A map analytic at a, whose derivative at a is a continuous linear equivalence, coincides with an OpenPartialHomeomorph whose source is a neighbourhood of a inside any prescribed neighbourhood s, which is analytic on its source, and whose inverse is analytic on its target.

theorem ImplicitFunctionData.analyticAt_implicitFunction {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] {φ : ImplicitFunctionData 𝕜 E F G} (hl : AnalyticAt 𝕜 φ.leftFun φ.pt) (hr : AnalyticAt 𝕜 φ.rightFun φ.pt) : AnalyticAt 𝕜 (Function.uncurry φ.implicitFunction) (φ.prodFun φ.pt)

The analytic implicit function theorem, general form: the implicit function defined by analytic leftFun and rightFun is analytic.

theorem HasStrictFDerivAt.analyticAt_implicitFunctionOfProdDomain {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {E₁ : Type u_4} [NormedAddCommGroup E₁] [NormedSpace 𝕜 E₁] [CompleteSpace E₁] {f : E₁ × E → F} {f'u : E₁ × E →L[𝕜] F} {u : E₁ × E} (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E).IsInvertible) (hf : AnalyticAt 𝕜 f u) : AnalyticAt 𝕜 (dfu.implicitFunctionOfProdDomain if₂u) u.1

The analytic implicit function theorem. If f : E₁ × E → F is analytic at u and its partial derivative in the second variable is invertible there, the implicit function ψ with f (x, ψ x) = f u near u.1 is analytic at u.1.

theorem AnalyticAt.exists_analyticAt_eventually_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [CompleteSpace 𝕜] {f : E × 𝕜 → 𝕜} {u : E × 𝕜} (hf : AnalyticAt 𝕜 f u) (hu : f u = 0) (h : deriv (fun (z : 𝕜) => f (u.1, z)) u.2 ≠ 0) : ∃ (g : E → 𝕜), AnalyticAt 𝕜 g u.1 ∧ g u.1 = u.2 ∧ (∀ᶠ (w : E) in nhds u.1, f (w, g w) = 0) ∧ ∀ᶠ (v : E × 𝕜) in nhds u, f v = 0 ↔ g v.1 = v.2

The analytic implicit root theorem. Let f (w, z) be analytic at u = (w₀, z₀), with f u = 0 and ∂f/∂z ≠ 0 at u. Then there is a function g, analytic at w₀ with g w₀ = z₀, such that near u the zeros of f are exactly the points (w, g w); in particular f (w, g w) = 0 for all w near w₀.