theorem linear_inverse_of_bijective_linear_map {n : ℕ} (T : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ) (hT : Function.Bijective ⇑T) : ∃ (Tinv : (Fin n → ℝ) →ₗ[ℝ] Fin n → ℝ), (∀ (x : Fin n → ℝ), Tinv (T x) = x) ∧ ∀ (y : Fin n → ℝ), T (Tinv y) = y

Lemma 6.8: if T : ℝ^n → ℝ^n is a bijective linear transformation, then its inverse map is also linear.

theorem helperForTheorem_6_9_hasDerivAt_f_at_x0 (f : ℝ → ℝ) (I : Set ℝ) (x0 : ℝ) (hI_open : IsOpen I) (hx0 : x0 ∈ I) (hdiff : DifferentiableOn ℝ f I) : HasDerivAt f (deriv f x0) x0

Helper for Theorem 6.9: obtain HasDerivAt f (deriv f x0) x0 from differentiability of f on an open set containing x0.

theorem helperForTheorem_6_9_eventually_right_inverse_near_y0 (f g : ℝ → ℝ) (J : Set ℝ) (x0 : ℝ) (hJ_open : IsOpen J) (hy0 : f x0 ∈ J) (hright : Set.RightInvOn g f J) : ∀ᶠ (y : ℝ) in nhds (f x0), f (g y) = y

Helper for Theorem 6.9: f (g y) = y holds in a neighborhood of f x0 because it holds on the open interval J containing f x0.

theorem helperForTheorem_6_9_localIntervalWithinIAndPreimageJ (f : ℝ → ℝ) (I J : Set ℝ) (x0 : ℝ) (hI_open : IsOpen I) (hx0 : x0 ∈ I) (hJ_open : IsOpen J) (hy0 : f x0 ∈ J) (hdiff : DifferentiableOn ℝ f I) : ∃ (p : ℝ) (q : ℝ), p < x0 ∧ x0 < q ∧ Set.Icc p q ⊆ I ∧ Set.MapsTo f (Set.Icc p q) J

Helper for Theorem 6.9: choose a closed interval around x0 contained in I, and mapped by f into J.

theorem helperForTheorem_6_9_strictOrderOnLocalInterval (f : ℝ → ℝ) (I : Set ℝ) (p q : ℝ) (hpq : p ≤ q) (hinj : Set.InjOn f I) (hIcc_subset_I : Set.Icc p q ⊆ I) (hdiff : DifferentiableOn ℝ f I) : StrictMonoOn f (Set.Icc p q) ∨ StrictAntiOn f (Set.Icc p q)

Helper for Theorem 6.9: on the local closed interval, injective continuous f is either strictly increasing or strictly decreasing.

theorem helperForTheorem_6_9_localImageNeighborhoodAt_y0 (f : ℝ → ℝ) (p q x0 : ℝ) (hpx0 : p < x0) (hx0q : x0 < q) (hcontIcc : ContinuousOn f (Set.Icc p q)) (horder : StrictMonoOn f (Set.Icc p q) ∨ StrictAntiOn f (Set.Icc p q)) : f '' Set.Icc p q ∈ nhds (f x0)

Helper for Theorem 6.9: the local image f '' Icc p q is a neighborhood of f x0.

theorem helperForTheorem_6_9_orderBehaviorOf_g_on_localImage (f g : ℝ → ℝ) (I J : Set ℝ) (x0 p q : ℝ) (hpx0 : p < x0) (hx0q : x0 < q) (hIcc_subset_I : Set.Icc p q ⊆ I) (hMaps_f : Set.MapsTo f (Set.Icc p q) J) (hleft : ∀ ⦃x : ℝ⦄, x ∈ I → f x ∈ J → g (f x) = x) (hright : Set.RightInvOn g f J) (horder : StrictMonoOn f (Set.Icc p q) ∨ StrictAntiOn f (Set.Icc p q)) : (MonotoneOn g (f '' Set.Icc p q) ∨ AntitoneOn g (f '' Set.Icc p q)) ∧ g '' (f '' Set.Icc p q) ∈ nhds x0

Helper for Theorem 6.9: order behavior of g on the local image, together with the neighborhood property of g '' (f '' Icc p q).

theorem helperForTheorem_6_9_continuousAt_g_at_y0 (f g : ℝ → ℝ) (I J : Set ℝ) (x0 : ℝ) (hinj : Set.InjOn f I) (hI_open : IsOpen I) (hI_interval : Convex ℝ I) (hx0 : x0 ∈ I) (hdiff : DifferentiableOn ℝ f I) (hJ_open : IsOpen J) (hy0 : f x0 ∈ J) (hMapsInv : Set.MapsTo g J I) (hleft : ∀ ⦃x : ℝ⦄, x ∈ I → f x ∈ J → g (f x) = x) (hright : Set.RightInvOn g f J) : ContinuousAt g (f x0)

