--- 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)
--- 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]
--- 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
--- 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)
--- 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
--- 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"
--- 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>
--- 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