new material to Blochj's theorem, as well as supporting lemmas
authorpaulson <lp15@cam.ac.uk>
Mon Mar 07 14:34:45 2016 +0000 (2016-03-07)
changeset 62533bc25f3916a99
parent 62532 edee1966fddf
child 62534 6855b348e828
new material to Blochj's theorem, as well as supporting lemmas
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Gamma.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Regularity.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 08:14:18 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Mar 07 14:34:45 2016 +0000
     1.3 @@ -2678,6 +2678,7 @@
     1.4  (** Existence of a primitive.*)
     1.5  
     1.6  lemma holomorphic_starlike_primitive:
     1.7 +  fixes f :: "complex \<Rightarrow> complex"
     1.8    assumes contf: "continuous_on s f"
     1.9        and s: "starlike s" and os: "open s"
    1.10        and k: "finite k"
    1.11 @@ -2796,6 +2797,8 @@
    1.12    done
    1.13  
    1.14  lemma holomorphic_convex_primitive:
    1.15 +  fixes f :: "complex \<Rightarrow> complex"
    1.16 +  shows
    1.17    "\<lbrakk>convex s; finite k; continuous_on s f;
    1.18      \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
    1.19     \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
     2.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 08:14:18 2016 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 07 14:34:45 2016 +0000
     2.3 @@ -277,11 +277,14 @@
     2.4  
     2.5  subsection\<open>Holomorphic functions\<close>
     2.6  
     2.7 -text\<open>Could be generalized to real normed fields, but in practice that would only include the reals\<close>
     2.8 -definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
     2.9 +definition complex_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
    2.10             (infixr "(complex'_differentiable)" 50)
    2.11    where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
    2.12  
    2.13 +lemma complex_differentiable_derivI:
    2.14 +    "f complex_differentiable (at x) \<Longrightarrow> (f has_field_derivative deriv f x) (at x)"
    2.15 +by (simp add: complex_differentiable_def DERIV_deriv_iff_has_field_derivative)
    2.16 +
    2.17  lemma complex_differentiable_imp_continuous_at:
    2.18      "f complex_differentiable (at x within s) \<Longrightarrow> continuous (at x within s) f"
    2.19    by (metis DERIV_continuous complex_differentiable_def)
    2.20 @@ -297,24 +300,24 @@
    2.21    unfolding complex_differentiable_def
    2.22    by (metis DERIV_subset top_greatest)
    2.23  
    2.24 -lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F"
    2.25 +lemma complex_differentiable_linear [simp,derivative_intros]: "(op * c) complex_differentiable F"
    2.26  proof -
    2.27    show ?thesis
    2.28      unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs
    2.29      by (force intro: has_derivative_mult_right)
    2.30  qed
    2.31  
    2.32 -lemma complex_differentiable_const [derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
    2.33 +lemma complex_differentiable_const [simp,derivative_intros]: "(\<lambda>z. c) complex_differentiable F"
    2.34    unfolding complex_differentiable_def has_field_derivative_def
    2.35    by (rule exI [where x=0])
    2.36       (metis has_derivative_const lambda_zero)
    2.37  
    2.38 -lemma complex_differentiable_ident [derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
    2.39 +lemma complex_differentiable_ident [simp,derivative_intros]: "(\<lambda>z. z) complex_differentiable F"
    2.40    unfolding complex_differentiable_def has_field_derivative_def
    2.41    by (rule exI [where x=1])
    2.42       (simp add: lambda_one [symmetric])
    2.43  
    2.44 -lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F"
    2.45 +lemma complex_differentiable_id [simp,derivative_intros]: "id complex_differentiable F"
    2.46    unfolding id_def by (rule complex_differentiable_ident)
    2.47  
    2.48  lemma complex_differentiable_minus [derivative_intros]:
    2.49 @@ -328,6 +331,10 @@
    2.50    using assms unfolding complex_differentiable_def
    2.51    by (metis field_differentiable_add)
    2.52  
    2.53 +lemma complex_differentiable_add_const [simp,derivative_intros]:
    2.54 +     "op + c complex_differentiable F"
    2.55 +  by (simp add: complex_differentiable_add)
    2.56 +
    2.57  lemma complex_differentiable_setsum [derivative_intros]:
    2.58    "(\<And>i. i \<in> I \<Longrightarrow> (f i) complex_differentiable F) \<Longrightarrow> (\<lambda>z. \<Sum>i\<in>I. f i z) complex_differentiable F"
    2.59    by (induct I rule: infinite_finite_induct)
    2.60 @@ -503,6 +510,11 @@
    2.61    "DERIV f x :> deriv f x \<longleftrightarrow> f complex_differentiable at x"
    2.62    unfolding complex_differentiable_def by (metis DERIV_imp_deriv)
    2.63  
    2.64 +lemma holomorphic_derivI:
    2.65 +     "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk>
    2.66 +      \<Longrightarrow> (f has_field_derivative deriv f x) (at x within T)"
    2.67 +by (metis DERIV_deriv_iff_complex_differentiable at_within_open  holomorphic_on_def has_field_derivative_at_within)
    2.68 +
    2.69  lemma complex_derivative_chain:
    2.70    "f complex_differentiable at x \<Longrightarrow> g complex_differentiable at (f x)
    2.71      \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
    2.72 @@ -568,6 +580,20 @@
    2.73  apply (simp add: algebra_simps)
    2.74  done
    2.75  
    2.76 +lemma nonzero_deriv_nonconstant:
    2.77 +  assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
    2.78 +    shows "\<not> f constant_on S"
    2.79 +unfolding constant_on_def
    2.80 +by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique)
    2.81 +
    2.82 +lemma holomorphic_nonconstant:
    2.83 +  assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0"
    2.84 +    shows "\<not> f constant_on S"
    2.85 +    apply (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S])
    2.86 +    using assms
    2.87 +    apply (auto simp: holomorphic_derivI)
    2.88 +    done
    2.89 +
    2.90  subsection\<open>Analyticity on a set\<close>
    2.91  
    2.92  definition analytic_on (infixl "(analytic'_on)" 50)
     3.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Mar 07 08:14:18 2016 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Mar 07 14:34:45 2016 +0000
     3.3 @@ -1633,13 +1633,15 @@
     3.4    done
     3.5  
     3.6  lemma complex_differentiable_powr_right:
     3.7 +  fixes w::complex
     3.8 +  shows
     3.9      "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
    3.10  using complex_differentiable_def has_field_derivative_powr_right by blast
    3.11  
    3.12  lemma holomorphic_on_powr_right:
    3.13      "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
    3.14 -    unfolding holomorphic_on_def
    3.15 -    using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
    3.16 +    unfolding holomorphic_on_def complex_differentiable_def
    3.17 +by (metis (full_types) DERIV_chain' has_field_derivative_powr_right) 
    3.18  
    3.19  lemma norm_powr_real_powr:
    3.20    "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
     4.1 --- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 08:14:18 2016 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Mar 07 14:34:45 2016 +0000
     4.3 @@ -1722,4 +1722,412 @@
     4.4      done
     4.5  qed
     4.6  
     4.7 +subsection\<open>Bloch's theorem\<close>
     4.8 +
     4.9 +lemma Bloch_lemma_0:
    4.10 +  assumes holf: "f holomorphic_on cball 0 r" and "0 < r"
    4.11 +      and [simp]: "f 0 = 0"
    4.12 +      and le: "\<And>z. norm z < r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f 0)"
    4.13 +    shows "ball 0 ((3 - 2 * sqrt 2) * r * norm(deriv f 0)) \<subseteq> f ` ball 0 r"
    4.14 +proof -
    4.15 +  have "sqrt 2 < 3/2"
    4.16 +    by (rule real_less_lsqrt) (auto simp: power2_eq_square)
    4.17 +  then have sq3: "0 < 3 - 2 * sqrt 2" by simp
    4.18 +  show ?thesis
    4.19 +  proof (cases "deriv f 0 = 0")
    4.20 +    case True then show ?thesis by simp
    4.21 +  next
    4.22 +    case False
    4.23 +    def C \<equiv> "2 * norm(deriv f 0)"
    4.24 +    have "0 < C" using False by (simp add: C_def)
    4.25 +    have holf': "f holomorphic_on ball 0 r" using holf
    4.26 +      using ball_subset_cball holomorphic_on_subset by blast
    4.27 +    then have holdf': "deriv f holomorphic_on ball 0 r"
    4.28 +      by (rule holomorphic_deriv [OF _ open_ball])
    4.29 +    have "Le1": "norm(deriv f z - deriv f 0) \<le> norm z / (r - norm z) * C"
    4.30 +                if "norm z < r" for z
    4.31 +    proof -
    4.32 +      have T1: "norm(deriv f z - deriv f 0) \<le> norm z / (R - norm z) * C"
    4.33 +              if R: "norm z < R" "R < r" for R
    4.34 +      proof -
    4.35 +        have "0 < R" using R
    4.36 +          by (metis less_trans norm_zero zero_less_norm_iff)
    4.37 +        have df_le: "\<And>x. norm x < r \<Longrightarrow> norm (deriv f x) \<le> C"
    4.38 +          using le by (simp add: C_def)
    4.39 +        have hol_df: "deriv f holomorphic_on cball 0 R"
    4.40 +          apply (rule holomorphic_on_subset) using R holdf' by auto
    4.41 +        have *: "((\<lambda>w. deriv f w / (w - z)) has_contour_integral 2 * pi * \<i> * deriv f z) (circlepath 0 R)"
    4.42 +                 if "norm z < R" for z
    4.43 +          using \<open>0 < R\<close> that Cauchy_integral_formula_convex_simple [OF convex_cball hol_df, of _ "circlepath 0 R"]
    4.44 +          by (force simp: winding_number_circlepath)
    4.45 +        have **: "((\<lambda>x. deriv f x / (x - z) - deriv f x / x) has_contour_integral
    4.46 +                   of_real (2 * pi) * \<i> * (deriv f z - deriv f 0))
    4.47 +                  (circlepath 0 R)"
    4.48 +           using has_contour_integral_diff [OF * [of z] * [of 0]] \<open>0 < R\<close> that
    4.49 +           by (simp add: algebra_simps)
    4.50 +        have [simp]: "\<And>x. norm x = R \<Longrightarrow> x \<noteq> z"  using that(1) by blast
    4.51 +        have "norm (deriv f x / (x - z) - deriv f x / x)
    4.52 +                     \<le> C * norm z / (R * (R - norm z))"
    4.53 +                  if "norm x = R" for x
    4.54 +        proof -
    4.55 +          have [simp]: "norm (deriv f x * x - deriv f x * (x - z)) =
    4.56 +                        norm (deriv f x) * norm z"
    4.57 +            by (simp add: norm_mult right_diff_distrib')
    4.58 +          show ?thesis
    4.59 +            using  \<open>0 < R\<close> \<open>0 < C\<close> R that
    4.60 +            apply (simp add: norm_mult norm_divide divide_simps)
    4.61 +            using df_le norm_triangle_ineq2 \<open>0 < C\<close> apply (auto intro!: mult_mono)
    4.62 +            done
    4.63 +        qed
    4.64 +        then show ?thesis
    4.65 +          using has_contour_integral_bound_circlepath
    4.66 +                  [OF **, of "C * norm z/(R*(R - norm z))"]
    4.67 +                \<open>0 < R\<close> \<open>0 < C\<close> R
    4.68 +          apply (simp add: norm_mult norm_divide)
    4.69 +          apply (simp add: divide_simps mult.commute)
    4.70 +          done
    4.71 +      qed
    4.72 +      obtain r' where r': "norm z < r'" "r' < r"
    4.73 +        using Rats_dense_in_real [of "norm z" r] \<open>norm z < r\<close> by blast
    4.74 +      then have [simp]: "closure {r'<..<r} = {r'..r}" by simp
    4.75 +      show ?thesis
    4.76 +        apply (rule continuous_ge_on_closure
    4.77 +                 [where f = "\<lambda>r. norm z / (r - norm z) * C" and s = "{r'<..<r}",
    4.78 +                  OF _ _ T1])
    4.79 +        apply (intro continuous_intros)
    4.80 +        using that r'
    4.81 +        apply (auto simp: not_le)
    4.82 +        done
    4.83 +    qed
    4.84 +    have "*": "(norm z - norm z^2/(r - norm z)) * norm(deriv f 0) \<le> norm(f z)"
    4.85 +              if r: "norm z < r" for z
    4.86 +    proof -
    4.87 +      have 1: "\<And>x. x \<in> ball 0 r \<Longrightarrow>
    4.88 +              ((\<lambda>z. f z - deriv f 0 * z) has_field_derivative deriv f x - deriv f 0)
    4.89 +               (at x within ball 0 r)"
    4.90 +        by (rule derivative_eq_intros holomorphic_derivI holf' | simp)+
    4.91 +      have 2: "closed_segment 0 z \<subseteq> ball 0 r"
    4.92 +        by (metis \<open>0 < r\<close> convex_ball convex_contains_segment dist_self mem_ball mem_ball_0 that)
    4.93 +      have 3: "(\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C) integrable_on {0..1}"
    4.94 +        apply (rule integrable_on_cmult_right [where 'b=real, simplified])
    4.95 +        apply (rule integrable_on_cdivide [where 'b=real, simplified])
    4.96 +        apply (rule integrable_on_cmult_left [where 'b=real, simplified])
    4.97 +        apply (rule ident_integrable_on)
    4.98 +        done
    4.99 +      have 4: "norm (deriv f (x *\<^sub>R z) - deriv f 0) * norm z \<le> norm z * norm z * x * C / (r - norm z)"
   4.100 +              if x: "0 \<le> x" "x \<le> 1" for x
   4.101 +      proof -
   4.102 +        have [simp]: "x * norm z < r"
   4.103 +          using r x by (meson le_less_trans mult_le_cancel_right2 norm_not_less_zero)
   4.104 +        have "norm (deriv f (x *\<^sub>R z) - deriv f 0) \<le> norm (x *\<^sub>R z) / (r - norm (x *\<^sub>R z)) * C"
   4.105 +          apply (rule Le1) using r x \<open>0 < r\<close> by simp
   4.106 +        also have "... \<le> norm (x *\<^sub>R z) / (r - norm z) * C"
   4.107 +          using r x \<open>0 < r\<close>
   4.108 +          apply (simp add: divide_simps)
   4.109 +          by (simp add: \<open>0 < C\<close> mult.assoc mult_left_le_one_le ordered_comm_semiring_class.comm_mult_left_mono)
   4.110 +        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"
   4.111 +          by (rule mult_right_mono) simp
   4.112 +        with x show ?thesis by (simp add: algebra_simps)
   4.113 +      qed
   4.114 +      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
   4.115 +        by (metis add_diff_cancel_left' add_diff_eq diff_left_mono norm_diff_ineq order_trans)
   4.116 +      have "norm (integral {0..1} (\<lambda>x. (deriv f (x *\<^sub>R z) - deriv f 0) * z))
   4.117 +            \<le> integral {0..1} (\<lambda>t. (norm z)\<^sup>2 * t / (r - norm z) * C)"
   4.118 +        apply (rule integral_norm_bound_integral)
   4.119 +        using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
   4.120 +        apply (simp add: has_contour_integral_linepath has_integral_integrable_integral)
   4.121 +        apply (rule 3)
   4.122 +        apply (simp add: norm_mult power2_eq_square 4)
   4.123 +        done
   4.124 +      then have int_le: "norm (f z - deriv f 0 * z) \<le> (norm z)\<^sup>2 * norm(deriv f 0) / ((r - norm z))"
   4.125 +        using contour_integral_primitive [OF 1, of "linepath 0 z"] 2
   4.126 +        apply (simp add: has_contour_integral_linepath has_integral_integrable_integral C_def)
   4.127 +        done
   4.128 +      show ?thesis
   4.129 +        apply (rule le_norm [OF _ int_le])
   4.130 +        using \<open>norm z < r\<close>
   4.131 +        apply (simp add: power2_eq_square divide_simps C_def norm_mult)
   4.132 +        proof -
   4.133 +          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)"
   4.134 +            by (simp add: linordered_field_class.sign_simps(38))
   4.135 +          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)"
   4.136 +            by (simp add: linordered_field_class.sign_simps(38) mult.commute mult.left_commute)
   4.137 +        qed
   4.138 +    qed
   4.139 +    have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2)  < 1"
   4.140 +      by (auto simp:  sqrt2_less_2)
   4.141 +    have 1: "continuous_on (closure (ball 0 ((1 - sqrt 2 / 2) * r))) f"
   4.142 +      apply (rule continuous_on_subset [OF holomorphic_on_imp_continuous_on [OF holf]])
   4.143 +      apply (subst closure_ball)
   4.144 +      using \<open>0 < r\<close> mult_pos_pos sq201
   4.145 +      apply (auto simp: cball_subset_cball_iff)
   4.146 +      done
   4.147 +    have 2: "open (f ` interior (ball 0 ((1 - sqrt 2 / 2) * r)))"
   4.148 +      apply (rule open_mapping_thm [OF holf' open_ball connected_ball], force)
   4.149 +      using \<open>0 < r\<close> mult_pos_pos sq201 apply (simp add: ball_subset_ball_iff)
   4.150 +      using False \<open>0 < r\<close> centre_in_ball holf' holomorphic_nonconstant by blast
   4.151 +    have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv f 0)) =
   4.152 +          ball (f 0) ((3 - 2 * sqrt 2) * r * norm (deriv f 0))"
   4.153 +      by simp
   4.154 +    also have "...  \<subseteq> f ` ball 0 ((1 - sqrt 2 / 2) * r)"
   4.155 +    proof -
   4.156 +      have 3: "(3 - 2 * sqrt 2) * r * norm (deriv f 0) \<le> norm (f z)"
   4.157 +           if "norm z = (1 - sqrt 2 / 2) * r" for z
   4.158 +        apply (rule order_trans [OF _ *])
   4.159 +        using  \<open>0 < r\<close>
   4.160 +        apply (simp_all add: field_simps  power2_eq_square that)
   4.161 +        apply (simp add: mult.assoc [symmetric])
   4.162 +        done
   4.163 +      show ?thesis
   4.164 +        apply (rule ball_subset_open_map_image [OF 1 2 _ bounded_ball])
   4.165 +        using \<open>0 < r\<close> sq201 3 apply simp_all
   4.166 +        using C_def \<open>0 < C\<close> sq3 apply force
   4.167 +        done
   4.168 +     qed
   4.169 +    also have "...  \<subseteq> f ` ball 0 r"
   4.170 +      apply (rule image_subsetI [OF imageI], simp)
   4.171 +      apply (erule less_le_trans)
   4.172 +      using \<open>0 < r\<close> apply (auto simp: field_simps)
   4.173 +      done
   4.174 +    finally show ?thesis .
   4.175 +  qed
   4.176 +qed
   4.177 +
   4.178 +lemma Bloch_lemma: 
   4.179 +  assumes holf: "f holomorphic_on cball a r" and "0 < r"
   4.180 +      and le: "\<And>z. z \<in> ball a r \<Longrightarrow> norm(deriv f z) \<le> 2 * norm(deriv f a)"
   4.181 +    shows "ball (f a) ((3 - 2 * sqrt 2) * r * norm(deriv f a)) \<subseteq> f ` ball a r"
   4.182 +proof -
   4.183 +  have fz: "(\<lambda>z. f (a + z)) = f o (\<lambda>z. (a + z))"
   4.184 +    by (simp add: o_def)
   4.185 +  have hol0: "(\<lambda>z. f (a + z)) holomorphic_on cball 0 r"
   4.186 +    unfolding fz by (intro holomorphic_intros holf holomorphic_on_compose | simp)+
   4.187 +  then have [simp]: "\<And>x. norm x < r \<Longrightarrow> (\<lambda>z. f (a + z)) complex_differentiable at x"
   4.188 +    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)
   4.189 +  have [simp]: "\<And>z. norm z < r \<Longrightarrow> f complex_differentiable at (a + z)"
   4.190 +    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)
   4.191 +  then have [simp]: "f complex_differentiable at a"
   4.192 +    by (metis add.comm_neutral \<open>0 < r\<close> norm_eq_zero)
   4.193 +  have hol1: "(\<lambda>z. f (a + z) - f a) holomorphic_on cball 0 r"
   4.194 +    by (intro holomorphic_intros hol0)
   4.195 +  then have "ball 0 ((3 - 2 * sqrt 2) * r * norm (deriv (\<lambda>z. f (a + z) - f a) 0))
   4.196 +             \<subseteq> (\<lambda>z. f (a + z) - f a) ` ball 0 r"
   4.197 +    apply (rule Bloch_lemma_0)
   4.198 +    apply (simp_all add: \<open>0 < r\<close>)
   4.199 +    apply (simp add: fz complex_derivative_chain)
   4.200 +    apply (simp add: dist_norm le)
   4.201 +    done
   4.202 +  then show ?thesis
   4.203 +    apply clarify
   4.204 +    apply (drule_tac c="x - f a" in subsetD)
   4.205 +     apply (force simp: fz \<open>0 < r\<close> dist_norm complex_derivative_chain complex_differentiable_compose)+
   4.206 +    done
   4.207 +qed
   4.208 +
   4.209 +proposition Bloch_unit: 
   4.210 +  assumes holf: "f holomorphic_on ball a 1" and [simp]: "deriv f a = 1"
   4.211 +  obtains b r where "1/12 < r" "ball b r \<subseteq> f ` (ball a 1)"
   4.212 +proof -
   4.213 +  def r \<equiv> "249/256::real"
   4.214 +  have "0 < r" "r < 1" by (auto simp: r_def)
   4.215 +  def g \<equiv> "\<lambda>z. deriv f z * of_real(r - norm(z - a))"
   4.216 +  have "deriv f holomorphic_on ball a 1"
   4.217 +    by (rule holomorphic_deriv [OF holf open_ball])
   4.218 +  then have "continuous_on (ball a 1) (deriv f)"
   4.219 +    using holomorphic_on_imp_continuous_on by blast
   4.220 +  then have "continuous_on (cball a r) (deriv f)"
   4.221 +    by (rule continuous_on_subset) (simp add: cball_subset_ball_iff \<open>r < 1\<close>)
   4.222 +  then have "continuous_on (cball a r) g"
   4.223 +    by (simp add: g_def continuous_intros)
   4.224 +  then have 1: "compact (g ` cball a r)"
   4.225 +    by (rule compact_continuous_image [OF _ compact_cball])
   4.226 +  have 2: "g ` cball a r \<noteq> {}"
   4.227 +    using \<open>r > 0\<close> by auto
   4.228 +  obtain p where pr: "p \<in> cball a r" 
   4.229 +             and pge: "\<And>y. y \<in> cball a r \<Longrightarrow> norm (g y) \<le> norm (g p)"
   4.230 +    using distance_attains_sup [OF 1 2, of 0] by force
   4.231 +  def t \<equiv> "(r - norm(p - a)) / 2"
   4.232 +  have "norm (p - a) \<noteq> r"
   4.233 +    using pge [of a] \<open>r > 0\<close> by (auto simp: g_def norm_mult)
   4.234 +  then have "norm (p - a) < r" using pr 
   4.235 +    by (simp add: norm_minus_commute dist_norm)
   4.236 +  then have "0 < t" 
   4.237 +    by (simp add: t_def)
   4.238 +  have cpt: "cball p t \<subseteq> ball a r"
   4.239 +    using \<open>0 < t\<close> by (simp add: cball_subset_ball_iff dist_norm t_def field_simps)
   4.240 +  have gen_le_dfp: "norm (deriv f y) * (r - norm (y - a)) / (r - norm (p - a)) \<le> norm (deriv f p)" 
   4.241 +            if "y \<in> cball a r" for y
   4.242 +  proof -
   4.243 +    have [simp]: "norm (y - a) \<le> r"
   4.244 +      using that by (simp add: dist_norm norm_minus_commute) 
   4.245 +    have "norm (g y) \<le> norm (g p)"
   4.246 +      using pge [OF that] by simp
   4.247 +    then have "norm (deriv f y) * abs (r - norm (y - a)) \<le> norm (deriv f p) * abs (r - norm (p - a))"
   4.248 +      by (simp only: dist_norm g_def norm_mult norm_of_real)
   4.249 +    with that \<open>norm (p - a) < r\<close> show ?thesis
   4.250 +      by (simp add: dist_norm divide_simps)
   4.251 +  qed
   4.252 +  have le_norm_dfp: "r / (r - norm (p - a)) \<le> norm (deriv f p)"
   4.253 +    using gen_le_dfp [of a] \<open>r > 0\<close> by auto
   4.254 +  have 1: "f holomorphic_on cball p t"
   4.255 +    apply (rule holomorphic_on_subset [OF holf])
   4.256 +    using cpt \<open>r < 1\<close> order_subst1 subset_ball by auto
   4.257 +  have 2: "norm (deriv f z) \<le> 2 * norm (deriv f p)" if "z \<in> ball p t" for z
   4.258 +  proof -
   4.259 +    have z: "z \<in> cball a r"
   4.260 +      by (meson ball_subset_cball subsetD cpt that)
   4.261 +    then have "norm(z - a) < r"
   4.262 +      by (metis ball_subset_cball contra_subsetD cpt dist_norm mem_ball norm_minus_commute that)
   4.263 +    have "norm (deriv f z) * (r - norm (z - a)) / (r - norm (p - a)) \<le> norm (deriv f p)" 
   4.264 +      using gen_le_dfp [OF z] by simp
   4.265 +    with \<open>norm (z - a) < r\<close> \<open>norm (p - a) < r\<close> 
   4.266 +    have "norm (deriv f z) \<le> (r - norm (p - a)) / (r - norm (z - a)) * norm (deriv f p)"
   4.267 +       by (simp add: field_simps)
   4.268 +    also have "... \<le> 2 * norm (deriv f p)"
   4.269 +      apply (rule mult_right_mono)
   4.270 +      using that \<open>norm (p - a) < r\<close> \<open>norm(z - a) < r\<close> 
   4.271 +      apply (simp_all add: field_simps t_def dist_norm [symmetric])
   4.272 +      using dist_triangle3 [of z a p] by linarith
   4.273 +    finally show ?thesis .
   4.274 +  qed
   4.275 +  have sqrt2: "sqrt 2 < 2113/1494"
   4.276 +    by (rule real_less_lsqrt) (auto simp: power2_eq_square)
   4.277 +  then have sq3: "0 < 3 - 2 * sqrt 2" by simp
   4.278 +  have "1 / 12 / ((3 - 2 * sqrt 2) / 2) < r"
   4.279 +    using sq3 sqrt2 by (auto simp: field_simps r_def) 
   4.280 +  also have "... \<le> cmod (deriv f p) * (r - cmod (p - a))"
   4.281 +    using \<open>norm (p - a) < r\<close> le_norm_dfp   by (simp add: pos_divide_le_eq)    
   4.282 +  finally have "1 / 12 < cmod (deriv f p) * (r - cmod (p - a)) * ((3 - 2 * sqrt 2) / 2)"  
   4.283 +    using pos_divide_less_eq half_gt_zero_iff sq3 by blast
   4.284 +  then have **: "1 / 12 < (3 - 2 * sqrt 2) * t * norm (deriv f p)"
   4.285 +    using sq3 by (simp add: mult.commute t_def)
   4.286 +  have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball p t"
   4.287 +    by (rule Bloch_lemma [OF 1 \<open>0 < t\<close> 2])
   4.288 +  also have "... \<subseteq> f ` ball a 1"
   4.289 +    apply (rule image_mono)
   4.290 +    apply (rule order_trans [OF ball_subset_cball])
   4.291 +    apply (rule order_trans [OF cpt])
   4.292 +    using \<open>0 < t\<close> \<open>r < 1\<close> apply (simp add: ball_subset_ball_iff dist_norm)
   4.293 +    done
   4.294 +  finally have "ball (f p) ((3 - 2 * sqrt 2) * t * norm (deriv f p)) \<subseteq> f ` ball a 1" .
   4.295 +  with ** show ?thesis
   4.296 +    by (rule that)
   4.297 +qed
   4.298 +
   4.299 +
   4.300 +theorem Bloch:
   4.301 +  assumes holf: "f holomorphic_on ball a r" and "0 < r" 
   4.302 +      and r': "r' \<le> r * norm (deriv f a) / 12"
   4.303 +  obtains b where "ball b r' \<subseteq> f ` (ball a r)"
   4.304 +proof (cases "deriv f a = 0")
   4.305 +  case True with r' show ?thesis
   4.306 +    using ball_eq_empty that by fastforce
   4.307 +next
   4.308 +  case False
   4.309 +    def C \<equiv> "deriv f a"
   4.310 +    have "0 < norm C" using False by (simp add: C_def)
   4.311 +    have dfa: "f complex_differentiable at a"
   4.312 +      apply (rule holomorphic_on_imp_differentiable_at [OF holf])
   4.313 +      using \<open>0 < r\<close> by auto
   4.314 +    have fo: "(\<lambda>z. f (a + of_real r * z)) = f o (\<lambda>z. (a + of_real r * z))"
   4.315 +      by (simp add: o_def)
   4.316 +    have holf': "f holomorphic_on (\<lambda>z. a + complex_of_real r * z) ` ball 0 1"
   4.317 +      apply (rule holomorphic_on_subset [OF holf])
   4.318 +      using \<open>0 < r\<close> apply (force simp: dist_norm norm_mult)
   4.319 +      done
   4.320 +    have 1: "(\<lambda>z. f (a + r * z) / (C * r)) holomorphic_on ball 0 1"
   4.321 +      apply (rule holomorphic_intros holomorphic_on_compose holf' | simp add: fo)+
   4.322 +      using \<open>0 < r\<close> by (simp add: C_def False)
   4.323 +    have "((\<lambda>z. f (a + of_real r * z) / (C * of_real r)) has_field_derivative
   4.324 +          (deriv f (a + of_real r * z) / C)) (at z)" 
   4.325 +         if "norm z < 1" for z
   4.326 +    proof -
   4.327 +    have *: "((\<lambda>x. f (a + of_real r * x)) has_field_derivative
   4.328 +             (deriv f (a + of_real r * z) * of_real r)) (at z)"
   4.329 +        apply (simp add: fo)
   4.330 +        apply (rule DERIV_chain [OF complex_differentiable_derivI])
   4.331 +        apply (rule holomorphic_on_imp_differentiable_at [OF holf], simp)
   4.332 +        using \<open>0 < r\<close> apply (simp add: dist_norm norm_mult that)
   4.333 +        apply (rule derivative_eq_intros | simp)+
   4.334 +        done
   4.335 +      show ?thesis
   4.336 +        apply (rule derivative_eq_intros * | simp)+
   4.337 +        using \<open>0 < r\<close> by (auto simp: C_def False)
   4.338 +    qed
   4.339 +    have 2: "deriv (\<lambda>z. f (a + of_real r * z) / (C * of_real r)) 0 = 1"
   4.340 +      apply (subst complex_derivative_cdivide_right)
   4.341 +      apply (simp add: complex_differentiable_def fo)
   4.342 +      apply (rule exI)
   4.343 +      apply (rule DERIV_chain [OF complex_differentiable_derivI])
   4.344 +      apply (simp add: dfa)
   4.345 +      apply (rule derivative_eq_intros | simp add: C_def False fo)+
   4.346 +      using \<open>0 < r\<close> 
   4.347 +      apply (simp add: C_def False fo)
   4.348 +      apply (simp add: derivative_intros dfa complex_derivative_chain)
   4.349 +      done
   4.350 +    have sb1: "op * (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1 
   4.351 +               \<subseteq> f ` ball a r"
   4.352 +      using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
   4.353 +    have sb2: "ball (C * r * b) r' \<subseteq> op * (C * r) ` ball b t" 
   4.354 +               if "1 / 12 < t" for b t
   4.355 +    proof -
   4.356 +      have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
   4.357 +        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 
   4.358 +        by auto
   4.359 +      show ?thesis
   4.360 +        apply clarify
   4.361 +        apply (rule_tac x="x / (C * r)" in image_eqI)
   4.362 +        using \<open>0 < r\<close>  
   4.363 +        apply (simp_all add: dist_norm norm_mult norm_divide C_def False field_simps)
   4.364 +        apply (erule less_le_trans)
   4.365 +        apply (rule order_trans [OF r' *])
   4.366 +        done
   4.367 +    qed
   4.368 +    show ?thesis
   4.369 +      apply (rule Bloch_unit [OF 1 2])
   4.370 +      apply (rename_tac t)
   4.371 +      apply (rule_tac b="(C * of_real r) * b" in that)
   4.372 +      apply (drule image_mono [where f = "\<lambda>z. (C * of_real r) * z"])
   4.373 +      using sb1 sb2
   4.374 +      apply force
   4.375 +      done
   4.376 +qed
   4.377 +
   4.378 +corollary Bloch_general:
   4.379 +  assumes holf: "f holomorphic_on s" and "a \<in> s" 
   4.380 +      and tle: "\<And>z. z \<in> frontier s \<Longrightarrow> t \<le> dist a z"
   4.381 +      and rle: "r \<le> t * norm(deriv f a) / 12"
   4.382 +  obtains b where "ball b r \<subseteq> f ` s"
   4.383 +proof -
   4.384 +  consider "r \<le> 0" | "0 < t * norm(deriv f a) / 12" using rle by force
   4.385 +  then show ?thesis
   4.386 +  proof cases
   4.387 +    case 1 then show ?thesis
   4.388 +      by (simp add: Topology_Euclidean_Space.ball_empty that)
   4.389 +  next
   4.390 +    case 2
   4.391 +    show ?thesis
   4.392 +    proof (cases "deriv f a = 0")
   4.393 +      case True then show ?thesis
   4.394 +        using rle by (simp add: Topology_Euclidean_Space.ball_empty that)
   4.395 +    next
   4.396 +      case False
   4.397 +      then have "t > 0"
   4.398 +        using 2 by (force simp: zero_less_mult_iff)
   4.399 +      have "~ ball a t \<subseteq> s \<Longrightarrow> ball a t \<inter> frontier s \<noteq> {}"
   4.400 +        apply (rule connected_Int_frontier [of "ball a t" s], simp_all)
   4.401 +        using \<open>0 < t\<close> \<open>a \<in> s\<close> centre_in_ball apply blast
   4.402 +        done
   4.403 +      with tle have *: "ball a t \<subseteq> s" by fastforce
   4.404 +      then have 1: "f holomorphic_on ball a t"
   4.405 +        using holf using holomorphic_on_subset by blast
   4.406 +      show ?thesis
   4.407 +        apply (rule Bloch [OF 1 \<open>t > 0\<close> rle])
   4.408 +        apply (rule_tac b=b in that)
   4.409 +        using * apply force
   4.410 +        done
   4.411 +    qed
   4.412 +  qed
   4.413 +qed
   4.414 +
   4.415  end
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 07 08:14:18 2016 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Mar 07 14:34:45 2016 +0000
     5.3 @@ -5277,7 +5277,7 @@
     5.4      proof -
     5.5        assume "v < 1"
     5.6        then show False
     5.7 -        using v(3)[THEN spec[where x=1]] using x and fs by auto
     5.8 +        using v(3)[THEN spec[where x=1]] using x fs by (simp add: pth_1 subset_iff)
     5.9      next
    5.10        assume "v > 1"
    5.11        then show False
    5.12 @@ -5294,8 +5294,7 @@
    5.13        apply (cases "u = 1")
    5.14          using assms(3)[THEN bspec[where x=x], THEN spec[where x=u]]
    5.15          using \<open>0\<le>u\<close> and x and fs
    5.16 -        apply auto
    5.17 -        done
    5.18 +        by auto
    5.19      qed auto
    5.20    qed
    5.21  
    5.22 @@ -9866,7 +9865,7 @@
    5.23      apply (rule le_setdistI, blast)
    5.24      using False apply (fastforce intro: le_setdistI)
    5.25      apply (simp add: algebra_simps)
    5.26 -    apply (metis dist_commute dist_triangle_alt order_trans [OF setdist_le_dist])
    5.27 +    apply (metis dist_commute dist_triangle3 order_trans [OF setdist_le_dist])
    5.28      done
    5.29    then have "setdist s t - setdist {a} t \<le> setdist s {a}"
    5.30      using False by (fastforce intro: le_setdistI)
     6.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 07 08:14:18 2016 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 07 14:34:45 2016 +0000
     6.3 @@ -194,6 +194,9 @@
     6.4    unfolding differentiable_def
     6.5    by auto
     6.6  
     6.7 +lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
     6.8 +  using differentiable_on_def by blast
     6.9 +
    6.10  lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
    6.11    unfolding differentiable_def
    6.12    using has_derivative_at_within
     7.1 --- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Mar 07 08:14:18 2016 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Mar 07 14:34:45 2016 +0000
     7.3 @@ -1384,6 +1384,8 @@
     7.4  
     7.5  
     7.6  lemma complex_differentiable_Polygamma:
     7.7 +  fixes z::complex
     7.8 +  shows
     7.9    "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Polygamma n complex_differentiable (at z within A)"
    7.10    using has_field_derivative_Polygamma[of z n] unfolding complex_differentiable_def by auto
    7.11  
     8.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 07 08:14:18 2016 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 07 14:34:45 2016 +0000
     8.3 @@ -2501,6 +2501,12 @@
     8.4    shows "integral s (\<lambda>x. c * f x) = c * integral s f"
     8.5  by (simp add: mult.commute [of c])
     8.6  
     8.7 +corollary integral_divide [simp]:
     8.8 +  fixes z :: "'a::real_normed_field"
     8.9 +  shows "integral S (\<lambda>x. f x / z) = integral S (\<lambda>x. f x) / z"
    8.10 +using integral_mult_left [of S f "inverse z"]
    8.11 +  by (simp add: divide_inverse_commute)
    8.12 +
    8.13  lemma has_integral_mult_right:
    8.14    fixes c :: "'a :: real_normed_algebra"
    8.15    shows "(f has_integral y) i \<Longrightarrow> ((\<lambda>x. c * f x) has_integral (c * y)) i"
    8.16 @@ -2681,6 +2687,12 @@
    8.17    using integrable_cmul[of "\<lambda>x. c * f x" s "1 / c"] integrable_cmul[of f s c] \<open>c \<noteq> 0\<close>
    8.18    by auto
    8.19  
    8.20 +lemma integrable_on_cmult_left:
    8.21 +  assumes "f integrable_on s"
    8.22 +  shows "(\<lambda>x. of_real c * f x) integrable_on s"
    8.23 +    using integrable_cmul[of f s "of_real c"] assms
    8.24 +    by (simp add: scaleR_conv_of_real)
    8.25 +
    8.26  lemma integrable_neg: "f integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) integrable_on s"
    8.27    unfolding integrable_on_def by(auto intro: has_integral_neg)
    8.28  
    8.29 @@ -2756,6 +2768,45 @@
    8.30    unfolding integral_def
    8.31  by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)
    8.32  
    8.33 +lemma integrable_on_cmult_left_iff [simp]:
    8.34 +  assumes "c \<noteq> 0"
    8.35 +  shows "(\<lambda>x. of_real c * f x) integrable_on s \<longleftrightarrow> f integrable_on s"
    8.36 +        (is "?lhs = ?rhs")
    8.37 +proof
    8.38 +  assume ?lhs
    8.39 +  then have "(\<lambda>x. of_real (1 / c) * (of_real c * f x)) integrable_on s"
    8.40 +    using integrable_cmul[of "\<lambda>x. of_real c * f x" s "1 / of_real c"]
    8.41 +    by (simp add: scaleR_conv_of_real)
    8.42 +  then have "(\<lambda>x. (of_real (1 / c) * of_real c * f x)) integrable_on s"
    8.43 +    by (simp add: algebra_simps)
    8.44 +  with \<open>c \<noteq> 0\<close> show ?rhs
    8.45 +    by (metis (no_types, lifting) integrable_eq mult.left_neutral nonzero_divide_eq_eq of_real_1 of_real_mult)
    8.46 +qed (blast intro: integrable_on_cmult_left)
    8.47 +
    8.48 +lemma integrable_on_cmult_right:
    8.49 +  fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
    8.50 +  assumes "f integrable_on s"
    8.51 +  shows "(\<lambda>x. f x * of_real c) integrable_on s"
    8.52 +using integrable_on_cmult_left [OF assms] by (simp add: mult.commute)
    8.53 +
    8.54 +lemma integrable_on_cmult_right_iff [simp]:
    8.55 +  fixes f :: "_ \<Rightarrow> 'b :: {comm_ring,real_algebra_1,real_normed_vector}"
    8.56 +  assumes "c \<noteq> 0"
    8.57 +  shows "(\<lambda>x. f x * of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
    8.58 +using integrable_on_cmult_left_iff [OF assms] by (simp add: mult.commute)
    8.59 +
    8.60 +lemma integrable_on_cdivide:
    8.61 +  fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
    8.62 +  assumes "f integrable_on s"
    8.63 +  shows "(\<lambda>x. f x / of_real c) integrable_on s"
    8.64 +by (simp add: integrable_on_cmult_right divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
    8.65 +
    8.66 +lemma integrable_on_cdivide_iff [simp]:
    8.67 +  fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
    8.68 +  assumes "c \<noteq> 0"
    8.69 +  shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
    8.70 +by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
    8.71 +
    8.72  lemma has_integral_null [intro]:
    8.73    assumes "content(cbox a b) = 0"
    8.74    shows "(f has_integral 0) (cbox a b)"
    8.75 @@ -6065,6 +6116,30 @@
    8.76    qed
    8.77  qed
    8.78  
    8.79 +lemma ident_has_integral:
    8.80 +  fixes a::real
    8.81 +  assumes "a \<le> b"
    8.82 +  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2) / 2) {a..b}"
    8.83 +proof -
    8.84 +  have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
    8.85 +    apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
    8.86 +    unfolding power2_eq_square
    8.87 +    by (rule derivative_eq_intros | simp)+
    8.88 +  then show ?thesis
    8.89 +    by (simp add: field_simps)
    8.90 +qed
    8.91 +
    8.92 +lemma integral_ident [simp]:
    8.93 +  fixes a::real
    8.94 +  assumes "a \<le> b"
    8.95 +  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
    8.96 +using ident_has_integral integral_unique by fastforce
    8.97 +
    8.98 +lemma ident_integrable_on:
    8.99 +  fixes a::real
   8.100 +  shows "(\<lambda>x. x) integrable_on {a..b}"
   8.101 +by (metis atLeastatMost_empty_iff integrable_on_def has_integral_empty ident_has_integral)
   8.102 +
   8.103  
   8.104  subsection \<open>Taylor series expansion\<close>
   8.105  
   8.106 @@ -6737,27 +6812,18 @@
   8.107  lemma content_image_affinity_cbox:
   8.108    "content((\<lambda>x::'a::euclidean_space. m *\<^sub>R x + c) ` cbox a b) =
   8.109      \<bar>m\<bar> ^ DIM('a) * content (cbox a b)" (is "?l = ?r")
   8.110 -proof -
   8.111 -  {
   8.112 -    presume *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
   8.113 -    show ?thesis
   8.114 -      apply cases
   8.115 -      apply (rule *)
   8.116 -      apply assumption
   8.117 -      unfolding not_not
   8.118 -      using content_empty
   8.119 -      apply auto
   8.120 -      done
   8.121 -  }
   8.122 -  assume as: "cbox a b \<noteq> {}"
   8.123 +proof (cases "cbox a b = {}")
   8.124 +  case True then show ?thesis by simp
   8.125 +next
   8.126 +  case False
   8.127    show ?thesis
   8.128    proof (cases "m \<ge> 0")
   8.129      case True
   8.130 -    with as have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
   8.131 +    with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) \<noteq> {}"
   8.132        unfolding box_ne_empty
   8.133        apply (intro ballI)
   8.134        apply (erule_tac x=i in ballE)
   8.135 -      apply (auto simp: inner_simps intro!: mult_left_mono)
   8.136 +      apply (auto simp: inner_simps mult_left_mono)
   8.137        done
   8.138      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"
   8.139        by (simp add: inner_simps field_simps)
   8.140 @@ -6766,11 +6832,11 @@
   8.141          setprod.distrib setprod_constant inner_diff_left)
   8.142    next
   8.143      case False
   8.144 -    with as have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
   8.145 +    with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
   8.146        unfolding box_ne_empty
   8.147        apply (intro ballI)
   8.148        apply (erule_tac x=i in ballE)
   8.149 -      apply (auto simp: inner_simps intro!: mult_left_mono)
   8.150 +      apply (auto simp: inner_simps mult_left_mono)
   8.151        done
   8.152      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"
   8.153        by (simp add: inner_simps field_simps)
     9.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 07 08:14:18 2016 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Mar 07 14:34:45 2016 +0000
     9.3 @@ -556,6 +556,190 @@
     9.4    by (rule ext) (auto simp: mult.commute)
     9.5  
     9.6  
     9.7 +subsection\<open>Some reversed and "if and only if" versions of joining theorems\<close>
     9.8 +
     9.9 +lemma path_join_path_ends: 
    9.10 +  fixes g1 :: "real \<Rightarrow> 'a::metric_space"
    9.11 +  assumes "path(g1 +++ g2)" "path g2" 
    9.12 +    shows "pathfinish g1 = pathstart g2"
    9.13 +proof (rule ccontr)
    9.14 +  def e \<equiv> "dist (g1 1) (g2 0)"
    9.15 +  assume Neg: "pathfinish g1 \<noteq> pathstart g2"
    9.16 +  then have "0 < dist (pathfinish g1) (pathstart g2)"
    9.17 +    by auto
    9.18 +  then have "e > 0"
    9.19 +    by (metis e_def pathfinish_def pathstart_def) 
    9.20 +  then obtain d1 where "d1 > 0" 
    9.21 +       and d1: "\<And>x'. \<lbrakk>x'\<in>{0..1}; norm x' < d1\<rbrakk> \<Longrightarrow> dist (g2 x') (g2 0) < e/2"
    9.22 +    using assms(2) unfolding path_def continuous_on_iff
    9.23 +    apply (drule_tac x=0 in bspec, simp)
    9.24 +    by (metis half_gt_zero_iff norm_conv_dist)
    9.25 +  obtain d2 where "d2 > 0" 
    9.26 +       and d2: "\<And>x'. \<lbrakk>x'\<in>{0..1}; dist x' (1/2) < d2\<rbrakk> 
    9.27 +                      \<Longrightarrow> dist ((g1 +++ g2) x') (g1 1) < e/2"
    9.28 +    using assms(1) \<open>e > 0\<close> unfolding path_def continuous_on_iff
    9.29 +    apply (drule_tac x="1/2" in bspec, simp)
    9.30 +    apply (drule_tac x="e/2" in spec)
    9.31 +    apply (force simp: joinpaths_def)
    9.32 +    done
    9.33 +  have int01_1: "min (1/2) (min d1 d2) / 2 \<in> {0..1}"
    9.34 +    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
    9.35 +  have dist1: "norm (min (1 / 2) (min d1 d2) / 2) < d1"
    9.36 +    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
    9.37 +  have int01_2: "1/2 + min (1/2) (min d1 d2) / 4 \<in> {0..1}"
    9.38 +    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
    9.39 +  have dist2: "dist (1 / 2 + min (1 / 2) (min d1 d2) / 4) (1 / 2) < d2"
    9.40 +    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def dist_norm)
    9.41 +  have [simp]: "~ min (1 / 2) (min d1 d2) \<le> 0"
    9.42 +    using \<open>d1 > 0\<close> \<open>d2 > 0\<close> by (simp add: min_def)
    9.43 +  have "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g1 1) < e/2"
    9.44 +       "dist (g2 (min (1 / 2) (min d1 d2) / 2)) (g2 0) < e/2"
    9.45 +    using d1 [OF int01_1 dist1] d2 [OF int01_2 dist2] by (simp_all add: joinpaths_def)
    9.46 +  then have "dist (g1 1) (g2 0) < e/2 + e/2"
    9.47 +    using dist_triangle_half_r e_def by blast
    9.48 +  then show False 
    9.49 +    by (simp add: e_def [symmetric])
    9.50 +qed
    9.51 +
    9.52 +lemma path_join_eq [simp]:  
    9.53 +  fixes g1 :: "real \<Rightarrow> 'a::metric_space"
    9.54 +  assumes "path g1" "path g2"
    9.55 +    shows "path(g1 +++ g2) \<longleftrightarrow> pathfinish g1 = pathstart g2"
    9.56 +  using assms by (metis path_join_path_ends path_join_imp)
    9.57 +
    9.58 +lemma simple_path_joinE: 
    9.59 +  assumes "simple_path(g1 +++ g2)" and "pathfinish g1 = pathstart g2"
    9.60 +  obtains "arc g1" "arc g2" 
    9.61 +          "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
    9.62 +proof -
    9.63 +  have *: "\<And>x y. \<lbrakk>0 \<le> x; x \<le> 1; 0 \<le> y; y \<le> 1; (g1 +++ g2) x = (g1 +++ g2) y\<rbrakk> 
    9.64 +               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
    9.65 +    using assms by (simp add: simple_path_def)
    9.66 +  have "path g1" 
    9.67 +    using assms path_join simple_path_imp_path by blast
    9.68 +  moreover have "inj_on g1 {0..1}"
    9.69 +  proof (clarsimp simp: inj_on_def)
    9.70 +    fix x y
    9.71 +    assume "g1 x = g1 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
    9.72 +    then show "x = y"
    9.73 +      using * [of "x/2" "y/2"] by (simp add: joinpaths_def split_ifs)
    9.74 +  qed
    9.75 +  ultimately have "arc g1"
    9.76 +    using assms  by (simp add: arc_def)
    9.77 +  have [simp]: "g2 0 = g1 1"
    9.78 +    using assms by (metis pathfinish_def pathstart_def) 
    9.79 +  have "path g2"
    9.80 +    using assms path_join simple_path_imp_path by blast
    9.81 +  moreover have "inj_on g2 {0..1}"
    9.82 +  proof (clarsimp simp: inj_on_def)
    9.83 +    fix x y
    9.84 +    assume "g2 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1"
    9.85 +    then show "x = y"
    9.86 +      using * [of "(x + 1) / 2" "(y + 1) / 2"]
    9.87 +      by (force simp: joinpaths_def split_ifs divide_simps)
    9.88 +  qed
    9.89 +  ultimately have "arc g2"
    9.90 +    using assms  by (simp add: arc_def)
    9.91 +  have "g2 y = g1 0 \<or> g2 y = g1 1" 
    9.92 +       if "g1 x = g2 y" "0 \<le> x" "x \<le> 1" "0 \<le> y" "y \<le> 1" for x y
    9.93 +      using * [of "x / 2" "(y + 1) / 2"] that
    9.94 +      by (auto simp: joinpaths_def split_ifs divide_simps)
    9.95 +  then have "path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
    9.96 +    by (fastforce simp: pathstart_def pathfinish_def path_image_def)
    9.97 +  with \<open>arc g1\<close> \<open>arc g2\<close> show ?thesis using that by blast
    9.98 +qed
    9.99 +
   9.100 +lemma simple_path_join_loop_eq:
   9.101 +  assumes "pathfinish g2 = pathstart g1" "pathfinish g1 = pathstart g2" 
   9.102 +    shows "simple_path(g1 +++ g2) \<longleftrightarrow>
   9.103 +             arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g1, pathstart g2}"
   9.104 +by (metis assms simple_path_joinE simple_path_join_loop)
   9.105 +
   9.106 +lemma arc_join_eq:
   9.107 +  assumes "pathfinish g1 = pathstart g2" 
   9.108 +    shows "arc(g1 +++ g2) \<longleftrightarrow>
   9.109 +           arc g1 \<and> arc g2 \<and> path_image g1 \<inter> path_image g2 \<subseteq> {pathstart g2}"
   9.110 +           (is "?lhs = ?rhs")
   9.111 +proof 
   9.112 +  assume ?lhs
   9.113 +  then have "simple_path(g1 +++ g2)" by (rule arc_imp_simple_path)
   9.114 +  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> 
   9.115 +               \<Longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0"
   9.116 +    using assms by (simp add: simple_path_def)
   9.117 +  have False if "g1 0 = g2 u" "0 \<le> u" "u \<le> 1" for u
   9.118 +    using * [of 0 "(u + 1) / 2"] that assms arc_distinct_ends [OF \<open>?lhs\<close>]
   9.119 +    by (auto simp: joinpaths_def pathstart_def pathfinish_def split_ifs divide_simps)
   9.120 +  then have n1: "~ (pathstart g1 \<in> path_image g2)"
   9.121 +    unfolding pathstart_def path_image_def
   9.122 +    using atLeastAtMost_iff by blast
   9.123 +  show ?rhs using \<open>?lhs\<close>
   9.124 +    apply (rule simple_path_joinE [OF arc_imp_simple_path assms])
   9.125 +    using n1 by force
   9.126 +next
   9.127 +  assume ?rhs then show ?lhs
   9.128 +    using assms
   9.129 +    by (fastforce simp: pathfinish_def pathstart_def intro!: arc_join)
   9.130 +qed
   9.131 +
   9.132 +lemma arc_join_eq_alt: 
   9.133 +        "pathfinish g1 = pathstart g2
   9.134 +        \<Longrightarrow> (arc(g1 +++ g2) \<longleftrightarrow>
   9.135 +             arc g1 \<and> arc g2 \<and>
   9.136 +             path_image g1 \<inter> path_image g2 = {pathstart g2})"
   9.137 +using pathfinish_in_path_image by (fastforce simp: arc_join_eq)
   9.138 +
   9.139 +
   9.140 +subsection\<open>The joining of paths is associative\<close>
   9.141 +
   9.142 +lemma path_assoc:
   9.143 +    "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
   9.144 +     \<Longrightarrow> path(p +++ (q +++ r)) \<longleftrightarrow> path((p +++ q) +++ r)"
   9.145 +by simp
   9.146 +
   9.147 +lemma simple_path_assoc: 
   9.148 +  assumes "pathfinish p = pathstart q" "pathfinish q = pathstart r" 
   9.149 +    shows "simple_path (p +++ (q +++ r)) \<longleftrightarrow> simple_path ((p +++ q) +++ r)"
   9.150 +proof (cases "pathstart p = pathfinish r")
   9.151 +  case True show ?thesis
   9.152 +  proof
   9.153 +    assume "simple_path (p +++ q +++ r)"
   9.154 +    with assms True show "simple_path ((p +++ q) +++ r)"
   9.155 +      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join 
   9.156 +                    dest: arc_distinct_ends [of r])
   9.157 +  next
   9.158 +    assume 0: "simple_path ((p +++ q) +++ r)"
   9.159 +    with assms True have q: "pathfinish r \<notin> path_image q"
   9.160 +      using arc_distinct_ends  
   9.161 +      by (fastforce simp add: simple_path_join_loop_eq arc_join_eq path_image_join)
   9.162 +    have "pathstart r \<notin> path_image p"
   9.163 +      using assms
   9.164 +      by (metis 0 IntI arc_distinct_ends arc_join_eq_alt empty_iff insert_iff 
   9.165 +              pathfinish_in_path_image pathfinish_join simple_path_joinE)
   9.166 +    with assms 0 q True show "simple_path (p +++ q +++ r)"
   9.167 +      by (auto simp: simple_path_join_loop_eq arc_join_eq path_image_join 
   9.168 +               dest!: subsetD [OF _ IntI])
   9.169 +  qed
   9.170 +next
   9.171 +  case False
   9.172 +  { fix x :: 'a
   9.173 +    assume a: "path_image p \<inter> path_image q \<subseteq> {pathstart q}"
   9.174 +              "(path_image p \<union> path_image q) \<inter> path_image r \<subseteq> {pathstart r}"
   9.175 +              "x \<in> path_image p" "x \<in> path_image r"
   9.176 +    have "pathstart r \<in> path_image q"
   9.177 +      by (metis assms(2) pathfinish_in_path_image)
   9.178 +    with a have "x = pathstart q"
   9.179 +      by blast
   9.180 +  }
   9.181 +  with False assms show ?thesis 
   9.182 +    by (auto simp: simple_path_eq_arc simple_path_join_loop_eq arc_join_eq path_image_join)
   9.183 +qed
   9.184 +
   9.185 +lemma arc_assoc: 
   9.186 +     "\<lbrakk>pathfinish p = pathstart q; pathfinish q = pathstart r\<rbrakk>
   9.187 +      \<Longrightarrow> arc(p +++ (q +++ r)) \<longleftrightarrow> arc((p +++ q) +++ r)"
   9.188 +by (simp add: arc_simple_path simple_path_assoc)
   9.189 +
   9.190 +
   9.191  section\<open>Choosing a subpath of an existing path\<close>
   9.192  
   9.193  definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
   9.194 @@ -2526,6 +2710,58 @@
   9.195    apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
   9.196    by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
   9.197  
   9.198 +subsection\<open>Condition for an open map's image to contain a ball\<close>
   9.199 +
   9.200 +lemma ball_subset_open_map_image:
   9.201 +  fixes f :: "'a::heine_borel \<Rightarrow> 'b :: {real_normed_vector,heine_borel}"
   9.202 +  assumes contf: "continuous_on (closure S) f"
   9.203 +      and oint: "open (f ` interior S)"
   9.204 +      and le_no: "\<And>z. z \<in> frontier S \<Longrightarrow> r \<le> norm(f z - f a)"
   9.205 +      and "bounded S" "a \<in> S" "0 < r"
   9.206 +    shows "ball (f a) r \<subseteq> f ` S"
   9.207 +proof (cases "f ` S = UNIV")
   9.208 +  case True then show ?thesis by simp
   9.209 +next
   9.210 +  case False
   9.211 +    obtain w where w: "w \<in> frontier (f ` S)"
   9.212 +               and dw_le: "\<And>y. y \<in> frontier (f ` S) \<Longrightarrow> norm (f a - w) \<le> norm (f a - y)"
   9.213 +      apply (rule distance_attains_inf [of "frontier(f ` S)" "f a"])
   9.214 +      using \<open>a \<in> S\<close> by (auto simp: frontier_eq_empty dist_norm False)
   9.215 +    then obtain \<xi> where \<xi>: "\<And>n. \<xi> n \<in> f ` S" and tendsw: "\<xi> \<longlonglongrightarrow> w"
   9.216 +      by (metis Diff_iff frontier_def closure_sequential)
   9.217 +    then have "\<And>n. \<exists>x \<in> S. \<xi> n = f x" by force
   9.218 +    then obtain z where zs: "\<And>n. z n \<in> S" and fz: "\<And>n. \<xi> n = f (z n)"
   9.219 +      by metis
   9.220 +    then obtain y K where y: "y \<in> closure S" and "subseq K" and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
   9.221 +      using \<open>bounded S\<close>
   9.222 +      apply (simp add: compact_closure [symmetric] compact_def)
   9.223 +      apply (drule_tac x=z in spec)
   9.224 +      using closure_subset apply force
   9.225 +      done
   9.226 +    then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
   9.227 +      by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
   9.228 +    have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
   9.229 +    have "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
   9.230 +      using fz by auto
   9.231 +    moreover then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
   9.232 +      by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
   9.233 +    ultimately have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
   9.234 +    have rle: "r \<le> norm (f y - f a)"
   9.235 +      apply (rule le_no)
   9.236 +      using w wy oint
   9.237 +      by (force simp: imageI image_mono interiorI interior_subset frontier_def y)
   9.238 +    have **: "(~(b \<inter> (- S) = {}) \<and> ~(b - (- S) = {}) \<Longrightarrow> (b \<inter> f \<noteq> {}))
   9.239 +              \<Longrightarrow> (b \<inter> S \<noteq> {}) \<Longrightarrow> b \<inter> f = {} \<Longrightarrow>
   9.240 +              b \<subseteq> S" for b f and S :: "'b set" 
   9.241 +      by blast
   9.242 +    show ?thesis
   9.243 +      apply (rule **)   (*such a horrible mess*)
   9.244 +      apply (rule connected_Int_frontier [where t = "f`S", OF connected_ball])
   9.245 +      using \<open>a \<in> S\<close> \<open>0 < r\<close> 
   9.246 +      apply (auto simp: disjoint_iff_not_equal  dist_norm)
   9.247 +      by (metis dw_le norm_minus_commute not_less order_trans rle wy)
   9.248 +qed
   9.249 +
   9.250  section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
   9.251  
   9.252  text\<open> We often just want to require that it fixes some subset, but to take in
    10.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 07 08:14:18 2016 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 07 14:34:45 2016 +0000
    10.3 @@ -859,6 +859,24 @@
    10.4  lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
    10.5    by (auto simp: cball_def ball_def dist_commute)
    10.6  
    10.7 +lemma image_add_ball [simp]:
    10.8 +  fixes a :: "'a::real_normed_vector"
    10.9 +  shows "op + b ` ball a r = ball (a+b) r"
   10.10 +apply (intro equalityI subsetI)
   10.11 +apply (force simp: dist_norm)
   10.12 +apply (rule_tac x="x-b" in image_eqI)
   10.13 +apply (auto simp: dist_norm algebra_simps)
   10.14 +done
   10.15 +
   10.16 +lemma image_add_cball [simp]:
   10.17 +  fixes a :: "'a::real_normed_vector"
   10.18 +  shows "op + b ` cball a r = cball (a+b) r"
   10.19 +apply (intro equalityI subsetI)
   10.20 +apply (force simp: dist_norm)
   10.21 +apply (rule_tac x="x-b" in image_eqI)
   10.22 +apply (auto simp: dist_norm algebra_simps)
   10.23 +done
   10.24 +
   10.25  lemma open_ball [intro, simp]: "open (ball x e)"
   10.26  proof -
   10.27    have "open (dist x -` {..<e})"
   10.28 @@ -2191,7 +2209,7 @@
   10.29  
   10.30  definition "frontier S = closure S - interior S"
   10.31  
   10.32 -lemma frontier_closed: "closed (frontier S)"
   10.33 +lemma frontier_closed [iff]: "closed (frontier S)"
   10.34    by (simp add: frontier_def closed_Diff)
   10.35  
   10.36  lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
   10.37 @@ -2202,11 +2220,11 @@
   10.38    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))"
   10.39    unfolding frontier_def closure_interior
   10.40    by (auto simp add: mem_interior subset_eq ball_def)
   10.41 -
   10.42 +                                               
   10.43  lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
   10.44    by (metis frontier_def closure_closed Diff_subset)
   10.45  
   10.46 -lemma frontier_empty[simp]: "frontier {} = {}"
   10.47 +lemma frontier_empty [simp]: "frontier {} = {}"
   10.48    by (simp add: frontier_def)
   10.49  
   10.50  lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
   10.51 @@ -2221,7 +2239,7 @@
   10.52    then show ?thesis using frontier_subset_closed[of S] ..
   10.53  qed
   10.54  
   10.55 -lemma frontier_complement  [simp]: "frontier (- S) = frontier S"
   10.56 +lemma frontier_complement [simp]: "frontier (- S) = frontier S"
   10.57    by (auto simp add: frontier_def closure_complement interior_complement)
   10.58  
   10.59  lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
   10.60 @@ -4465,6 +4483,11 @@
   10.61      by auto
   10.62  qed
   10.63  
   10.64 +lemma compact_closure [simp]:
   10.65 +  fixes S :: "'a::heine_borel set"
   10.66 +  shows "compact(closure S) \<longleftrightarrow> bounded S"
   10.67 +by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
   10.68 +
   10.69  lemma compact_components:
   10.70    fixes s :: "'a::heine_borel set"
   10.71    shows "\<lbrakk>compact s; c \<in> components s\<rbrakk> \<Longrightarrow> compact c"
   10.72 @@ -5541,10 +5564,6 @@
   10.73  
   10.74  subsubsection \<open>Structural rules for pointwise continuity\<close>
   10.75  
   10.76 -lemmas continuous_within_id = continuous_ident
   10.77 -
   10.78 -lemmas continuous_at_id = continuous_ident
   10.79 -
   10.80  lemma continuous_infdist[continuous_intros]:
   10.81    assumes "continuous F f"
   10.82    shows "continuous F (\<lambda>x. infdist (f x) A)"
   10.83 @@ -5890,6 +5909,111 @@
   10.84    qed
   10.85  qed
   10.86  
   10.87 +subsection\<open> Theorems relating continuity and uniform continuity to closures\<close>
   10.88 +
   10.89 +lemma continuous_on_closure:
   10.90 +   "continuous_on (closure S) f \<longleftrightarrow>
   10.91 +    (\<forall>x e. x \<in> closure S \<and> 0 < e
   10.92 +           \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"
   10.93 +   (is "?lhs = ?rhs")
   10.94 +proof
   10.95 +  assume ?lhs then show ?rhs
   10.96 +    unfolding continuous_on_iff  by (metis Un_iff closure_def)
   10.97 +next
   10.98 +  assume R [rule_format]: ?rhs
   10.99 +  show ?lhs
  10.100 +  proof
  10.101 +    fix x and e::real
  10.102 +    assume "0 < e" and x: "x \<in> closure S"
  10.103 +    obtain \<delta>::real where "\<delta> > 0" 
  10.104 +                   and \<delta>: "\<And>y. \<lbrakk>y \<in> S; dist y x < \<delta>\<rbrakk> \<Longrightarrow> dist (f y) (f x) < e/2"
  10.105 +      using R [of x "e/2"] \<open>0 < e\<close> x by auto 
  10.106 +    have "dist (f y) (f x) \<le> e" if y: "y \<in> closure S" and dyx: "dist y x < \<delta>/2" for y
  10.107 +    proof -
  10.108 +      obtain \<delta>'::real where "\<delta>' > 0" 
  10.109 +                      and \<delta>': "\<And>z. \<lbrakk>z \<in> S; dist z y < \<delta>'\<rbrakk> \<Longrightarrow> dist (f z) (f y) < e/2"
  10.110 +        using R [of y "e/2"] \<open>0 < e\<close> y by auto 
  10.111 +      obtain z where "z \<in> S" and z: "dist z y < min \<delta>' \<delta> / 2"
  10.112 +        using closure_approachable y
  10.113 +        by (metis \<open>0 < \<delta>'\<close> \<open>0 < \<delta>\<close> divide_pos_pos min_less_iff_conj zero_less_numeral)
  10.114 +      have "dist (f z) (f y) < e/2"
  10.115 +        apply (rule \<delta>' [OF \<open>z \<in> S\<close>])
  10.116 +        using z \<open>0 < \<delta>'\<close> by linarith 
  10.117 +      moreover have "dist (f z) (f x) < e/2"
  10.118 +        apply (rule \<delta> [OF \<open>z \<in> S\<close>])
  10.119 +        using z \<open>0 < \<delta>\<close>  dist_commute[of y z] dist_triangle_half_r [of y] dyx by auto 
  10.120 +      ultimately show ?thesis
  10.121 +        by (metis dist_commute dist_triangle_half_l less_imp_le)
  10.122 +    qed
  10.123 +    then show "\<exists>d>0. \<forall>x'\<in>closure S. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
  10.124 +      by (rule_tac x="\<delta>/2" in exI) (simp add: \<open>\<delta> > 0\<close>)
  10.125 +  qed
  10.126 +qed
  10.127 +
  10.128 +lemma continuous_on_closure_sequentially:
  10.129 +  fixes f :: "'a::metric_space \<Rightarrow> 'b :: metric_space"
  10.130 +  shows
  10.131 +   "continuous_on (closure S) f \<longleftrightarrow>
  10.132 +    (\<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)"
  10.133 +   (is "?lhs = ?rhs")
  10.134 +proof -
  10.135 +  have "continuous_on (closure S) f \<longleftrightarrow> 
  10.136 +           (\<forall>x \<in> closure S. continuous (at x within S) f)"
  10.137 +    by (force simp: continuous_on_closure Topology_Euclidean_Space.continuous_within_eps_delta)
  10.138 +  also have "... = ?rhs"
  10.139 +    by (force simp: continuous_within_sequentially)
  10.140 +  finally show ?thesis .
  10.141 +qed
  10.142 +
  10.143 +lemma uniformly_continuous_on_closure:
  10.144 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
  10.145 +  assumes ucont: "uniformly_continuous_on S f"
  10.146 +      and cont: "continuous_on (closure S) f"
  10.147 +    shows "uniformly_continuous_on (closure S) f"
  10.148 +unfolding uniformly_continuous_on_def
  10.149 +proof (intro allI impI)
  10.150 +  fix e::real
  10.151 +  assume "0 < e"
  10.152 +  then obtain d::real 
  10.153 +    where "d>0" 
  10.154 +      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"
  10.155 +    using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
  10.156 +  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"
  10.157 +  proof (rule exI [where x="d/3"], clarsimp simp: \<open>d > 0\<close>)
  10.158 +    fix x y
  10.159 +    assume x: "x \<in> closure S" and y: "y \<in> closure S" and dyx: "dist y x * 3 < d"
  10.160 +    obtain d1::real where "d1 > 0" 
  10.161 +           and d1: "\<And>w. \<lbrakk>w \<in> closure S; dist w x < d1\<rbrakk> \<Longrightarrow> dist (f w) (f x) < e/3"
  10.162 +      using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \<open>0 < e\<close> x by auto
  10.163 +     obtain x' where "x' \<in> S" and x': "dist x' x < min d1 (d / 3)"
  10.164 +        using closure_approachable [of x S] 
  10.165 +        by (metis \<open>0 < d1\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj x zero_less_numeral) 
  10.166 +    obtain d2::real where "d2 > 0" 
  10.167 +           and d2: "\<forall>w \<in> closure S. dist w y < d2 \<longrightarrow> dist (f w) (f y) < e/3"
  10.168 +      using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \<open>0 < e\<close> y by auto
  10.169 +     obtain y' where "y' \<in> S" and y': "dist y' y < min d2 (d / 3)"
  10.170 +        using closure_approachable [of y S] 
  10.171 +        by (metis \<open>0 < d2\<close> \<open>0 < d\<close> divide_pos_pos min_less_iff_conj y zero_less_numeral)
  10.172 +     have "dist x' x < d/3" using x' by auto
  10.173 +     moreover have "dist x y < d/3"
  10.174 +       by (metis dist_commute dyx less_divide_eq_numeral1(1)) 
  10.175 +     moreover have "dist y y' < d/3"
  10.176 +       by (metis (no_types) dist_commute min_less_iff_conj y') 
  10.177 +     ultimately have "dist x' y' < d/3 + d/3 + d/3"
  10.178 +       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
  10.179 +     then have "dist x' y' < d" by simp 
  10.180 +     then have "dist (f x') (f y') < e/3" 
  10.181 +       by (rule d [OF \<open>y' \<in> S\<close> \<open>x' \<in> S\<close>])
  10.182 +     moreover have "dist (f x') (f x) < e/3" using \<open>x' \<in> S\<close> closure_subset x' d1
  10.183 +       by (simp add: closure_def)
  10.184 +     moreover have "dist (f y') (f y) < e/3" using \<open>y' \<in> S\<close> closure_subset y' d2
  10.185 +       by (simp add: closure_def)
  10.186 +     ultimately have "dist (f y) (f x) < e/3 + e/3 + e/3"
  10.187 +       by (meson dist_commute_lessI dist_triangle_lt add_strict_mono)
  10.188 +    then show "dist (f y) (f x) < e" by simp
  10.189 +  qed
  10.190 +qed
  10.191 +
  10.192  subsection \<open>A function constant on a set\<close>
  10.193  
  10.194  definition constant_on  (infixl "(constant'_on)" 50)
  10.195 @@ -6047,7 +6171,7 @@
  10.196    {
  10.197      fix x
  10.198      have "continuous (at x) (\<lambda>x. x - a)"
  10.199 -      by (intro continuous_diff continuous_at_id continuous_const)
  10.200 +      by (intro continuous_diff continuous_ident continuous_const)
  10.201    }
  10.202    moreover have "{x. x - a \<in> s} = op + a ` s"
  10.203      by force
  10.204 @@ -6385,7 +6509,7 @@
  10.205    have "?B \<noteq> {}" using \<open>b \<in> s\<close>
  10.206      by (auto simp: dist_commute)
  10.207    moreover have "continuous_on ?B (dist a)"
  10.208 -    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const)
  10.209 +    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
  10.210    moreover have "compact ?B"
  10.211      by (intro closed_inter_compact \<open>closed s\<close> compact_cball)
  10.212    ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
  10.213 @@ -6828,7 +6952,7 @@
  10.214    then have "s \<noteq> {}" "t \<noteq> {}" by auto
  10.215    let ?inf = "\<lambda>x. infdist x t"
  10.216    have "continuous_on s ?inf"
  10.217 -    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_at_id)
  10.218 +    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
  10.219    then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"
  10.220      using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto
  10.221    then have "0 < ?inf x"
  10.222 @@ -7134,7 +7258,7 @@
  10.223  lemma open_box[intro]: "open (box a b)"
  10.224  proof -
  10.225    have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
  10.226 -    by (auto intro!: continuous_open_vimage continuous_inner continuous_at_id continuous_const)
  10.227 +    by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
  10.228    also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
  10.229      by (auto simp add: box_def inner_commute)
  10.230    finally show ?thesis .
  10.231 @@ -8344,7 +8468,7 @@
  10.232    let ?D = "(\<lambda>x. (x, x)) ` s"
  10.233    have D: "compact ?D" "?D \<noteq> {}"
  10.234      by (rule compact_continuous_image)
  10.235 -       (auto intro!: s continuous_Pair continuous_within_id simp: continuous_on_eq_continuous_within)
  10.236 +       (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
  10.237  
  10.238    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"
  10.239      using dist by fastforce
  10.240 @@ -8353,7 +8477,7 @@
  10.241    then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
  10.242      unfolding continuous_on_eq_continuous_within
  10.243      by (intro continuous_dist ballI continuous_within_compose)
  10.244 -       (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
  10.245 +       (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)
  10.246  
  10.247    obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
  10.248      using continuous_attains_inf[OF D cont] by auto
  10.249 @@ -8408,7 +8532,7 @@
  10.250  next
  10.251    assume ?rhs then show ?lhs
  10.252      apply (auto simp: ball_def dist_norm)
  10.253 -    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
  10.254 +    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans)
  10.255      done
  10.256  qed
  10.257  
  10.258 @@ -8448,7 +8572,7 @@
  10.259  next
  10.260    assume ?rhs then show ?lhs
  10.261      apply (auto simp: ball_def dist_norm )
  10.262 -    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
  10.263 +    apply (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans)
  10.264      done
  10.265  qed
  10.266  
    11.1 --- a/src/HOL/Probability/Regularity.thy	Mon Mar 07 08:14:18 2016 +0100
    11.2 +++ b/src/HOL/Probability/Regularity.thy	Mon Mar 07 14:34:45 2016 +0000
    11.3 @@ -249,7 +249,7 @@
    11.4          fix d
    11.5          have "?G d = (\<lambda>x. infdist x A) -` {..<d}" by auto
    11.6          also have "open \<dots>"
    11.7 -          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_at_id)
    11.8 +          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident)
    11.9          finally have "open (?G d)" .
   11.10        } note open_G = this
   11.11        from in_closed_iff_infdist_zero[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>]
    12.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Mar 07 08:14:18 2016 +0100
    12.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Mar 07 14:34:45 2016 +0000
    12.3 @@ -1050,15 +1050,14 @@
    12.4      using dist_triangle2 [of y x y] by simp
    12.5  qed
    12.6  
    12.7 +lemma dist_commute_lessI: "dist y x < e \<Longrightarrow> dist x y < e"
    12.8 +  by (simp add: dist_commute)
    12.9 +
   12.10  lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
   12.11 -using dist_triangle2 [of x z y] by (simp add: dist_commute)
   12.12 +  using dist_triangle2 [of x z y] by (simp add: dist_commute)
   12.13  
   12.14  lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
   12.15 -using dist_triangle2 [of x y a] by (simp add: dist_commute)
   12.16 -
   12.17 -lemma dist_triangle_alt:
   12.18 -  shows "dist y z <= dist x y + dist x z"
   12.19 -by (rule dist_triangle3)
   12.20 +  using dist_triangle2 [of x y a] by (simp add: dist_commute)
   12.21  
   12.22  lemma dist_pos_lt:
   12.23    shows "x \<noteq> y ==> 0 < dist x y"
   12.24 @@ -1337,6 +1336,11 @@
   12.25    assumes "linear D" obtains d where "D = (\<lambda>x. x *\<^sub>R d)"
   12.26    by (metis assms linear.scaleR mult.commute mult.left_neutral real_scaleR_def)
   12.27  
   12.28 +corollary real_linearD:
   12.29 +  fixes f :: "real \<Rightarrow> real"
   12.30 +  assumes "linear f" obtains c where "f = op* c"
   12.31 +by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
   12.32 +
   12.33  lemma linearI:
   12.34    assumes "\<And>x y. f (x + y) = f x + f y"
   12.35    assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
    13.1 --- a/src/HOL/Topological_Spaces.thy	Mon Mar 07 08:14:18 2016 +0100
    13.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Mar 07 14:34:45 2016 +0000
    13.3 @@ -399,7 +399,7 @@
    13.4  definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"
    13.5    where "nhds a = (INF S:{S. open S \<and> a \<in> S}. principal S)"
    13.6  
    13.7 -definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)
    13.8 +definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_)/ within (_)" [1000, 60] 60)
    13.9    where "at a within s = inf (nhds a) (principal (s - {a}))"
   13.10  
   13.11  abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where