Helper for Theorem 6.9: continuity of the inverse branch g at f x0.

theorem helperForTheorem_6_9_hasDerivAt_g_at_y0 (f g : ℝ → ℝ) (I J : Set ℝ) (x0 : ℝ) (hinj : Set.InjOn f I) (hI_open : IsOpen I) (hI_interval : Convex ℝ I) (hx0 : x0 ∈ I) (hdiff : DifferentiableOn ℝ f I) (hderiv_ne : deriv f x0 ≠ 0) (hJ_open : IsOpen J) (hy0 : f x0 ∈ J) (hMapsInv : Set.MapsTo g J I) (hleft : ∀ ⦃x : ℝ⦄, x ∈ I → f x ∈ J → g (f x) = x) (hright : Set.RightInvOn g f J) : HasDerivAt g (deriv f x0)⁻¹ (f x0)

Helper for Theorem 6.9: derivative of the inverse branch at y0 = f x0.

theorem inverse_function_theorem_one_variable_6_9 (f g : ℝ → ℝ) (I J : Set ℝ) (x0 : ℝ) (hinj : Set.InjOn f I) (hI_open : IsOpen I) (hI_interval : Convex ℝ I) (hx0 : x0 ∈ I) (hdiff : DifferentiableOn ℝ f I) (hderiv_ne : deriv f x0 ≠ 0) (hJ_open : IsOpen J) (hJ_interval : Convex ℝ J) (hy0 : f x0 ∈ J) (hMapsInv : Set.MapsTo g J I) (hleft : ∀ ⦃x : ℝ⦄, x ∈ I → f x ∈ J → g (f x) = x) (hright : Set.RightInvOn g f J) : DifferentiableAt ℝ g (f x0) ∧ deriv g (f x0) = 1 / deriv f x0

Theorem 6.9 (Inverse function theorem in one variable): let f : ℝ → ℝ be injective and differentiable on an open interval I, let x₀ ∈ I and set y₀ = f x₀. Assume deriv f x₀ ≠ 0, and suppose g is the inverse of f on an open interval J containing y₀ (so g (f x) = x for x ∈ I and f (g y) = y for y ∈ J). Then g is differentiable at y₀ and deriv g y₀ = 1 / deriv f x₀.

def LocallyInvertibleNear (f : ℝ → ℝ) (x0 : ℝ) : Prop

Definition 6.15 (Local invertibility): a function f : ℝ → ℝ is locally invertible near x₀ if there exist open intervals (a, b) and (c, d) with x₀ ∈ (a, b) and f x₀ ∈ (c, d) such that the restriction f|(a,b) : (a,b) → (c,d) is a bijection.

Equations

• LocallyInvertibleNear f x0 = ∃ (a : ℝ) (b : ℝ) (c : ℝ) (d : ℝ), a < x0 ∧ x0 < b ∧ c < f x0 ∧ f x0 < d ∧ Set.BijOn f (Set.Ioo a b) (Set.Ioo c d)

theorem inverse_function_theorem_several_variables_6_10 {n : ℕ} {E : Set (Fin n → ℝ)} {f : (Fin n → ℝ) → Fin n → ℝ} {x0 : Fin n → ℝ} (hE_open : IsOpen E) (hcont : ContDiffOn ℝ 1 f E) (hx0 : x0 ∈ E) (f0 : (Fin n → ℝ) ≃L[ℝ] Fin n → ℝ) (hderiv : fderiv ℝ f x0 = ↑f0) : ∃ (U : Set (Fin n → ℝ)) (V : Set (Fin n → ℝ)), IsOpen U ∧ IsOpen V ∧ x0 ∈ U ∧ U ⊆ E ∧ f x0 ∈ V ∧ Set.BijOn f U V ∧ ∃ (g : (Fin n → ℝ) → Fin n → ℝ), Set.MapsTo g V U ∧ Set.LeftInvOn g f U ∧ Set.RightInvOn g f V ∧ DifferentiableAt ℝ g (f x0) ∧ fderiv ℝ g (f x0) = ↑f0.symm

Theorem 6.10 (Inverse Function Theorem): let E ⊆ ℝ^n be open and let f : E → ℝ^n be continuously differentiable on E. If x₀ ∈ E and f'(x₀) is invertible (encoded by fderiv ℝ f x₀ = f₀ for a linear equivalence f₀), then there exist open sets U ⊆ E and V ⊆ ℝ^n with x₀ ∈ U and f x₀ ∈ V such that f restricts to a bijection U → V with inverse g : V → U. Moreover, g is differentiable at y₀ = f x₀ and fderiv ℝ g y₀ = (f'(x₀))⁻¹.