# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1572705094 0
# Node ID 5b753486c075578c90c78c79639f6854c1bf34e8
# Parent  38ade730f6dfdd127e02eafb7eb8a4f2dca47ed4
Inverse function theorem + lemmas

diff -r 38ade730f6df -r 5b753486c075 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -216,6 +216,8 @@
 
 lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left
 
+declare blinfun.zero_left [simp] blinfun.zero_right [simp]
+
 
 context bounded_bilinear
 begin
@@ -682,6 +684,28 @@
   "blinfun_compose x 0 = 0"
   by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
 
+lemma blinfun_bij2:
+  fixes f::"'a \<Rightarrow>\<^sub>L 'a::euclidean_space"
+  assumes "f o\<^sub>L g = id_blinfun"
+  shows "bij (blinfun_apply g)"
+proof (rule bijI)
+  show "inj g"
+    using assms
+    by (metis blinfun_apply_id_blinfun blinfun_compose.rep_eq injI inj_on_imageI2)
+  then show "surj g"
+    using blinfun.bounded_linear_right bounded_linear_def linear_inj_imp_surj by blast
+qed
+
+lemma blinfun_bij1:
+  fixes f::"'a \<Rightarrow>\<^sub>L 'a::euclidean_space"
+  assumes "f o\<^sub>L g = id_blinfun"
+  shows "bij (blinfun_apply f)"
+proof (rule bijI)
+  show "surj (blinfun_apply f)"
+    by (metis assms blinfun_apply_blinfun_compose blinfun_apply_id_blinfun surjI)
+  then show "inj (blinfun_apply f)"
+    using blinfun.bounded_linear_right bounded_linear_def linear_surj_imp_inj by blast
+qed
 
 lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "(\<bullet>)"
   by (rule bounded_linear_inner_right)
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -1267,23 +1267,55 @@
 
 lemma
   assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
-    shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
-      and Im_Ln_less_pi:           "Im (Ln z) < pi"
+  shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
+    and Im_Ln_less_pi:           "Im (Ln z) < pi"
 proof -
-  have znz: "z \<noteq> 0"
+  have znz [simp]: "z \<noteq> 0"
     using assms by auto
   then have "Im (Ln z) \<noteq> pi"
     by (metis (no_types) Im_exp Ln_in_Reals assms complex_nonpos_Reals_iff complex_is_Real_iff exp_Ln mult_zero_right not_less pi_neq_zero sin_pi znz)
   then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
