Holomorphic inverse functions

This file supplies global-on-the-image forms of the holomorphic inverse function theorem for functions that are injective on an open set and for holomorphic open partial homeomorphisms.

Main results

• DifferentiableOn.invFunOn — the inverse of a holomorphic injection on an open set is holomorphic on its image.
• TauCeti.hasDerivAt_invFunOn — the derivative of the inverse at f z₀ is (deriv f z₀)⁻¹, via HasDerivAt.of_local_left_inverse.
• TauCeti.hasDerivAt_invFunOn_comp_segment — the chain rule for the inverse along an affine segment through the image of z₀.
• TauCeti.OpenPartialHomeomorph.differentiableOn_symm — the inverse of a holomorphic open partial homeomorphism is holomorphic on its target.

theorem DifferentiableOn.invFunOn {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : DifferentiableOn ℂ (Function.invFunOn f U) (f '' U)

The inverse of a holomorphic injection on an open set is holomorphic on its image.

The inverse is Function.invFunOn f U, which chooses the unique preimage lying in U. No global injectivity of f outside U is required.

theorem TauCeti.OpenPartialHomeomorph.differentiableOn_symm {e : OpenPartialHomeomorph ℂ ℂ} (he : DifferentiableOn ℂ (↑e) e.source) : DifferentiableOn ℂ (↑e.symm) e.target

The inverse of a holomorphic open partial homeomorphism of ℂ is holomorphic on its target.

theorem TauCeti.hasDerivAt_invFunOn {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) {z₀ : ℂ} (hz₀ : z₀ ∈ U) : HasDerivAt (Function.invFunOn f U) (deriv f z₀)⁻¹ (f z₀)

The derivative of the holomorphic inverse. At f z₀, the inverse Function.invFunOn f U of a holomorphic injection f of the open set U has derivative (deriv f z₀)⁻¹, by HasDerivAt.of_local_left_inverse applied to the right-inverse relation f (invFunOn f U w) = w on the open image f '' U.

theorem TauCeti.hasDerivAt_invFunOn_comp_segment {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) {z₀ : ℂ} (hz₀ : z₀ ∈ U) (n : ℂ) : HasDerivAt (fun (t : ℝ) => Function.invFunOn f U (deriv f z₀ * n * ↑t + f z₀)) n 0

The chain rule for invFunOn along a segment. Specialization of hasDerivAt_comp_segment_of_hasDerivAt_inv to the canonical inverse.