--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Mon Mar 07 14:34:45 2016 +0000
@@ -2678,6 +2678,7 @@
(** Existence of a primitive.*)
lemma holomorphic_starlike_primitive:
+ fixes f :: "complex \<Rightarrow> complex"
assumes contf: "continuous_on s f"
and s: "starlike s" and os: "open s"
and k: "finite k"
@@ -2796,6 +2797,8 @@
done
lemma holomorphic_convex_primitive:
+ fixes f :: "complex \<Rightarrow> complex"
+ shows
"\<lbrakk>convex s; finite k; continuous_on s f;
\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
\<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Mon Mar 07 14:34:45 2016 +0000
@@ -277,11 +277,14 @@
subsection\<open>Holomorphic functions\<close>
-text\<open>Could be generalized to real normed fields, but in practice that would only include the reals\<close>
-definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
+definition complex_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
(infixr "(complex'_differentiable)" 50)
where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
+lemma complex_differentiable_derivI:
+ "f complex_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
+by (simp add: complex_differentiable_def DERIV_deriv_iff_has_field_derivative)
+
lemma complex_differentiable_imp_continuous_at:
"f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
by (metis DERIV_continuous complex_differentiable_def)
@@ -297,24 +300,24 @@
unfolding complex_differentiable_def
by (metis DERIV_subset top_greatest)
-lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F"
+lemma complex_differentiable_linear [simp,derivative_intros]: "(op * c) complex_differentiable F"
proof -
show ?thesis
unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
by (force intro: has_derivative_mult_right)
qed
-lemma complex_differentiable_const [derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
+lemma complex_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
unfolding complex_differentiable_def has_field_derivative_def
by (rule exI [where x=0])
(metis has_derivative_const lambda_zero)
-lemma complex_differentiable_ident [derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
+lemma complex_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
unfolding complex_differentiable_def has_field_derivative_def
by (rule exI [where x=1])
(simp add: lambda_one [symmetric])
-lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F"
+lemma complex_differentiable_id [simp,derivative_intros]: "id complex_differentiable F"
unfolding id_def by (rule complex_differentiable_ident)
lemma complex_differentiable_minus [derivative_intros]:
@@ -328,6 +331,10 @@
using assms unfolding complex_differentiable_def
by (metis field_differentiable_add)
+lemma complex_differentiable_add_const [simp,derivative_intros]:
+ "op + c complex_differentiable F"
+ by (simp add: complex_differentiable_add)
+
lemma complex_differentiable_setsum [derivative_intros]:
"(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
by (induct I rule: infinite_finite_induct)
@@ -503,6 +510,11 @@
"DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
+lemma holomorphic_derivI:
+ "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
+ \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
+by (metis DERIV_deriv_iff_complex_differentiable at_within_open holomorphic_on_def has_field_derivative_at_within)
+
lemma complex_derivative_chain:
"f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
\<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
@@ -568,6 +580,20 @@
apply (simp add: algebra_simps)
done
+lemma nonzero_deriv_nonconstant:
+ assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
+ shows "\<not> f constant_on S"
+unfolding constant_on_def
+by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique)
+
+lemma holomorphic_nonconstant:
+ assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0"
+ shows "\<not> f constant_on S"
+ apply (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
+ using assms
+ apply (auto simp: holomorphic_derivI)
+ done
+
subsection\<open>Analyticity on a set\<close>
definition analytic_on (infixl "(analytic'_on)" 50)
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Mar 07 14:34:45 2016 +0000
@@ -1633,13 +1633,15 @@
done
lemma complex_differentiable_powr_right:
+ fixes w::complex
+ shows
"w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
using complex_differentiable_def has_field_derivative_powr_right by blast
lemma holomorphic_on_powr_right:
"f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
- unfolding holomorphic_on_def
- using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
+ unfolding holomorphic_on_def complex_differentiable_def
+by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
lemma norm_powr_real_powr:
"w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Mon Mar 07 14:34:45 2016 +0000
@@ -1722,4 +1722,412 @@
done
qed
+subsection\<open>Bloch's theorem\<close>
+
+lemma Bloch_lemma_0:
+ assumes holf: "f holomorphic_on cball 0 r" and "0 < r"
+ and [simp]: "f 0 = 0"
+ and le: "\<And>z. norm z < r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f 0)"
+ shows "ball 0 ((3 - 2 * sqrt 2) * r * norm(deriv f 0)) \<subseteq> f ` ball 0 r"
+proof -
+ have "sqrt 2 < 3/2"
+ by (rule real_less_lsqrt) (auto simp: power2_eq_square)
+ then have sq3: "0 < 3 - 2 * sqrt 2" by simp
+ show ?thesis
+ proof (cases "deriv f 0 = 0")
+ case True then show ?thesis by simp
+ next
+ case False
+ def C \<equiv> "2 * norm(deriv f 0)"
+ have "0 < C" using False by (simp add: C_def)
+ have holf': "f holomorphic_on ball 0 r" using holf
+ using ball_subset_cball holomorphic_on_subset by blast
+ then have holdf': "deriv f holomorphic_on ball 0 r"
+ by (rule holomorphic_deriv [OF _ open_ball])
+ have "Le1": "norm(deriv f z - deriv f 0) \<le> norm z / (r - norm z) * C"
+ if "norm z < r" for z
+ proof -
+ have T1: "norm(deriv f z - deriv f 0) \<le> norm z / (R - norm z) * C"
+ if R: "norm z < R" "R < r" for R
+ proof -
+ have "0 < R" using R
+ by (metis less_trans norm_zero zero_less_norm_iff)
+ have df_le: "\<And>x. norm x < r \<Longrightarrow> norm (deriv f x) \<le> C"
+ using le by (simp add: C_def)
+ have hol_df: "deriv f holomorphic_on cball 0 R"
+ apply (rule holomorphic_on_subset) using R holdf' by auto
+ have *: "((\<lambda>w. deriv f w / (w - z)) has_contour_integral 2 * pi * \<i> * deriv f z) (circlepath 0 R)"
+ if "norm z < R" for z
+ using \<open>0 < R\<close> that Cauchy_integral_formula_convex_simple [OF convex_cball hol_df, of _ "circlepath 0 R"]
+ by (force simp: winding_number_circlepath)
+ have **: "((\<lambda>x. deriv f x / (x - z) - deriv f x / x) has_contour_integral
+ of_real (2 * pi) * \<i> * (deriv f z - deriv f 0))
+ (circlepath 0 R)"
+ using has_contour_integral_diff [OF * [of z] * [of 0]] \<open>0 < R\<close> that
+ by (simp add: algebra_simps)
+ have [simp]: "\<And>x. norm x = R \<Longrightarrow> x \<noteq> z" using that(1) by blast
+ have "norm (deriv f x / (x - z) - deriv f x / x)
+ \<le> C * norm z / (R * (R - norm z))"
+ if "norm x = R" for x
+ proof -
+ have [simp]: "norm (deriv f x * x - deriv f x * (x - z)) =
+ norm (deriv f x) * norm z"
+ by (simp add: norm_mult right_diff_distrib')
+ show ?thesis
+ using \<open>0 < R\<close> \<open>0 < C\<close> R that
+ apply (simp add: norm_mult norm_divide divide_simps)
+ using df_le norm_triangle_ineq2 \<open>0 < C\<close> apply (auto intro!: mult_mono)
+ done
+ qed
+ then show ?thesis
+ using has_contour_integral_bound_circlepath
+ [OF **, of "C * norm z/(R*(R - norm z))"]
+ \<open>0 < R\<close> \<open>0 < C\<close> R
+ apply (simp add: norm_mult norm_divide)
+ apply (simp add: divide_simps mult.commute)
+ done
+ qed
+ obtain r' where r': "norm z < r'" "r' < r"
+ using Rats_dense_in_real [of "norm z" r] \<open>norm z < r\<close> by blast
+ then have [simp]: "closure {r'<..<r} = {r'..r}" by simp
+ show ?thesis
+ apply (rule continuous_ge_on_closure
+ [where f = "\<lambda>r. norm z / (r - norm z) * C" and s = "{r'<..<r}",
+ OF _ _ T1])
+ apply (intro continuous_intros)
+ using that r'
+ apply (auto simp: not_le)
+ done
+ qed
+ have "*": "(norm z - norm z^2/(r - norm z)) * norm(deriv f 0) \<le> norm(f z)"
+ if r: "norm z < r" for z
+ proof -
+ have 1: "\<And>x. x \<in> ball 0 r \<Longrightarrow>
+ ((\<lambda>z. f z - deriv f 0 * z) has_field_derivative deriv f x - deriv f 0)
+ (at x within ball 0 r)"
+ by (rule derivative_eq_intros holomorphic_derivI holf' | simp)+
+ have 2: "closed_segment 0 z \<subseteq> ball 0 r"
+ by (metis \<open>0 < r\<close> convex_ball convex_contains_segment dist_self mem_ball mem_ball_0 that)
+ have 3: "(\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C) integrable_on {0..1}"
+ apply (rule integrable_on_cmult_right [where 'b=real, simplified])
+ apply (rule integrable_on_cdivide [where 'b=real, simplified])
+ apply (rule integrable_on_cmult_left [where 'b=real, simplified])
+ apply (rule ident_integrable_on)
+ done
+ have 4: "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm z * norm z * x * C / (r - norm z)"
+ if x: "0 \<le> x" "x \<le> 1" for x
+ proof -
+ have [simp]: "x * norm z < r"
+ using r x by (meson le_less_trans mult_le_cancel_right2 norm_not_less_zero)
+ have "norm (deriv f (x *\<^sub>R z) - deriv f 0) \<le> norm (x *\<^sub>R z) / (r - norm (x *\<^sub>R z)) * C"
+ apply (rule Le1) using r x \<open>0 < r\<close> by simp
+ also have "... \<le> norm (x *\<^sub>R z) / (r - norm z) * C"
+ using r x \<open>0 < r\<close>
+ apply (simp add: divide_simps)
+ by (simp add: \<open>0 < C\<close> mult.assoc mult_left_le_one_le ordered_comm_semiring_class.comm_mult_left_mono)
+ finally have "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm (x *\<^sub>R z) / (r - norm z) * C * norm z"
+ by (rule mult_right_mono) simp
+ with x show ?thesis by (simp add: algebra_simps)
+ qed
+ have le_norm: "abc \<le> norm d - e \<Longrightarrow> norm(f - d) \<le> e \<Longrightarrow> abc \<le> norm f" for abc d e and f::complex
+ by (metis add_diff_cancel_left' add_diff_eq diff_left_mono norm_diff_ineq order_trans)
+ have "norm (integral {0..1} (\<lambda>x. (deriv f (x *\<^sub>R z) - deriv f 0) * z))
+ \<le> integral {0..1} (\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C)"
+ apply (rule integral_norm_bound_integral)
+ using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
+ apply (simp add: has_contour_integral_linepath has_integral_integrable_integral)
+ apply (rule 3)
+ apply (simp add: norm_mult power2_eq_square 4)
+ done
+ then have int_le: "norm (f z - deriv f 0 * z) \<le> (norm z)\<^sup>2 * norm(deriv f 0) / ((r - norm z))"
+ using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
+ apply (simp add: has_contour_integral_linepath has_integral_integrable_integral C_def)
+ done
+ show ?thesis
+ apply (rule le_norm [OF _ int_le])
+ using \<open>norm z < r\<close>
+ apply (simp add: power2_eq_square divide_simps C_def norm_mult)
+ proof -
+ have "norm z * (norm (deriv f 0) * (r - norm z - norm z)) \<le> norm z * (norm (deriv f 0) * (r - norm z) - norm (deriv f 0) * norm z)"
+ by (simp add: linordered_field_class.sign_simps(38))
+ then show "(norm z * (r - norm z) - norm z * norm z) * norm (deriv f 0) \<le> norm (deriv f 0) * norm z * (r - norm z) - norm z * norm z * norm (deriv f 0)"
+ by (simp add: linordered_field_class.sign_simps(38) mult.commute mult.left_commute)
+ qed
+ qed
+ have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2) < 1"
+ by (auto simp: sqrt2_less_2)
+ have 1: "continuous_on (closure (ball 0 ((1 - sqrt 2 / 2) * r))) f"
+ apply (rule continuous_on_subset [OF holomorphic_on_imp_continuous_on [OF holf]])
+ apply (subst closure_ball)
+ using \<open>0 < r\<close> mult_pos_pos sq201
+ apply (auto simp: cball_subset_cball_iff)
+ done
+ have 2: "open (f ` interior (ball 0 ((1 - sqrt 2 / 2) * r)))"
+ apply (rule open_mapping_thm [OF holf' open_ball connected_ball], force)
+ using \<open>0 < r\<close> mult_pos_pos sq201 apply (simp add: ball_subset_ball_iff)
+ using False \<open>0 < r\<close> centre_in_ball holf' holomorphic_nonconstant by blast
+ have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv f 0)) =
+ ball (f 0) ((3 - 2 * sqrt 2) * r * norm (deriv f 0))"
+ by simp
+ also have "... \<subseteq> f ` ball 0 ((1 - sqrt 2 / 2) * r)"
+ proof -
+ have 3: "(3 - 2 * sqrt 2) * r * norm (deriv f 0) \<le> norm (f z)"
+ if "norm z = (1 - sqrt 2 / 2) * r" for z
+ apply (rule order_trans [OF _ *])
+ using \<open>0 < r\<close>
+ apply (simp_all add: field_simps power2_eq_square that)
+ apply (simp add: mult.assoc [symmetric])
+ done
+ show ?thesis
+ apply (rule ball_subset_open_map_image [OF 1 2 _ bounded_ball])
+ using \<open>0 < r\<close> sq201 3 apply simp_all
+ using C_def \<open>0 < C\<close> sq3 apply force
+ done
+ qed
+ also have "... \<subseteq> f ` ball 0 r"
+ apply (rule image_subsetI [OF imageI], simp)
+ apply (erule less_le_trans)
+ using \<open>0 < r\<close> apply (auto simp: field_simps)
+ done
+ finally show ?thesis .
+ qed
+qed
+
+lemma Bloch_lemma:
+ assumes holf: "f holomorphic_on cball a r" and "0 < r"
+ and le: "\<And>z. z \<in> ball a r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f a)"
+ shows "ball (f a) ((3 - 2 * sqrt 2) * r * norm(deriv f a)) \<subseteq> f ` ball a r"
+proof -
+ have fz: "(\<lambda>z. f (a + z)) = f o (\<lambda>z. (a + z))"
+ by (simp add: o_def)
+ have hol0: "(\<lambda>z. f (a + z)) holomorphic_on cball 0 r"
+ unfolding fz by (intro holomorphic_intros holf holomorphic_on_compose | simp)+
+ then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) complex_differentiable at x"
+ by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball diff_0 dist_norm holomorphic_on_def holomorphic_on_subset mem_ball norm_minus_cancel)
+ have [simp]: "\<And>z. norm z < r \<Longrightarrow> f complex_differentiable at (a + z)"
+ by (metis holf open_ball add_diff_cancel_left' dist_complex_def holomorphic_on_imp_differentiable_at holomorphic_on_subset interior_cball interior_subset mem_ball norm_minus_commute)
+ then have [simp]: "f complex_differentiable at a"
+ by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
+ have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
+ by (intro holomorphic_intros hol0)
+ then have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv (\<lambda>z. f (a + z) - f a) 0))
+ \<subseteq> (\<lambda>z. f (a + z) - f a) ` ball 0 r"
+ apply (rule Bloch_lemma_0)
+ apply (simp_all add: \<open>0 < r\<close>)
+ apply (simp add: fz complex_derivative_chain)
+ apply (simp add: dist_norm le)
+ done
+ then show ?thesis
+ apply clarify
+ apply (drule_tac c="x - f a" in subsetD)
+ apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain complex_differentiable_compose)+
+ done
+qed
+
+proposition Bloch_unit:
+ assumes holf: "f holomorphic_on ball a 1" and [simp]: "deriv f a = 1"
+ obtains b r where "1/12 < r" "ball b r \<subseteq> f ` (ball a 1)"
+proof -
+ def r \<equiv> "249/256::real"
+ have "0 < r" "r < 1" by (auto simp: r_def)
+ def g \<equiv> "\<lambda>z. deriv f z * of_real(r - norm(z - a))"
+ have "deriv f holomorphic_on ball a 1"
+ by (rule holomorphic_deriv [OF holf open_ball])
+ then have "continuous_on (ball a 1) (deriv f)"
+ using holomorphic_on_imp_continuous_on by blast
+ then have "continuous_on (cball a r) (deriv f)"
+ by (rule continuous_on_subset) (simp add: cball_subset_ball_iff \<open>r < 1\<close>)
+ then have "continuous_on (cball a r) g"
+ by (simp add: g_def continuous_intros)
+ then have 1: "compact (g ` cball a r)"
+ by (rule compact_continuous_image [OF _ compact_cball])
+ have 2: "g ` cball a r \<noteq> {}"
+ using \<open>r > 0\<close> by auto
+ obtain p where pr: "p \<in> cball a r"
+ and pge: "\<And>y. y \<in> cball a r \<Longrightarrow> norm (g y) \<le> norm (g p)"
+ using distance_attains_sup [OF 1 2, of 0] by force
+ def t \<equiv> "(r - norm(p - a)) / 2"
+ have "norm (p - a) \<noteq> r"
+ using pge [of a] \<open>r > 0\<close> by (auto simp: g_def norm_mult)
+ then have "norm (p - a) < r" using pr
+ by (simp add: norm_minus_commute dist_norm)
+ then have "0 < t"
+ by (simp add: t_def)
+ have cpt: "cball p t \<subseteq> ball a r"
+ using \<open>0 < t\<close> by (simp add: cball_subset_ball_iff dist_norm t_def field_simps)
+ have gen_le_dfp: "norm (deriv f y) * (r - norm (y - a)) / (r - norm (p - a)) \<le> norm (deriv f p)"
+ if "y \<in> cball a r" for y
+ proof -
+ have [simp]: "norm (y - a) \<le> r"
+ using that by (simp add: dist_norm norm_minus_commute)
+ have "norm (g y) \<le> norm (g p)"
+ using pge [OF that] by simp
+ then have "norm (deriv f y) * abs (r - norm (y - a)) \<le> norm (deriv f p) * abs (r - norm (p - a))"
+ by (simp only: dist_norm g_def norm_mult norm_of_real)
+ with that \<open>norm (p - a) < r\<close> show ?thesis
+ by (simp add: dist_norm divide_simps)
+ qed
+ have le_norm_dfp: "r / (r - norm (p - a)) \<le> norm (deriv f p)"
+ using gen_le_dfp [of a] \<open>r > 0\<close> by auto
+ have 1: "f holomorphic_on cball p t"
+ apply (rule holomorphic_on_subset [OF holf])
+ using cpt \<open>r < 1\<close> order_subst1 subset_ball by auto
+ have 2: "norm (deriv f z) \<le> 2 * norm (deriv f p)" if "z \<in> ball p t" for z
+ proof -
+ have z: "z \<in> cball a r"
+ by (meson ball_subset_cball subsetD cpt that)
+ then have "norm(z - a) < r"
+ by (metis ball_subset_cball contra_subsetD cpt dist_norm mem_ball norm_minus_commute that)
+ have "norm (deriv f z) * (r - norm (z - a)) / (r - norm (p - a)) \<le> norm (deriv f p)"
+ using gen_le_dfp [OF z] by simp
+ with \<open>norm (z - a) < r\<close> \<open>norm (p - a) < r\<close>
+ have "norm (deriv f z) \<le> (r - norm (p - a)) / (r - norm (z - a)) * norm (deriv f p)"
+ by (simp add: field_simps)
+ also have "... \<le> 2 * norm (deriv f p)"
+ apply (rule mult_right_mono)
+ using that \<open>norm (p - a) < r\<close> \<open>norm(z - a) < r\<close>
+ apply (simp_all add: field_simps t_def dist_norm [symmetric])
+ using dist_triangle3 [of z a p] by linarith
+ finally show ?thesis .
+ qed
+ have sqrt2: "sqrt 2 < 2113/1494"
+ by (rule real_less_lsqrt) (auto simp: power2_eq_square)
+ then have sq3: "0 < 3 - 2 * sqrt 2" by simp
+ have "1 / 12 / ((3 - 2 * sqrt 2) / 2) < r"
+ using sq3 sqrt2 by (auto simp: field_simps r_def)
+ also have "... \<le> cmod (deriv f p) * (r - cmod (p - a))"
+ using \<open>norm (p - a) < r\<close> le_norm_dfp by (simp add: pos_divide_le_eq)
+ finally have "1 / 12 < cmod (deriv f p) * (r - cmod (p - a)) * ((3 - 2 * sqrt 2) / 2)"
+ using pos_divide_less_eq half_gt_zero_iff sq3 by blast
+ then have **: "1 / 12 < (3 - 2 * sqrt 2) * t * norm (deriv f p)"
+ using sq3 by (simp add: mult.commute t_def)
+ have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball p t"
+ by (rule Bloch_lemma [OF 1 \<open>0 < t\<close> 2])
+ also have "... \<subseteq> f ` ball a 1"
+ apply (rule image_mono)
+ apply (rule order_trans [OF ball_subset_cball])
+ apply (rule order_trans [OF cpt])
+ using \<open>0 < t\<close> \<open>r < 1\<close> apply (simp add: ball_subset_ball_iff dist_norm)
+ done
+ finally have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball a 1" .
+ with ** show ?thesis
+ by (rule that)
+qed
+
+
+theorem Bloch:
+ assumes holf: "f holomorphic_on ball a r" and "0 < r"
+ and r': "r' \<le> r * norm (deriv f a) / 12"
+ obtains b where "ball b r' \<subseteq> f ` (ball a r)"
+proof (cases "deriv f a = 0")
+ case True with r' show ?thesis
+ using ball_eq_empty that by fastforce
+next
+ case False
+ def C \<equiv> "deriv f a"
+ have "0 < norm C" using False by (simp add: C_def)
+ have dfa: "f complex_differentiable at a"
+ apply (rule holomorphic_on_imp_differentiable_at [OF holf])
+ using \<open>0 < r\<close> by auto
+ have fo: "(\<lambda>z. f (a + of_real r * z)) = f o (\<lambda>z. (a + of_real r * z))"
+ by (simp add: o_def)
+ have holf': "f holomorphic_on (\<lambda>z. a + complex_of_real r * z) ` ball 0 1"
+ apply (rule holomorphic_on_subset [OF holf])
+ using \<open>0 < r\<close> apply (force simp: dist_norm norm_mult)
+ done
+ have 1: "(\<lambda>z. f (a + r * z) / (C * r)) holomorphic_on ball 0 1"
+ apply (rule holomorphic_intros holomorphic_on_compose holf' | simp add: fo)+
+ using \<open>0 < r\<close> by (simp add: C_def False)
+ have "((\<lambda>z. f (a + of_real r * z) / (C * of_real r)) has_field_derivative
+ (deriv f (a + of_real r * z) / C)) (at z)"
+ if "norm z < 1" for z
+ proof -
+ have *: "((\<lambda>x. f (a + of_real r * x)) has_field_derivative
+ (deriv f (a + of_real r * z) * of_real r)) (at z)"
+ apply (simp add: fo)
+ apply (rule DERIV_chain [OF complex_differentiable_derivI])
+ apply (rule holomorphic_on_imp_differentiable_at [OF holf], simp)
+ using \<open>0 < r\<close> apply (simp add: dist_norm norm_mult that)
+ apply (rule derivative_eq_intros | simp)+
+ done
+ show ?thesis
+ apply (rule derivative_eq_intros * | simp)+
+ using \<open>0 < r\<close> by (auto simp: C_def False)
+ qed
+ have 2: "deriv (\<lambda>z. f (a + of_real r * z) / (C * of_real r)) 0 = 1"
+ apply (subst complex_derivative_cdivide_right)
+ apply (simp add: complex_differentiable_def fo)
+ apply (rule exI)
+ apply (rule DERIV_chain [OF complex_differentiable_derivI])
+ apply (simp add: dfa)
+ apply (rule derivative_eq_intros | simp add: C_def False fo)+
+ using \<open>0 < r\<close>
+ apply (simp add: C_def False fo)
+ apply (simp add: derivative_intros dfa complex_derivative_chain)
+ done
+ have sb1: "op * (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
+ \<subseteq> f ` ball a r"
+ using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
+ have sb2: "ball (C * r * b) r' \<subseteq> op * (C * r) ` ball b t"
+ if "1 / 12 < t" for b t
+ proof -
+ have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
+ using that \<open>0 < r\<close> less_eq_real_def mult.commute mult.right_neutral mult_left_mono norm_ge_zero times_divide_eq_right
+ by auto
+ show ?thesis
+ apply clarify
+ apply (rule_tac x="x / (C * r)" in image_eqI)
+ using \<open>0 < r\<close>
+ apply (simp_all add: dist_norm norm_mult norm_divide C_def False field_simps)
+ apply (erule less_le_trans)
+ apply (rule order_trans [OF r' *])
+ done
+ qed
+ show ?thesis
+ apply (rule Bloch_unit [OF 1 2])
+ apply (rename_tac t)
+ apply (rule_tac b="(C * of_real r) * b" in that)
+ apply (drule image_mono [where f = "\<lambda>z. (C * of_real r) * z"])
+ using sb1 sb2
+ apply force
+ done
+qed
+
+corollary Bloch_general:
+ assumes holf: "f holomorphic_on s" and "a \<in> s"
+ and tle: "\<And>z. z \<in> frontier s \<Longrightarrow> t \<le> dist a z"
+ and rle: "r \<le> t * norm(deriv f a) / 12"
+ obtains b where "ball b r \<subseteq> f ` s"
+proof -
+ consider "r \<le> 0" | "0 < t * norm(deriv f a) / 12" using rle by force
+ then show ?thesis
+ proof cases
+ case 1 then show ?thesis
+ by (simp add: Topology_Euclidean_Space.ball_empty that)
+ next
+ case 2
+ show ?thesis
+ proof (cases "deriv f a = 0")
+ case True then show ?thesis
+ using rle by (simp add: Topology_Euclidean_Space.ball_empty that)
+ next
+ case False
+ then have "t > 0"
+ using 2 by (force simp: zero_less_mult_iff)
+ have "~ ball a t \<subseteq> s \<Longrightarrow> ball a t \<inter> frontier s \<noteq> {}"
+ apply (rule connected_Int_frontier [of "ball a t" s], simp_all)
+ using \<open>0 < t\<close> \<open>a \<in> s\<close> centre_in_ball apply blast
+ done
+ with tle have *: "ball a t \<subseteq> s" by fastforce
+ then have 1: "f holomorphic_on ball a t"
+ using holf using holomorphic_on_subset by blast
+ show ?thesis
+ apply (rule Bloch [OF 1 \<open>t > 0\<close> rle])
+ apply (rule_tac b=b in that)
+ using * apply force
+ done
+ qed
+ qed
+qed
+
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Mar 07 14:34:45 2016 +0000
@@ -5277,7 +5277,7 @@
proof -
assume "v < 1"
then show False
- using v(3)[THEN spec[where x=1]] using x and fs by auto
+ using v(3)[THEN spec[where x=1]] using x fs by (simp add: pth_1 subset_iff)
next
assume "v > 1"
then show False
@@ -5294,8 +5294,7 @@
apply (cases "u = 1")
using assms(3)[THEN bspec[where x=x], THEN spec[where x=u]]
using \<open>0\<le>u\<close> and x and fs
- apply auto
- done
+ by auto
qed auto
qed
@@ -9866,7 +9865,7 @@
apply (rule le_setdistI, blast)
using False apply (fastforce intro: le_setdistI)
apply (simp add: algebra_simps)
- apply (metis dist_commute dist_triangle_alt order_trans [OF setdist_le_dist])
+ apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
done
then have "setdist s t - setdist {a} t \<le> setdist s {a}"
using False by (fastforce intro: le_setdistI)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Mar 07 14:34:45 2016 +0000
@@ -194,6 +194,9 @@
unfolding differentiable_def
by auto
+lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
+ using differentiable_on_def by blast
+
lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
unfolding differentiable_def
using has_derivative_at_within
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Mon Mar 07 14:34:45 2016 +0000
@@ -1384,6 +1384,8 @@
lemma complex_differentiable_Polygamma:
+ fixes z::complex
+ shows
"z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)"
using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Mar 07 14:34:45 2016 +0000
@@ -2501,6 +2501,12 @@
shows "integral s (\<lambda>x. c * f x) = c * integral s f"
by (simp add: mult.commute [of c])
+corollary integral_divide [simp]:
+ fixes z :: "'a::real_normed_field"
+ shows "integral S (\<lambda>x. f x / z) = integral S (\<lambda>x. f x) / z"
+using integral_mult_left [of S f "inverse z"]
+ by (simp add: divide_inverse_commute)
+
lemma has_integral_mult_right:
fixes c :: "'a :: real_normed_algebra"
shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
@@ -2681,6 +2687,12 @@
using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] \<open>c \<noteq> 0\<close>
by auto
+lemma integrable_on_cmult_left:
+ assumes "f integrable_on s"
+ shows "(\<lambda>x. of_real c * f x) integrable_on s"
+ using integrable_cmul[of f s "of_real c"] assms
+ by (simp add: scaleR_conv_of_real)
+
lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
unfolding integrable_on_def by(auto intro: has_integral_neg)
@@ -2756,6 +2768,45 @@
unfolding integral_def
by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)
+lemma integrable_on_cmult_left_iff [simp]:
+ assumes "c \<noteq> 0"
+ shows "(\<lambda>x. of_real c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "(\<lambda>x. of_real (1 / c) * (of_real c * f x)) integrable_on s"
+ using integrable_cmul[of "\<lambda>x. of_real c * f x" s "1 / of_real c"]
+ by (simp add: scaleR_conv_of_real)
+ then have "(\<lambda>x. (of_real (1 / c) * of_real c * f x)) integrable_on s"
+ by (simp add: algebra_simps)
+ with \<open>c \<noteq> 0\<close> show ?rhs
+ by (metis (no_types, lifting) integrable_eq mult.left_neutral nonzero_divide_eq_eq of_real_1 of_real_mult)
+qed (blast intro: integrable_on_cmult_left)
+
+lemma integrable_on_cmult_right:
+ fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
+ assumes "f integrable_on s"
+ shows "(\<lambda>x. f x * of_real c) integrable_on s"
+using integrable_on_cmult_left [OF assms] by (simp add: mult.commute)
+
+lemma integrable_on_cmult_right_iff [simp]:
+ fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
+ assumes "c \<noteq> 0"
+ shows "(\<lambda>x. f x * of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
+using integrable_on_cmult_left_iff [OF assms] by (simp add: mult.commute)
+
+lemma integrable_on_cdivide:
+ fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
+ assumes "f integrable_on s"
+ shows "(\<lambda>x. f x / of_real c) integrable_on s"
+by (simp add: integrable_on_cmult_right divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+
+lemma integrable_on_cdivide_iff [simp]:
+ fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
+ assumes "c \<noteq> 0"
+ shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
+by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+
lemma has_integral_null [intro]:
assumes "content(cbox a b) = 0"
shows "(f has_integral 0) (cbox a b)"
@@ -6065,6 +6116,30 @@
qed
qed
+lemma ident_has_integral:
+ fixes a::real
+ assumes "a \<le> b"
+ shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2) / 2) {a..b}"
+proof -
+ have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
+ apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
+ unfolding power2_eq_square
+ by (rule derivative_eq_intros | simp)+
+ then show ?thesis
+ by (simp add: field_simps)
+qed
+
+lemma integral_ident [simp]:
+ fixes a::real
+ assumes "a \<le> b"
+ shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
+using ident_has_integral integral_unique by fastforce
+
+lemma ident_integrable_on:
+ fixes a::real
+ shows "(\<lambda>x. x) integrable_on {a..b}"
+by (metis atLeastatMost_empty_iff integrable_on_def has_integral_empty ident_has_integral)
+
subsection \<open>Taylor series expansion\<close>
@@ -6737,27 +6812,18 @@
lemma content_image_affinity_cbox:
"content((\<lambda>x::'a::euclidean_space. m *\<^sub>R x + c) ` cbox a b) =
\<bar>m\<bar> ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
-proof -
- {
- presume *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
- show ?thesis
- apply cases
- apply (rule *)
- apply assumption
- unfolding not_not
- using content_empty
- apply auto
- done
- }
- assume as: "cbox a b \<noteq> {}"
+proof (cases "cbox a b = {}")
+ case True then show ?thesis by simp
+next
+ case False
show ?thesis
proof (cases "m \<ge> 0")
case True
- with as have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
+ with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
unfolding box_ne_empty
apply (intro ballI)
apply (erule_tac x=i in ballE)
- apply (auto simp: inner_simps intro!: mult_left_mono)
+ apply (auto simp: inner_simps mult_left_mono)
done
moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b - a) \<bullet> i"
by (simp add: inner_simps field_simps)
@@ -6766,11 +6832,11 @@
setprod.distrib setprod_constant inner_diff_left)
next
case False
- with as have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
+ with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
unfolding box_ne_empty
apply (intro ballI)
apply (erule_tac x=i in ballE)
- apply (auto simp: inner_simps intro!: mult_left_mono)
+ apply (auto simp: inner_simps mult_left_mono)
done
moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b - a) \<bullet> i"
by (simp add: inner_simps field_simps)
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 07 14:34:45 2016 +0000
@@ -556,6 +556,190 @@
by (rule ext) (auto simp: mult.commute)
+subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close>
+
+lemma path_join_path_ends:
+ fixes g1 :: "real \<Rightarrow> 'a::metric_space"
+ assumes "path(g1 +++ g2)" "path g2"
+ shows "pathfinish g1 = pathstart g2"
+proof (rule ccontr)
+ def e \<equiv> "dist (g1 1) (g2 0)"
+ assume Neg: "pathfinish g1 \<noteq> pathstart g2"
+ then have "0 < dist (pathfinish g1) (pathstart g2)"
+ by auto
+ then have "e > 0"
+ by (metis e_def pathfinish_def pathstart_def)
+ then obtain d1 where "d1 > 0"
+ and d1: "\<And>x'. \<lbrakk>x'\<in>{0..1}; norm x' < d1\<rbrakk> \<Longrightarrow> dist (g2 x') (g2 0) < e/2"
+ using assms(2) unfolding path_def continuous_on_iff
+ apply (drule_tac x=0 in bspec, simp)
+ by (metis half_gt_zero_iff norm_conv_dist)
+ obtain d2 where "d2 > 0"
+ and d2: "\<And>x'. \<lbrakk>x'\<in>{0..1}; dist x' (1/2) < d2\<rbrakk>
+ \<Longrightarrow> dist ((g1 +++ g2) x') (g1 1) < e/2"
+ using assms(1) \<open>e > 0\<close> unfolding path_def continuous_on_iff
+ apply (drule_tac x="1/2" in bspec, simp)
+ apply (drule_tac x="e/2" in spec)
+ apply (force simp: joinpaths_def)
+ done
+ have int01_1: "min (1/2) (min d1 d2) / 2 \<in> {0..1}"
+ using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
+ have dist1: "norm (min (1 / 2) (min d1 d2) / 2) < d1"
+ using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
+ have int01_2: "1/2 + min (1/2) (min d1 d2) / 4 \<in> {0..1}"
+ using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
+ have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
+ using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
+ have [simp]: "~ min (1 / 2) (min d1 d2) \<le> 0"
+ using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
+ have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
+ "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
+ using d1 [OF int01_1 dist1] d2 [OF int01_2 dist2] by (simp_all add: joinpaths_def)
+ then have "dist (g1 1) (g2 0) < e/2 + e/2"
+ using dist_triangle_half_r e_def by blast
+ then show False
+ by (simp add: e_def [symmetric])
+qed
+
+lemma path_join_eq [simp]:
+ fixes g1 :: "real \<Rightarrow> 'a::metric_space"
+ assumes "path g1" "path g2"
+ shows "path(g1 +++ g2) \<longleftrightarrow> pathfinish g1 = pathstart g2"
+ using assms by (metis path_join_path_ends path_join_imp)
+
+lemma simple_path_joinE:
+ assumes "simple_path(g1 +++ g2)" and "pathfinish g1 = pathstart g2"
+ obtains "arc g1" "arc g2"
+ "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
+proof -
+ have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk>
+ \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
+ using assms by (simp add: simple_path_def)
+ have "path g1"
+ using assms path_join simple_path_imp_path by blast
+ moreover have "inj_on g1 {0..1}"
+ proof (clarsimp simp: inj_on_def)
+ fix x y
+ assume "g1 x = g1 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
+ then show "x = y"
+ using * [of "x/2" "y/2"] by (simp add: joinpaths_def split_ifs)
+ qed
+ ultimately have "arc g1"
+ using assms by (simp add: arc_def)
+ have [simp]: "g2 0 = g1 1"
+ using assms by (metis pathfinish_def pathstart_def)
+ have "path g2"
+ using assms path_join simple_path_imp_path by blast
+ moreover have "inj_on g2 {0..1}"
+ proof (clarsimp simp: inj_on_def)
+ fix x y
+ assume "g2 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
+ then show "x = y"
+ using * [of "(x + 1) / 2" "(y + 1) / 2"]
+ by (force simp: joinpaths_def split_ifs divide_simps)
+ qed
+ ultimately have "arc g2"
+ using assms by (simp add: arc_def)
+ have "g2 y = g1 0 \<or> g2 y = g1 1"
+ if "g1 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" for x y
+ using * [of "x / 2" "(y + 1) / 2"] that
+ by (auto simp: joinpaths_def split_ifs divide_simps)
+ then have "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
+ by (fastforce simp: pathstart_def pathfinish_def path_image_def)
+ with \<open>arc g1\<close> \<open>arc g2\<close> show ?thesis using that by blast
+qed
+
+lemma simple_path_join_loop_eq:
+ assumes "pathfinish g2 = pathstart g1" "pathfinish g1 = pathstart g2"
+ shows "simple_path(g1 +++ g2) \<longleftrightarrow>
+ arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
+by (metis assms simple_path_joinE simple_path_join_loop)
+
+lemma arc_join_eq:
+ assumes "pathfinish g1 = pathstart g2"
+ shows "arc(g1 +++ g2) \<longleftrightarrow>
+ arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "simple_path(g1 +++ g2)" by (rule arc_imp_simple_path)
+ then have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk>
+ \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
+ using assms by (simp add: simple_path_def)
+ have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u
+ using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>]
+ by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps)
+ then have n1: "~ (pathstart g1 \<in> path_image g2)"
+ unfolding pathstart_def path_image_def
+ using atLeastAtMost_iff by blast
+ show ?rhs using \<open>?lhs\<close>
+ apply (rule simple_path_joinE [OF arc_imp_simple_path assms])
+ using n1 by force
+next
+ assume ?rhs then show ?lhs
+ using assms
+ by (fastforce simp: pathfinish_def pathstart_def intro!: arc_join)
+qed
+
+lemma arc_join_eq_alt:
+ "pathfinish g1 = pathstart g2
+ \<Longrightarrow> (arc(g1 +++ g2) \<longleftrightarrow>
+ arc g1 \<and> arc g2 \<and>
+ path_image g1 \<inter> path_image g2 = {pathstart g2})"
+using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
+
+
+subsection\<open>The joining of paths is associative\<close>
+
+lemma path_assoc:
+ "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
+ \<Longrightarrow> path(p +++ (q +++ r)) \<longleftrightarrow> path((p +++ q) +++ r)"
+by simp
+
+lemma simple_path_assoc:
+ assumes "pathfinish p = pathstart q" "pathfinish q = pathstart r"
+ shows "simple_path (p +++ (q +++ r)) \<longleftrightarrow> simple_path ((p +++ q) +++ r)"
+proof (cases "pathstart p = pathfinish r")
+ case True show ?thesis
+ proof
+ assume "simple_path (p +++ q +++ r)"
+ with assms True show "simple_path ((p +++ q) +++ r)"
+ by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join
+ dest: arc_distinct_ends [of r])
+ next
+ assume 0: "simple_path ((p +++ q) +++ r)"
+ with assms True have q: "pathfinish r \<notin> path_image q"
+ using arc_distinct_ends
+ by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join)
+ have "pathstart r \<notin> path_image p"
+ using assms
+ by (metis 0 IntI arc_distinct_ends arc_join_eq_alt empty_iff insert_iff
+ pathfinish_in_path_image pathfinish_join simple_path_joinE)
+ with assms 0 q True show "simple_path (p +++ q +++ r)"
+ by (auto simp: simple_path_join_loop_eq arc_join_eq path_image_join
+ dest!: subsetD [OF _ IntI])
+ qed
+next
+ case False
+ { fix x :: 'a
+ assume a: "path_image p \<inter> path_image q \<subseteq> {pathstart q}"
+ "(path_image p \<union> path_image q) \<inter> path_image r \<subseteq> {pathstart r}"
+ "x \<in> path_image p" "x \<in> path_image r"
+ have "pathstart r \<in> path_image q"
+ by (metis assms(2) pathfinish_in_path_image)
+ with a have "x = pathstart q"
+ by blast
+ }
+ with False assms show ?thesis
+ by (auto simp: simple_path_eq_arc simple_path_join_loop_eq arc_join_eq path_image_join)
+qed
+
+lemma arc_assoc:
+ "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
+ \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
+by (simp add: arc_simple_path simple_path_assoc)
+
+
section\<open>Choosing a subpath of an existing path\<close>
definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
@@ -2526,6 +2710,58 @@
apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
+subsection\<open>Condition for an open map's image to contain a ball\<close>
+
+lemma ball_subset_open_map_image:
+ fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
+ assumes contf: "continuous_on (closure S) f"
+ and oint: "open (f ` interior S)"
+ and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
+ and "bounded S" "a \<in> S" "0 < r"
+ shows "ball (f a) r \<subseteq> f ` S"
+proof (cases "f ` S = UNIV")
+ case True then show ?thesis by simp
+next
+ case False
+ obtain w where w: "w \<in> frontier (f ` S)"
+ and dw_le: "\<And>y. y \<in> frontier (f ` S) \<Longrightarrow> norm (f a - w) \<le> norm (f a - y)"
+ apply (rule distance_attains_inf [of "frontier(f ` S)" "f a"])
+ using \<open>a \<in> S\<close> by (auto simp: frontier_eq_empty dist_norm False)
+ then obtain \<xi> where \<xi>: "\<And>n. \<xi> n \<in> f ` S" and tendsw: "\<xi> \<longlonglongrightarrow> w"
+ by (metis Diff_iff frontier_def closure_sequential)
+ then have "\<And>n. \<exists>x \<in> S. \<xi> n = f x" by force
+ then obtain z where zs: "\<And>n. z n \<in> S" and fz: "\<And>n. \<xi> n = f (z n)"
+ by metis
+ then obtain y K where y: "y \<in> closure S" and "subseq K" and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
+ using \<open>bounded S\<close>
+ apply (simp add: compact_closure [symmetric] compact_def)
+ apply (drule_tac x=z in spec)
+ using closure_subset apply force
+ done
+ then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
+ by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
+ have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
+ have "f \<circ> z = \<xi>" "(\<lambda>n. f (z n)) = \<xi>"
+ using fz by auto
+ moreover then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
+ by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
+ ultimately have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
+ have rle: "r \<le> norm (f y - f a)"
+ apply (rule le_no)
+ using w wy oint
+ by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
+ have **: "(~(b \<inter> (- S) = {}) \<and> ~(b - (- S) = {}) \<Longrightarrow> (b \<inter> f \<noteq> {}))
+ \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
+ b \<subseteq> S" for b f and S :: "'b set"
+ by blast
+ show ?thesis
+ apply (rule **) (*such a horrible mess*)
+ apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
+ using \<open>a \<in> S\<close> \<open>0 < r\<close>
+ apply (auto simp: disjoint_iff_not_equal dist_norm)
+ by (metis dw_le norm_minus_commute not_less order_trans rle wy)
+qed
+
section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
text\<open> We often just want to require that it fixes some subset, but to take in
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Mar 07 14:34:45 2016 +0000
@@ -859,6 +859,24 @@
lemma cball_diff_eq_sphere: "cball a r - ball a r = {x. dist x a = r}"
by (auto simp: cball_def ball_def dist_commute)
+lemma image_add_ball [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "op + b ` ball a r = ball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
+lemma image_add_cball [simp]:
+ fixes a :: "'a::real_normed_vector"
+ shows "op + b ` cball a r = cball (a+b) r"
+apply (intro equalityI subsetI)
+apply (force simp: dist_norm)
+apply (rule_tac x="x-b" in image_eqI)
+apply (auto simp: dist_norm algebra_simps)
+done
+
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
have "open (dist x -` {..<e})"
@@ -2191,7 +2209,7 @@
definition "frontier S = closure S - interior S"
-lemma frontier_closed: "closed (frontier S)"
+lemma frontier_closed [iff]: "closed (frontier S)"
by (simp add: frontier_def closed_Diff)
lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
@@ -2202,11 +2220,11 @@
shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
unfolding frontier_def closure_interior
by (auto simp add: mem_interior subset_eq ball_def)
-
+
lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
by (metis frontier_def closure_closed Diff_subset)
-lemma frontier_empty[simp]: "frontier {} = {}"
+lemma frontier_empty [simp]: "frontier {} = {}"
by (simp add: frontier_def)
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
@@ -2221,7 +2239,7 @@
then show ?thesis using frontier_subset_closed[of S] ..
qed
-lemma frontier_complement [simp]: "frontier (- S) = frontier S"
+lemma frontier_complement [simp]: "frontier (- S) = frontier S"
by (auto simp add: frontier_def closure_complement interior_complement)
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
@@ -4465,6 +4483,11 @@
by auto
qed
+lemma compact_closure [simp]:
+ fixes S :: "'a::heine_borel set"
+ shows "compact(closure S) \<longleftrightarrow> bounded S"
+by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
+
lemma compact_components:
fixes s :: "'a::heine_borel set"
shows "\<lbrakk>compact s; c \<in> components s\<rbrakk> \<Longrightarrow> compact c"
@@ -5541,10 +5564,6 @@
subsubsection \<open>Structural rules for pointwise continuity\<close>
-lemmas continuous_within_id = continuous_ident
-
-lemmas continuous_at_id = continuous_ident
-
lemma continuous_infdist[continuous_intros]:
assumes "continuous F f"
shows "continuous F (\<lambda>x. infdist (f x) A)"
@@ -5890,6 +5909,111 @@
qed
qed
+subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
+
+lemma continuous_on_closure:
+ "continuous_on (closure S) f \<longleftrightarrow>
+ (\<forall>x e. x \<in> closure S \<and> 0 < e
+ \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ unfolding continuous_on_iff by (metis Un_iff closure_def)
+next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ proof
+ fix x and e::real
+ assume "0 < e" and x: "x \<in> closure S"
+ obtain \<delta>::real where "\<delta> > 0"
+ and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
+ using R [of x "e/2"] \<open>0 < e\<close> x by auto
+ have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
+ proof -
+ obtain \<delta>'::real where "\<delta>' > 0"
+ and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
+ using R [of y "e/2"] \<open>0 < e\<close> y by auto
+ obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
+ using closure_approachable y
+ by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
+ have "dist (f z) (f y) < e/2"
+ apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
+ using z \<open>0 < \<delta>'\<close> by linarith
+ moreover have "dist (f z) (f x) < e/2"
+ apply (rule \<delta> [OF \<open>z \<in> S\<close>])
+ using z \<open>0 < \<delta>\<close> dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto
+ ultimately show ?thesis
+ by (metis dist_commute dist_triangle_half_l less_imp_le)
+ qed
+ then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
+ by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
+ qed
+qed
+
+lemma continuous_on_closure_sequentially:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
+ shows
+ "continuous_on (closure S) f \<longleftrightarrow>
+ (\<forall>x a. a \<in> closure S \<and> (\<forall>n. x n \<in> S) \<and> x \<longlonglongrightarrow> a \<longrightarrow> (f \<circ> x) \<longlonglongrightarrow> f a)"
+ (is "?lhs = ?rhs")
+proof -
+ have "continuous_on (closure S) f \<longleftrightarrow>
+ (\<forall>x \<in> closure S. continuous (at x within S) f)"
+ by (force simp: continuous_on_closure Topology_Euclidean_Space.continuous_within_eps_delta)
+ also have "... = ?rhs"
+ by (force simp: continuous_within_sequentially)
+ finally show ?thesis .
+qed
+
+lemma uniformly_continuous_on_closure:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ assumes ucont: "uniformly_continuous_on S f"
+ and cont: "continuous_on (closure S) f"
+ shows "uniformly_continuous_on (closure S) f"
+unfolding uniformly_continuous_on_def
+proof (intro allI impI)
+ fix e::real
+ assume "0 < e"
+ then obtain d::real
+ where "d>0"
+ and d: "\<And>x x'. \<lbrakk>x\<in>S; x'\<in>S; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e/3"
+ using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
+ show "\<exists>d>0. \<forall>x\<in>closure S. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
+ proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
+ fix x y
+ assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
+ obtain d1::real where "d1 > 0"
+ and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
+ using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
+ obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
+ using closure_approachable [of x S]
+ by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral)
+ obtain d2::real where "d2 > 0"
+ and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
+ using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
+ obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
+ using closure_approachable [of y S]
+ by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
+ have "dist x' x < d/3" using x' by auto
+ moreover have "dist x y < d/3"
+ by (metis dist_commute dyx less_divide_eq_numeral1(1))
+ moreover have "dist y y' < d/3"
+ by (metis (no_types) dist_commute min_less_iff_conj y')
+ ultimately have "dist x' y' < d/3 + d/3 + d/3"
+ by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
+ then have "dist x' y' < d" by simp
+ then have "dist (f x') (f y') < e/3"
+ by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
+ moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
+ by (simp add: closure_def)
+ moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
+ by (simp add: closure_def)
+ ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
+ by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
+ then show "dist (f y) (f x) < e" by simp
+ qed
+qed
+
subsection \<open>A function constant on a set\<close>
definition constant_on (infixl "(constant'_on)" 50)
@@ -6047,7 +6171,7 @@
{
fix x
have "continuous (at x) (\<lambda>x. x - a)"
- by (intro continuous_diff continuous_at_id continuous_const)
+ by (intro continuous_diff continuous_ident continuous_const)
}
moreover have "{x. x - a \<in> s} = op + a ` s"
by force
@@ -6385,7 +6509,7 @@
have "?B \<noteq> {}" using \<open>b \<in> s\<close>
by (auto simp: dist_commute)
moreover have "continuous_on ?B (dist a)"
- by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const)
+ by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
moreover have "compact ?B"
by (intro closed_inter_compact \<open>closed s\<close> compact_cball)
ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
@@ -6828,7 +6952,7 @@
then have "s \<noteq> {}" "t \<noteq> {}" by auto
let ?inf = "\<lambda>x. infdist x t"
have "continuous_on s ?inf"
- by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_at_id)
+ by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"
using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto
then have "0 < ?inf x"
@@ -7134,7 +7258,7 @@
lemma open_box[intro]: "open (box a b)"
proof -
have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
- by (auto intro!: continuous_open_vimage continuous_inner continuous_at_id continuous_const)
+ by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
by (auto simp add: box_def inner_commute)
finally show ?thesis .
@@ -8344,7 +8468,7 @@
let ?D = "(\<lambda>x. (x, x)) ` s"
have D: "compact ?D" "?D \<noteq> {}"
by (rule compact_continuous_image)
- (auto intro!: s continuous_Pair continuous_within_id simp: continuous_on_eq_continuous_within)
+ (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
using dist by fastforce
@@ -8353,7 +8477,7 @@
then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
unfolding continuous_on_eq_continuous_within
by (intro continuous_dist ballI continuous_within_compose)
- (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
+ (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)
obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
using continuous_attains_inf[OF D cont] by auto
@@ -8408,7 +8532,7 @@
next
assume ?rhs then show ?lhs
apply (auto simp: ball_def dist_norm)
- apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
+ apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans)
done
qed
@@ -8448,7 +8572,7 @@
next
assume ?rhs then show ?lhs
apply (auto simp: ball_def dist_norm )
- apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
+ apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans)
done
qed
--- a/src/HOL/Probability/Regularity.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Probability/Regularity.thy Mon Mar 07 14:34:45 2016 +0000
@@ -249,7 +249,7 @@
fix d
have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
also have "open \<dots>"
- by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
+ by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident)
finally have "open (?G d)" .
} note open_G = this
from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>]
--- a/src/HOL/Real_Vector_Spaces.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Mar 07 14:34:45 2016 +0000
@@ -1050,15 +1050,14 @@
using dist_triangle2 [of y x y] by simp
qed
+lemma dist_commute_lessI: "dist y x < e \<Longrightarrow> dist x y < e"
+ by (simp add: dist_commute)
+
lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
-using dist_triangle2 [of x z y] by (simp add: dist_commute)
+ using dist_triangle2 [of x z y] by (simp add: dist_commute)
lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
-using dist_triangle2 [of x y a] by (simp add: dist_commute)
-
-lemma dist_triangle_alt:
- shows "dist y z <= dist x y + dist x z"
-by (rule dist_triangle3)
+ using dist_triangle2 [of x y a] by (simp add: dist_commute)
lemma dist_pos_lt:
shows "x \<noteq> y ==> 0 < dist x y"
@@ -1337,6 +1336,11 @@
assumes "linear D" obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
+corollary real_linearD:
+ fixes f :: "real \<Rightarrow> real"
+ assumes "linear f" obtains c where "f = op* c"
+by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
+
lemma linearI:
assumes "\<And>x y. f (x + y) = f x + f y"
assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
--- a/src/HOL/Topological_Spaces.thy Mon Mar 07 08:14:18 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Mar 07 14:34:45 2016 +0000
@@ -399,7 +399,7 @@
definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
-definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
+definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_)/ within (_)" [1000, 60] 60)
where "at a within s = inf (nhds a) (principal (s - {a}))"
abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where