-    by (simp add: le_neq_trans znz)
-  have "(exp has_field_derivative z) (at (Ln z))"
-    by (metis znz DERIV_exp exp_Ln)
-  then show "(Ln has_field_derivative inverse(z)) (at z)"
-    apply (rule has_field_derivative_inverse_strong_x
-              [where S = "{w. -pi < Im(w) \<and> Im(w) < pi}"])
-    using znz *
-    apply (auto simp: continuous_on_exp [OF continuous_on_id] open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt mpi_less_Im_Ln)
-    done
+    by (simp add: le_neq_trans)
+  let ?U = "{w. -pi < Im(w) \<and> Im(w) < pi}"
+  have 1: "open ?U"
+    by (simp add: open_Collect_conj open_halfspace_Im_gt open_halfspace_Im_lt)
+  have 2: "\<And>x. x \<in> ?U \<Longrightarrow> (exp has_derivative blinfun_apply(Blinfun ((*) (exp x)))) (at x)"
+    apply (simp add: bounded_linear_Blinfun_apply bounded_linear_mult_right)
+    using DERIV_exp has_field_derivative_def by blast
+  have 3: "continuous_on ?U (\<lambda>x. Blinfun ((*) (exp x)))"
+    unfolding blinfun_mult_right.abs_eq [symmetric] by (intro continuous_intros)
+  have 4: "Ln z \<in> ?U"
+    by (auto simp: mpi_less_Im_Ln *)
+  have 5: "Blinfun ((*) (inverse z)) o\<^sub>L Blinfun ((*) (exp (Ln z))) = id_blinfun"
+    by (rule blinfun_eqI) (simp add: bounded_linear_mult_right bounded_linear_Blinfun_apply)
+  obtain U' V g g' where "open U'" and sub: "U' \<subseteq> ?U"
+    and "Ln z \<in> U'" "open V" "z \<in> V"
+    and hom: "homeomorphism U' V exp g"
+    and g: "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)"
+    and g': "\<And>y. y \<in> V \<Longrightarrow> g' y = inv ((*) (exp (g y)))"
+    and bij: "\<And>y. y \<in> V \<Longrightarrow> bij ((*) (exp (g y)))"
+    using inverse_function_theorem [OF 1 2 3 4 5]
+    by (simp add: bounded_linear_Blinfun_apply bounded_linear_mult_right) blast
+  show "(Ln has_field_derivative inverse(z)) (at z)"
+    unfolding has_field_derivative_def
+  proof (rule has_derivative_transform_within_open)
+    show g_eq_Ln: "g y = Ln y" if "y \<in> V" for y
+    proof -
+      obtain x where "y = exp x" "x \<in> U'"
+        using hom homeomorphism_image1 that \<open>y \<in> V\<close> by blast
+      then show ?thesis
+        using sub hom homeomorphism_apply1 by fastforce
+    qed
+    have "0 \<notin> V"
+      by (meson exp_not_eq_zero hom homeomorphism_def)
+    then have "\<And>y. y \<in> V \<Longrightarrow> g' y = inv ((*) y)"
+      by (metis exp_Ln g' g_eq_Ln)
+    then have g': "g' z = (\<lambda>x. x/z)"
+      by (metis (no_types, hide_lams) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
+    show "(g has_derivative (*) (inverse z)) (at z)"
+      using g [OF \<open>z \<in> V\<close>] g'
+      by (simp add: \<open>z \<in> V\<close> field_class.field_divide_inverse has_derivative_imp_has_field_derivative has_field_derivative_imp_has_derivative)
+  qed (auto simp: \<open>z \<in> V\<close> \<open>open V\<close>)
 qed
 
 declare has_field_derivative_Ln [derivative_intros]
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -57,11 +57,6 @@
   unfolding has_derivative_within' has_derivative_at'
   by blast
 
-lemma has_derivative_within_open:
-  "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
-    (f has_derivative f') (at a within S) \<longleftrightarrow> (f has_derivative f') (at a)"
-  by (simp only: at_within_interior interior_open)
-
 lemma has_derivative_right:
   fixes f :: "real \<Rightarrow> real"
     and y :: "real"
@@ -913,8 +908,7 @@
     have "(f \<circ> ?p has_derivative (f' ?u) \<circ> (\<lambda>u. 0 + u *\<^sub>R (y - x))) (at u within box 0 1)"
       by (intro derivative_intros has_derivative_within_subset [OF derf]) (use u * in auto)
     hence "((f \<circ> ?p) has_vector_derivative f' ?u (y - x)) (at u)"
-      by (simp add: has_derivative_within_open[OF u open_greaterThanLessThan]
-        scaleR has_vector_derivative_def o_def)
+      by (simp add: at_within_open[OF u open_greaterThanLessThan] scaleR has_vector_derivative_def o_def)
   } note 2 = this
   have 3: "continuous_on {0..1} ?\<phi>"
     by (rule continuous_intros)+
@@ -2553,4 +2547,354 @@
   subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
   by (auto simp: assms)
 
+subsection\<^marker>\<open>tag important\<close>\<open>The Inverse Function Theorem\<close>
+
+lemma linear_injective_contraction:
+  assumes "linear f" "c < 1" and le: "\<And>x. norm (f x - x) \<le> c * norm x"
+  shows "inj f"
+  unfolding linear_injective_0[OF \<open>linear f\<close>]
+proof safe
+  fix x
+  assume "f x = 0"
+  with le [of x] have "norm x \<le> c * norm x"
+    by simp
+  then show "x = 0"
+    using \<open>c < 1\<close> by (simp add: mult_le_cancel_right1)
+qed
+
+text\<open>From an online proof by J. Michael Boardman, Department of Mathematics, Johns Hopkins University\<close>
+lemma inverse_function_theorem_scaled:
+  fixes f::"'a::euclidean_space \<Rightarrow> 'a"
+    and f'::"'a \<Rightarrow> ('a \<Rightarrow>\<^sub>L 'a)"
+  assumes "open U"
+    and derf: "\<And>x. x \<in> U \<Longrightarrow> (f has_derivative blinfun_apply (f' x)) (at x)"
+    and contf: "continuous_on U f'"
+    and "0 \<in> U" and [simp]: "f 0 = 0"
+    and id: "f' 0 = id_blinfun"
+  obtains U' V g g' where "open U'" "U' \<subseteq> U" "0 \<in> U'" "open V" "0 \<in> V" "homeomorphism U' V f g"
+                "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)"
+                "\<And>y. y \<in> V \<Longrightarrow> g' y = inv (blinfun_apply (f'(g y)))"
+                "\<And>y. y \<in> V \<Longrightarrow> bij (blinfun_apply (f'(g y)))"
+proof -
+  obtain d1 where "cball 0 d1 \<subseteq> U" "d1 > 0"
+    using \<open>open U\<close> \<open>0 \<in> U\<close> open_contains_cball by blast
+  obtain d2 where d2: "\<And>x. \<lbrakk>x \<in> U; dist x 0 \<le> d2\<rbrakk> \<Longrightarrow> dist (f' x) (f' 0) < 1/2" "0 < d2"
+    using continuous_onE [OF contf, of 0 "1/2"] by (metis \<open>0 \<in> U\<close> half_gt_zero_iff zero_less_one)
+  obtain \<delta> where le: "\<And>x. norm x \<le> \<delta> \<Longrightarrow> dist (f' x) id_blinfun \<le> 1/2" and "0 < \<delta>"
+    and subU: "cball 0 \<delta> \<subseteq> U"
+  proof
+    show "min d1 d2 > 0"
+      by (simp add: \<open>0 < d1\<close> \<open>0 < d2\<close>)
+    show "cball 0 (min d1 d2) \<subseteq> U"
+      using \<open>cball 0 d1 \<subseteq> U\<close> by auto
+    show "dist (f' x) id_blinfun \<le> 1/2" if "norm x \<le> min d1 d2" for x
+      using \<open>cball 0 d1 \<subseteq> U\<close> d2 that id by fastforce
+  qed
+  let ?D = "cball 0 \<delta>"
+  define V:: "'a set" where "V \<equiv> ball 0 (\<delta>/2)"
+  have 4: "norm (f (x + h) - f x - h) \<le> 1/2 * norm h"
+    if "x \<in> ?D" "x+h \<in> ?D" for x h
+  proof -
+    let ?w = "\<lambda>x. f x - x"
+    have B: "\<And>x. x \<in> ?D \<Longrightarrow> onorm (blinfun_apply (f' x - id_blinfun)) \<le> 1/2"
+      by (metis dist_norm le mem_cball_0 norm_blinfun.rep_eq)
+    have "\<And>x. x \<in> ?D \<Longrightarrow> (?w has_derivative (blinfun_apply (f' x - id_blinfun))) (at x)"
+      by (rule derivative_eq_intros derf subsetD [OF subU] | force simp: blinfun.diff_left)+
+    then have Dw: "\<And>x. x \<in> ?D \<Longrightarrow> (?w has_derivative (blinfun_apply (f' x - id_blinfun))) (at x within ?D)"
+      using has_derivative_at_withinI by blast
+    have "norm (?w (x+h) - ?w x) \<le> (1/2) * norm h"
+      using differentiable_bound [OF convex_cball Dw B] that by fastforce
+    then show ?thesis
+      by (auto simp: algebra_simps)
+  qed
+  have for_g: "\<exists>!x. norm x < \<delta> \<and> f x = y" if y: "norm y < \<delta>/2" for y
+  proof -
+    let ?u = "\<lambda>x. x + (y - f x)"
+    have *: "norm (?u x) < \<delta>" if "x \<in> ?D" for x
+    proof -
+      have fxx: "norm (f x - x) \<le> \<delta>/2"
+        using 4 [of 0 x] \<open>0 < \<delta>\<close> \<open>f 0 = 0\<close> that by auto
+      have "norm (?u x) \<le> norm y + norm (f x - x)"
+        by (metis add.commute add_diff_eq norm_minus_commute norm_triangle_ineq)
+      also have "\<dots> < \<delta>/2 + \<delta>/2"
+        using fxx y by auto
+      finally show ?thesis
+        by simp
+    qed
+    have "\<exists>!x \<in> ?D. ?u x = x"
+    proof (rule banach_fix)
+      show "cball 0 \<delta> \<noteq> {}"
+        using \<open>0 < \<delta>\<close> by auto
+      show "(\<lambda>x. x + (y - f x)) ` cball 0 \<delta> \<subseteq> cball 0 \<delta>"
+        using * by force
+      have "dist (x + (y - f x)) (xh + (y - f xh)) * 2 \<le> dist x xh"
+        if "norm x \<le> \<delta>" and "norm xh \<le> \<delta>" for x xh
+        using that 4 [of x "xh-x"] by (auto simp: dist_norm norm_minus_commute algebra_simps)
+      then show "\<forall>x\<in>cball 0 \<delta>. \<forall>ya\<in>cball 0 \<delta>. dist (x + (y - f x)) (ya + (y - f ya)) \<le> (1/2) * dist x ya"
+        by auto
+    qed (auto simp: complete_eq_closed)
+    then show ?thesis
+      by (metis "*" add_cancel_right_right eq_iff_diff_eq_0 le_less mem_cball_0)
+  qed
+  define g where "g \<equiv> \<lambda>y. THE x. norm x < \<delta> \<and> f x = y"
+  have g: "norm (g y) < \<delta> \<and> f (g y) = y" if "norm y < \<delta>/2" for y
+    unfolding g_def using that theI' [OF for_g] by meson
+  then have fg[simp]: "f (g y) = y" if "y \<in> V" for y
+    using that by (auto simp: V_def)
+  have 5: "norm (g y' - g y) \<le> 2 * norm (y' - y)" if "y \<in> V" "y' \<in> V" for y y'
+  proof -
+    have no: "norm (g y) \<le> \<delta>" "norm (g y') \<le> \<delta>" and [simp]: "f (g y) = y"
+      using that g unfolding V_def by force+
+    have "norm (g y' - g y) \<le> norm (g y' - g y - (y' - y)) + norm (y' - y)"
+      by (simp add: add.commute norm_triangle_sub)
+    also have "\<dots> \<le> (1/2) * norm (g y' - g y) + norm (y' - y)"
+      using 4 [of "g y" "g y' - g y"] that no by (simp add: g norm_minus_commute V_def)
+    finally show ?thesis
+      by auto
+  qed
+  have contg: "continuous_on V g"
+  proof
+    fix y::'a and e::real
+    assume "0 < e" and y: "y \<in> V"
+    show "\<exists>d>0. \<forall>x'\<in>V. dist x' y < d \<longrightarrow> dist (g x') (g y) \<le> e"
+    proof (intro exI conjI ballI impI)
+      show "0 < e/2"
+        by (simp add: \<open>0 < e\<close>)
+    qed (use 5 y in \<open>force simp: dist_norm\<close>)
+  qed
+  show thesis
+  proof
+    define U' where "U' \<equiv> (f -` V) \<inter> ball 0 \<delta>"
+    have contf: "continuous_on U f"
+      using derf has_derivative_at_withinI by (fast intro: has_derivative_continuous_on)
+    then have "continuous_on (ball 0 \<delta>) f"
+      by (meson ball_subset_cball continuous_on_subset subU)
+    then show "open U'"
+      by (simp add: U'_def V_def Int_commute continuous_open_preimage)
+    show "0 \<in> U'" "U' \<subseteq> U" "open V" "0 \<in> V"
+      using \<open>0 < \<delta>\<close> subU by (auto simp: U'_def V_def)
+    show hom: "homeomorphism U' V f g"
+    proof
+      show "continuous_on U' f"
+        using \<open>U' \<subseteq> U\<close> contf continuous_on_subset by blast
+      show "continuous_on V g"
+        using contg by blast
+      show "f ` U' \<subseteq> V"
+        using U'_def by blast
+      show "g ` V \<subseteq> U'"
+        by (simp add: U'_def V_def g image_subset_iff)
+      show "g (f x) = x" if "x \<in> U'" for x
+        by (metis that fg Int_iff U'_def V_def for_g g mem_ball_0 vimage_eq)
+      show "f (g y) = y" if "y \<in> V" for y
+        using that by (simp add: g V_def)
+    qed
+    show bij: "bij (blinfun_apply (f'(g y)))" if "y \<in> V" for y
+    proof -
+      have inj: "inj (blinfun_apply (f' (g y)))"
+      proof (rule linear_injective_contraction)
+        show "linear (blinfun_apply (f' (g y)))"
+          using blinfun.bounded_linear_right bounded_linear_def by blast
+      next
+        fix x
+        have "norm (blinfun_apply (f' (g y)) x - x) = norm (blinfun_apply (f' (g y) - id_blinfun) x)"
+          by (simp add: blinfun.diff_left)
+        also have "\<dots> \<le> norm (f' (g y) - id_blinfun) * norm x"
+          by (rule norm_blinfun)
+        also have "\<dots> \<le> (1/2) * norm x"
+        proof (rule mult_right_mono)
+          show "norm (f' (g y) - id_blinfun) \<le> 1/2"
+            using that g [of y] le by (auto simp: V_def dist_norm)
+        qed auto
+        finally show "norm (blinfun_apply (f' (g y)) x - x) \<le> (1/2) * norm x" .
+      qed auto
+      moreover
+      have "surj (blinfun_apply (f' (g y)))"
+        using blinfun.bounded_linear_right bounded_linear_def
+        by (blast intro!: linear_inj_imp_surj [OF _ inj])
+      ultimately show ?thesis
+        using bijI by blast
+    qed
+    define g' where "g' \<equiv> \<lambda>y. inv (blinfun_apply (f'(g y)))"
+    show "(g has_derivative g' y) (at y)" if "y \<in> V" for y
+    proof -
+      have gy: "g y \<in> U"
+        using g subU that unfolding V_def by fastforce
+      obtain e where e: "\<And>h. f (g y + h) = y + blinfun_apply (f' (g y)) h + e h"
+        and e0: "(\<lambda>h. norm (e h) / norm h) \<midarrow>0\<rightarrow> 0"
+        using iffD1 [OF has_derivative_iff_Ex derf [OF gy]] \<open>y \<in> V\<close> by auto
+      have [simp]: "e 0 = 0"
+        using e [of 0] that by simp
+      let ?INV = "inv (blinfun_apply (f' (g y)))"
+      have inj: "inj (blinfun_apply (f' (g y)))"
+        using bij bij_betw_def that by blast
+      have "(g has_derivative g' y) (at y within V)"
+        unfolding has_derivative_at_within_iff_Ex [OF \<open>y \<in> V\<close> \<open>open V\<close>]
+      proof
+        show blinv: "bounded_linear (g' y)"
+          unfolding g'_def using derf gy inj inj_linear_imp_inv_bounded_linear by blast
+        define eg where "eg \<equiv> \<lambda>k. - ?INV (e (g (y+k) - g y))"
+        have "g (y+k) = g y + g' y k + eg k" if "y + k \<in> V" for k
+        proof -
+          have "?INV k = ?INV (blinfun_apply (f' (g y)) (g (y+k) - g y) + e (g (y+k) - g y))"
+            using e [of "g(y+k) - g y"] that by simp
+          then have "g (y+k) = g y + ?INV k - ?INV (e (g (y+k) - g y))"
+            using inj blinv by (simp add: linear_simps g'_def)
+          then show ?thesis
+            by (auto simp: eg_def g'_def)
+        qed
+        moreover have "(\<lambda>k. norm (eg k) / norm k) \<midarrow>0\<rightarrow> 0"
+        proof (rule Lim_null_comparison)
+          let ?g = "\<lambda>k. 2 * onorm ?INV * norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)"
+          show "\<forall>\<^sub>F k in at 0. norm (norm (eg k) / norm k) \<le> ?g k"
+            unfolding eventually_at_topological
+          proof (intro exI conjI ballI impI)
+            show "open ((+)(-y) ` V)"
+              using \<open>open V\<close> open_translation by blast
+            show "0 \<in> (+)(-y) ` V"
+              by (simp add: that)
+            show "norm (norm (eg k) / norm k) \<le> 2 * onorm (inv (blinfun_apply (f' (g y)))) * norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)"
+              if "k \<in> (+)(-y) ` V" "k \<noteq> 0" for k
+            proof -
+              have "y+k \<in> V"
+                using that by auto
+              have "norm (norm (eg k) / norm k) \<le> onorm ?INV * norm (e (g (y+k) - g y)) / norm k"
+                using blinv g'_def onorm by (force simp: eg_def divide_simps)
+              also have "\<dots> = (norm (g (y+k) - g y) / norm k) * (onorm ?INV * (norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)))"
+                by (simp add: divide_simps)
+              also have "\<dots> \<le> 2 * (onorm ?INV * (norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)))"
+                apply (rule mult_right_mono)
+                using 5 [of y "y+k"] \<open>y \<in> V\<close> \<open>y + k \<in> V\<close>  onorm_pos_le [OF blinv]
+                 apply (auto simp: divide_simps zero_le_mult_iff zero_le_divide_iff g'_def)
+                done
+              finally show "norm (norm (eg k) / norm k) \<le> 2 * onorm ?INV * norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)"
+                by simp
+            qed
+          qed
+          have 1: "(\<lambda>h. norm (e h) / norm h) \<midarrow>0\<rightarrow> (norm (e 0) / norm 0)"
+            using e0 by auto
+          have 2: "(\<lambda>k. g (y+k) - g y) \<midarrow>0\<rightarrow> 0"
+            using contg \<open>open V\<close> \<open>y \<in> V\<close> LIM_offset_zero_iff LIM_zero_iff at_within_open continuous_on_def by fastforce
+          from tendsto_compose [OF 1 2, simplified]
+          have "(\<lambda>k. norm (e (g (y+k) - g y)) / norm (g (y+k) - g y)) \<midarrow>0\<rightarrow> 0" .
+          from tendsto_mult_left [OF this] show "?g \<midarrow>0\<rightarrow> 0" by auto
+        qed
+        ultimately show "\<exists>e. (\<forall>k. y + k \<in> V \<longrightarrow> g (y+k) = g y + g' y k + e k) \<and> (\<lambda>k. norm (e k) / norm k) \<midarrow>0\<rightarrow> 0"
+          by blast
+      qed
+      then show ?thesis
+        by (metis \<open>open V\<close> at_within_open that)
+    qed
+    show "g' y = inv (blinfun_apply (f' (g y)))"
+      if "y \<in> V" for y
+      by (simp add: g'_def)
+  qed
+qed
+
+
+text\<open>We need all this to justify the scaling and translations.\<close>
+theorem inverse_function_theorem:
+  fixes f::"'a::euclidean_space \<Rightarrow> 'a"
+    and f'::"'a \<Rightarrow> ('a \<Rightarrow>\<^sub>L 'a)"
+  assumes "open U"
+    and derf: "\<And>x. x \<in> U \<Longrightarrow> (f has_derivative (blinfun_apply (f' x))) (at x)"
+    and contf:  "continuous_on U f'"
+    and "x0 \<in> U"
+    and invf: "invf o\<^sub>L f' x0 = id_blinfun"
+  obtains U' V g g' where "open U'" "U' \<subseteq> U" "x0 \<in> U'" "open V" "f x0 \<in> V" "homeomorphism U' V f g"
+    "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)"
+    "\<And>y. y \<in> V \<Longrightarrow> g' y = inv (blinfun_apply (f'(g y)))"
+    "\<And>y. y \<in> V \<Longrightarrow> bij (blinfun_apply (f'(g y)))"
+proof -
+  have apply1 [simp]: "\<And>i. blinfun_apply invf (blinfun_apply (f' x0) i) = i"
+    by (metis blinfun_apply_blinfun_compose blinfun_apply_id_blinfun invf)
+  have apply2 [simp]: "\<And>i. blinfun_apply (f' x0) (blinfun_apply invf i) = i"
+    by (metis apply1 bij_inv_eq_iff blinfun_bij1 invf)
+  have [simp]: "(range (blinfun_apply invf)) = UNIV"
+    using apply1 surjI by blast
+  let ?f = "invf \<circ> (\<lambda>x. (f \<circ> (+)x0)x - f x0)"
+  let ?f' = "\<lambda>x. invf o\<^sub>L (f' (x + x0))"
+  obtain U' V g g' where "open U'" and U': "U' \<subseteq> (+)(-x0) ` U" "0 \<in> U'"
+    and "open V" "0 \<in> V" and hom: "homeomorphism U' V ?f g"
+    and derg: "\<And>y. y \<in> V \<Longrightarrow> (g has_derivative (g' y)) (at y)"
+    and g': "\<And>y. y \<in> V \<Longrightarrow> g' y = inv (?f'(g y))"
+    and bij: "\<And>y. y \<in> V \<Longrightarrow> bij (?f'(g y))"
+  proof (rule inverse_function_theorem_scaled [of "(+)(-x0) ` U" ?f "?f'"])
+    show ope: "open ((+) (- x0) ` U)"
+      using \<open>open U\<close> open_translation by blast
+    show "(?f has_derivative blinfun_apply (?f' x)) (at x)"
+      if "x \<in> (+) (- x0) ` U" for x
+      using that
+      apply clarify
+      apply (rule derf derivative_eq_intros | simp add: blinfun_compose.rep_eq)+
+      done
+    have YY: "(\<lambda>x. f' (x + x0)) \<midarrow>u-x0\<rightarrow> f' u"
+      if "f' \<midarrow>u\<rightarrow> f' u" "u \<in> U" for u
+      using that LIM_offset [where k = x0] by (auto simp: algebra_simps)
+    then have "continuous_on ((+) (- x0) ` U) (\<lambda>x. f' (x + x0))"
+      using contf \<open>open U\<close> Lim_at_imp_Lim_at_within
+      by (fastforce simp: continuous_on_def at_within_open_NO_MATCH ope)
+    then show "continuous_on ((+) (- x0) ` U) ?f'"
+      by (intro continuous_intros) simp
+  qed (auto simp: invf \<open>x0 \<in> U\<close>)
+  show thesis
+  proof
+    let ?U' = "(+)x0 ` U'"
+    let ?V = "((+)(f x0) \<circ> f' x0) ` V"
+    let ?g = "(+)x0 \<circ> g \<circ> invf \<circ> (+)(- f x0)"
+    let ?g' = "\<lambda>y. inv (blinfun_apply (f' (?g y)))"
+    show oU': "open ?U'"
+      by (simp add: \<open>open U'\<close> open_translation)
+    show subU: "?U' \<subseteq> U"
+      using ComplI \<open>U' \<subseteq> (+) (- x0) ` U\<close> by auto
+    show "x0 \<in> ?U'"
+      by (simp add: \<open>0 \<in> U'\<close>)
+    show "open ?V"
+      using blinfun_bij2 [OF invf]
+      by (metis \<open>open V\<close> bij_is_surj blinfun.bounded_linear_right bounded_linear_def image_comp open_surjective_linear_image open_translation)
+    show "f x0 \<in> ?V"
+      using \<open>0 \<in> V\<close> image_iff by fastforce
+    show "homeomorphism ?U' ?V f ?g"
+    proof
+      show "continuous_on ?U' f"
+        by (meson subU continuous_on_eq_continuous_at derf has_derivative_continuous oU' subsetD)
+      have "?f ` U' \<subseteq> V"
+        using hom homeomorphism_image1 by blast
+      then show "f ` ?U' \<subseteq> ?V"
+        unfolding image_subset_iff
+        by (clarsimp simp: image_def) (metis apply2 add.commute diff_add_cancel)
+      show "?g ` ?V \<subseteq> ?U'"
+        using hom invf by (auto simp: image_def homeomorphism_def)
+      show "?g (f x) = x"
+        if "x \<in> ?U'" for x
+        using that hom homeomorphism_apply1 by fastforce
+      have "continuous_on V g"
+        using hom homeomorphism_def by blast
+      then show "continuous_on ?V ?g"
+        by (intro continuous_intros) (auto elim!: continuous_on_subset)
+      have fg: "?f (g x) = x" if "x \<in> V" for x
+        using hom homeomorphism_apply2 that by blast
+      show "f (?g y) = y"
+        if "y \<in> ?V" for y
+        using that fg by (simp add: image_iff) (metis apply2 add.commute diff_add_cancel)
+    qed
+    show "(?g has_derivative ?g' y) (at y)" "bij (blinfun_apply (f' (?g y)))"
+      if "y \<in> ?V" for y
+    proof -
+      have 1: "bij (blinfun_apply invf)"
+        using blinfun_bij1 invf by blast
+      then have 2: "bij (blinfun_apply (f' (x0 + g x)))" if "x \<in> V" for x
+        by (metis add.commute bij bij_betw_comp_iff2 blinfun_compose.rep_eq that top_greatest)
+      then show "bij (blinfun_apply (f' (?g y)))"
+        using that by auto
+      have "g' x \<circ> blinfun_apply invf = inv (blinfun_apply (f' (x0 + g x)))"
+        if "x \<in> V" for x
+        using that
+        by (simp add: g' o_inv_distrib blinfun_compose.rep_eq 1 2 add.commute bij_is_inj flip: o_assoc)
+      then show "(?g has_derivative ?g' y) (at y)"
+        using that invf
+        by clarsimp (rule derg derivative_eq_intros | simp flip: id_def)+
+    qed
+  qed auto
+qed
+
 end
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -1192,10 +1192,16 @@
     by (metis assms continuous_open_vimage vimage_def)
 qed
 
+lemma open_translation_subtract:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "open S"
+  shows "open ((\<lambda>x. x - a) ` S)" 
+  using assms open_translation [of S "- a"] by (simp cong: image_cong_simp)
+
 lemma open_neg_translation:
-  fixes s :: "'a::real_normed_vector set"
-  assumes "open s"
-  shows "open((\<lambda>x. a - x) ` s)"
+  fixes S :: "'a::real_normed_vector set"
+  assumes "open S"
+  shows "open((\<lambda>x. a - x) ` S)"
   using open_translation[OF open_negations[OF assms], of a]
   by (auto simp: image_image)
 
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -4405,7 +4405,7 @@
       by (rule continuous_on_subset[OF contf])
     show "(f has_vector_derivative 0) (at z)" if z: "z \<in> {a<..<x}" and notin: "z \<notin> k" for z
       unfolding has_vector_derivative_def
-    proof (simp add: has_derivative_within_open[OF z, symmetric])
+    proof (simp add: at_within_open[OF z, symmetric])
       show "(f has_derivative (\<lambda>x. 0)) (at z within {a<..<x})"
         by (rule has_derivative_within_subset [OF fder]) (use x z notin in auto)
     qed
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -646,6 +646,11 @@
 
 lemmas linear_linear = linear_conv_bounded_linear[symmetric]
 
+lemma inj_linear_imp_inv_bounded_linear:
+  fixes f::"'a::euclidean_space \<Rightarrow> 'a"
+  shows "\<lbrakk>bounded_linear f; inj f\<rbrakk> \<Longrightarrow> bounded_linear (inv f)"
+  by (simp add: inj_linear_imp_inv_linear linear_linear)
+
 lemma linear_bounded_pos:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes lf: "linear f"
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Deriv.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -169,6 +169,40 @@
   finally show ?thesis .
 qed
 
+lemma has_derivative_iff_Ex:
+  "(f has_derivative f') (at x) \<longleftrightarrow>
+    bounded_linear f' \<and> (\<exists>e. (\<forall>h. f (x+h) = f x + f' h + e h) \<and> ((\<lambda>h. norm (e h) / norm h) \<longlongrightarrow> 0) (at 0))"
+  unfolding has_derivative_at by force
+
+lemma has_derivative_at_within_iff_Ex:
+  assumes "x \<in> S" "open S"
+  shows "(f has_derivative f') (at x within S) \<longleftrightarrow>
+         bounded_linear f' \<and> (\<exists>e. (\<forall>h. x+h \<in> S \<longrightarrow> f (x+h) = f x + f' h + e h) \<and> ((\<lambda>h. norm (e h) / norm h) \<longlongrightarrow> 0) (at 0))"
+    (is "?lhs = ?rhs")
+proof safe
+  show "bounded_linear f'"
+    if "(f has_derivative f') (at x within S)"
+    using has_derivative_bounded_linear that by blast
+  show "\<exists>e. (\<forall>h. x + h \<in> S \<longrightarrow> f (x + h) = f x + f' h + e h) \<and> (\<lambda>h. norm (e h) / norm h) \<midarrow>0\<rightarrow> 0"
+    if "(f has_derivative f') (at x within S)"
+    by (metis (full_types) assms that has_derivative_iff_Ex at_within_open)
+  show "(f has_derivative f') (at x within S)"
+    if "bounded_linear f'"
+      and eq [rule_format]: "\<forall>h. x + h \<in> S \<longrightarrow> f (x + h) = f x + f' h + e h"
+      and 0: "(\<lambda>h. norm (e (h::'a)::'b) / norm h) \<midarrow>0\<rightarrow> 0"
+    for e 
+  proof -
+    have 1: "f y - f x = f' (y-x) + e (y-x)" if "y \<in> S" for y
+      using eq [of "y-x"] that by simp
+    have 2: "((\<lambda>y. norm (e (y-x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
+      by (simp add: "0" assms tendsto_offset_zero_iff)
+    have "((\<lambda>y. norm (f y - f x - f' (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
+      by (simp add: Lim_cong_within 1 2)
+    then show ?thesis
+      by (simp add: has_derivative_iff_norm \<open>bounded_linear f'\<close>)
+  qed
+qed
+
 lemma has_derivativeI:
   "bounded_linear f' \<Longrightarrow>
     ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s) \<Longrightarrow>
diff -r 38ade730f6df -r 5b753486c075 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Limits.thy	Sat Nov 02 14:31:34 2019 +0000
@@ -703,7 +703,7 @@
 
 subsubsection \<open>Linear operators and multiplication\<close>
 
-lemma linear_times: "linear (\<lambda>x. c * x)"
+lemma linear_times [simp]: "linear (\<lambda>x. c * x)"
   for c :: "'a::real_algebra"
   by (auto simp: linearI distrib_left)
 
@@ -2472,6 +2472,12 @@
   for f :: "'a :: real_normed_vector \<Rightarrow> _"
   using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
 
+lemma tendsto_offset_zero_iff:
+  fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
+  assumes "a \<in> S" "open S"
+  shows "(f \<longlongrightarrow> L) (at a within S) \<longleftrightarrow> ((\<lambda>h. f (a + h)) \<longlongrightarrow> L) (at 0)"
+  by (metis LIM_offset_zero_iff assms tendsto_within_open)
+
 lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
   for f :: "'a \<Rightarrow> 'b::real_normed_vector"
   unfolding tendsto_iff dist_norm by simp