theorem inverse_derivative_at {I J : Set ℝ} {f : ℝ → ℝ} {x0 f'x0 : ℝ} (hI : I.OrdConnected) (hJ : J.OrdConnected) (hmono : StrictMonoOn f I) (hmap : Set.MapsTo f I J) (hsurj : Set.SurjOn f I J) (hx0 : x0 ∈ I) (hdiff : HasDerivWithinAt f f'x0 I x0) (hzero : f'x0 ≠ 0) : HasDerivWithinAt (fun (y : ℝ) => Function.invFunOn f I y) f'x0⁻¹ J (f x0)

Lemma 4.4.1: If I, J ⊆ ℝ are intervals and f : ℝ → ℝ is strictly monotone on I, maps I onto J, is differentiable at x₀ ∈ I, and f' x₀ ≠ 0, then the inverse satisfies (f ⁻¹)' (f x₀) = 1 / f' x₀. If moreover f is continuously differentiable with derivative never zero on I, then the inverse is continuously differentiable on J.

theorem inverse_contDiff_on {I J : Set ℝ} {f : ℝ → ℝ} (hI : I.OrdConnected) (hJ : J.OrdConnected) (hmono : StrictMonoOn f I) (hmap : Set.MapsTo f I J) (hsurj : Set.SurjOn f I J) (hcont : ContDiffOn ℝ 1 f I) (hzero : ∀ x ∈ I, derivWithin f I x ≠ 0) : ContDiffOn ℝ 1 (fun (y : ℝ) => Function.invFunOn f I y) J

Lemma 4.4.1 (smoothness of the inverse): If f : ℝ → ℝ is continuously C¹, strictly monotone on an interval I, maps I onto another interval J, and derivWithin f I x ≠ 0 for every x ∈ I, then the inverse function is continuously differentiable on J.

theorem exists_Ioo_subset_of_mem {a b x₀ : ℝ} (hx₀ : x₀ ∈ Set.Ioo a b) : ∃ δ > 0, Set.Ioo (x₀ - δ) (x₀ + δ) ⊆ Set.Ioo a b

If x₀ ∈ (a, b) then there is a small open interval around x₀ contained in (a, b).

theorem inverse_function_open_interval {a b x0 : ℝ} (f : ℝ → ℝ) (hx0 : x0 ∈ Set.Ioo a b) (hcont : ContDiffOn ℝ 1 f (Set.Ioo a b)) (hderiv : derivWithin f (Set.Ioo a b) x0 ≠ 0) : ∃ (I : Set ℝ) (J : Set ℝ), IsOpen I ∧ x0 ∈ I ∧ I ⊆ Set.Ioo a b ∧ J = f '' I ∧ Set.InjOn f I ∧ Set.SurjOn f I J ∧ ∃ (g : ℝ → ℝ), Set.MapsTo g J I ∧ Set.SurjOn g J I ∧ (∀ x ∈ I, g (f x) = x) ∧ (∀ y ∈ J, f (g y) = y) ∧ ContDiffOn ℝ 1 g J ∧ ∀ y ∈ J, derivWithin g J y = (derivWithin f (Set.Ioo a b) (g y))⁻¹

Theorem 4.4.2 (inverse function theorem). Given a continuously C¹ function f : ℝ → ℝ on (a, b) with derivWithin f (Set.Ioo a b) x₀ ≠ 0 at some x₀ ∈ (a, b), there exists an open interval I ⊆ (a, b) containing x₀ such that f restricts to an injective map on I with a continuously differentiable inverse g : J → I on J = f '' I, and for every y ∈ J we have derivWithin g J y = (derivWithin f (Set.Ioo a b) (g y))⁻¹.

theorem nth_root_exists_unique_and_deriv (n : ℕ) (hn : 0 < n) (x : ℝ) (hx : 0 ≤ x) : (∃! y : ℝ, 0 ≤ y ∧ y ^ n = x) ∧ ∃ (g : ℝ → ℝ), (g = fun (t : ℝ) => t ^ (1 / ↑n)) ∧ ContDiffOn ℝ 1 g (Set.Ioi 0) ∧ ∀ t ∈ Set.Ioi 0, derivWithin g (Set.Ioi 0) t = 1 / ↑n * t ^ ((1 - ↑n) / ↑n)

Corollary 4.4.3: For n ∈ ℕ and x ≥ 0 there is a unique y ≥ 0 with y ^ n = x. The function g x = x^{1/n} on (0, ∞) is continuously differentiable with derivative g' x = (1 / n) * x ^ ((1 - n) / n), where fractional powers use the convention x ^ (m / n) = (x ^ (1 / n)) ^ m.

theorem inverse_function_example_square {x0 : ℝ} (hx0 : 0 < x0) : derivWithin (fun (x : ℝ) => x ^ 2) (Set.Ioi 0) x0 ≠ 0 ∧ Set.InjOn (fun (x : ℝ) => x ^ 2) (Set.Ioi 0) ∧ ∀ (I : Set ℝ), IsOpen I → I.OrdConnected → x0 ∈ I → Set.InjOn (fun (x : ℝ) => x ^ 2) I → I ⊆ Set.Ioi 0

Example 4.4.4: For f x = x^2, the derivative at x₀ ≠ 0 is nonzero. At a positive point x₀, the inverse function theorem applies on the maximal open interval (0, ∞) where f is injective; any open set on which f is injective and contains x₀ must lie in (0, ∞).

theorem cube_inverse_not_differentiable_at_zero : (ContDiff ℝ 1 fun (x : ℝ) => x ^ 3) ∧ (StrictMono fun (x : ℝ) => x ^ 3) ∧ (Function.Surjective fun (x : ℝ) => x ^ 3) ∧ deriv (fun (x : ℝ) => x ^ 3) 0 = 0 ∧ ∃ (g : ℝ → ℝ), (Function.LeftInverse g fun (x : ℝ) => x ^ 3) ∧ (Function.RightInverse g fun (x : ℝ) => x ^ 3) ∧ ¬DifferentiableAt ℝ g 0

Example 4.4.5: The cubic f x = x^3 : ℝ → ℝ is bijective with a continuous derivative, so it has a set-theoretic inverse g y = y^{1/3} on all of ℝ. Nevertheless the inverse fails to be differentiable at 0 because f' 0 = 0, and the graph of the cube root has a vertical tangent at the origin.