new lemmas about vector_derivative, complex numbers, paths, etc.

--- a/src/HOL/Complex.thy	Wed Sep 02 23:31:41 2015 +0200
+++ b/src/HOL/Complex.thy	Thu Sep 03 20:27:53 2015 +0100
@@ -527,6 +527,9 @@
    (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
          simp del: of_real_power)
 
+lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)^2"
+  using complex_norm_square by auto
+
 lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
   by (auto simp add: Re_divide)
 
@@ -567,6 +570,18 @@
 lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
   by (metis Im_complex_div_gt_0 not_le)
 
+lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"
+  by (simp add: Re_divide power2_eq_square)
+
+lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
+  by (simp add: Im_divide power2_eq_square)
+
+lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
+  by (metis Re_divide_of_real of_real_Re)
+
+lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
+  by (metis Im_divide_of_real of_real_Re)
+
 lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
   by (induct s rule: infinite_finite_induct) auto
 
@@ -588,6 +603,12 @@
 lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
   unfolding summable_complex_iff by blast
 
+lemma complex_is_Nat_iff: "z \<in> \<nat> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_nat i)"
+  by (auto simp: Nats_def complex_eq_iff)
+
+lemma complex_is_Int_iff: "z \<in> \<int> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_int i)"
+  by (auto simp: Ints_def complex_eq_iff)
+
 lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   by (auto simp: Reals_def complex_eq_iff)
 

--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Sep 02 23:31:41 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 03 20:27:53 2015 +0100
@@ -1140,10 +1140,6 @@
 
 subsection "Derivative"
 
-lemma differentiable_at_imp_differentiable_on:
-  "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
-  by (metis differentiable_at_withinI differentiable_on_def)
-
 definition "jacobian f net = matrix(frechet_derivative f net)"
 
 lemma jacobian_works:

--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Sep 02 23:31:41 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Thu Sep 03 20:27:53 2015 +0100
@@ -1,7 +1,7 @@
 section \<open>Complex path integrals and Cauchy's integral theorem\<close>
 
 theory Cauchy_Integral_Thm
-imports Complex_Transcendental Path_Connected
+imports Complex_Transcendental Weierstrass
 begin
 
 
@@ -2512,13 +2512,14 @@
   apply (rule path_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g])
   using fh  by (simp add: complex_differentiable_def holomorphic_on_open os)
 
-lemma path_integrable_inversediff:
+lemma continuous_on_inversediff:
+  fixes z:: "'a::real_normed_field" shows "z \<notin> s \<Longrightarrow> continuous_on s (\<lambda>w. 1 / (w - z))"
+  by (rule continuous_intros | force)+
+
+corollary path_integrable_inversediff:
     "\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) path_integrable_on g"
-apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}"])
-    apply (rule continuous_intros | simp)+
- apply blast
-apply (simp add: holomorphic_on_open open_delete)
-apply (force intro: derivative_eq_intros)
+apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff])
+apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
 done
 
 text{*Key fact that path integral is the same for a "nearby" path. This is the
@@ -2688,7 +2689,7 @@
                  \<subseteq> ball (p t) (ee (p t))"
             apply (intro subset_path_image_join pi_hgn pi_ghn')
             using `N>0` Suc.prems
-            apply (auto simp: dist_norm field_simps ptgh_ee)
+            apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
             done
           have pi0: "(f has_path_integral 0)
                        (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
@@ -2778,4 +2779,64 @@
   using path_integral_nearby [OF assms, where Ends=False]
   by simp_all
 
+lemma valid_path_polynomial_function:
+  fixes p :: "real \<Rightarrow> 'b::euclidean_space"
+  shows "polynomial_function p \<Longrightarrow> valid_path p"
+apply (simp add: valid_path_def)
+apply (rule differentiable_on_imp_piecewise_differentiable [OF differentiable_at_imp_differentiable_on])
+using differentiable_def has_vector_derivative_def
+apply (blast intro: dest: has_vector_derivative_polynomial_function)
+done
+
+lemma path_integral_bound_exists:
+assumes s: "open s"
+    and g: "valid_path g"
+    and pag: "path_image g \<subseteq> s"
+  shows "\<exists>L. 0 < L \<and>
+	     (\<forall>f B. f holomorphic_on s \<and> (\<forall>z \<in> s. norm(f z) \<le> B)
+		     \<longrightarrow> norm(path_integral g f) \<le> L*B)"
+proof -
+have "path g" using g
+  by (simp add: valid_path_imp_path)
+then obtain d::real and p
+  where d: "0 < d"
+    and p: "polynomial_function p" "path_image p \<subseteq> s"
+    and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
+  using path_integral_nearby_ends [OF s `path g` pag]
+  apply clarify
+  apply (drule_tac x=g in spec)
+  apply (simp only: assms)
+  apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
+  done
+then obtain p' where p': "polynomial_function p'"
+	       "\<And>x. (p has_vector_derivative (p' x)) (at x)"
+  using has_vector_derivative_polynomial_function by force
+then have "bounded(p' ` {0..1})"
+  using continuous_on_polymonial_function
+  by (force simp: intro!: compact_imp_bounded compact_continuous_image)
+then obtain L where L: "L>0" and nop': "\<And>x. x \<in> {0..1} \<Longrightarrow> norm (p' x) \<le> L"
+  by (force simp: bounded_pos)
+{ fix f B
+  assume f: "f holomorphic_on s"
+     and B: "\<And>z. z\<in>s \<Longrightarrow> cmod (f z) \<le> B"
+  then have "f path_integrable_on p \<and> valid_path p"
+    using p s
+    by (blast intro: valid_path_polynomial_function path_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
+  moreover have "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (vector_derivative p (at x)) * cmod (f (p x)) \<le> L * B"
+    apply (rule mult_mono)
+    apply (subst Derivative.vector_derivative_at; force intro: p' nop')
+    using L B p
+    apply (auto simp: path_image_def image_subset_iff)
+    done
+  ultimately have "cmod (path_integral g f) \<le> L * B"
+    apply (simp add: pi [OF f])
+    apply (simp add: path_integral_integral)
+    apply (rule order_trans [OF integral_norm_bound_integral])
+    apply (auto simp: mult.commute integral_norm_bound_integral path_integrable_on [symmetric] norm_mult)
+    done
+} then
+show ?thesis
+  by (force simp: L path_integral_integral)
+qed
+
 end

--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Sep 02 23:31:41 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 03 20:27:53 2015 +0100
@@ -6375,7 +6375,7 @@
   using segment_furthest_le[OF assms, of b]
   by (auto simp add:norm_minus_commute)
 
-lemma segment_refl: "closed_segment a a = {a}"
+lemma segment_refl [simp]: "closed_segment a a = {a}"
   unfolding segment by (auto simp add: algebra_simps)
 
 lemma closed_segment_commute: "closed_segment a b = closed_segment b a"

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Sep 02 23:31:41 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 03 20:27:53 2015 +0100
@@ -138,7 +138,7 @@
 qed
 
 lemma DERIV_caratheodory_within:
-  "(f has_field_derivative l) (at x within s) \<longleftrightarrow> 
+  "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
    (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
       (is "?lhs = ?rhs")
 proof
@@ -209,6 +209,15 @@
   using has_derivative_at_within
   by blast
 
+lemma differentiable_at_imp_differentiable_on:
+  "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
+  by (metis differentiable_at_withinI differentiable_on_def)
+
+corollary differentiable_iff_scaleR:
+  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
+  shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
+  by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
+
 lemma differentiable_within_open: (* TODO: delete *)
   assumes "a \<in> s"
     and "open s"
@@ -2241,6 +2250,24 @@
   apply auto
   done
 
+lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
+  by (simp add: vector_derivative_at)
+
+lemma vector_derivative_minus_at [simp]:
+  "f differentiable at a
+   \<Longrightarrow> vector_derivative (\<lambda>x. - f x) (at a) = - vector_derivative f (at a)"
+  by (simp add: vector_derivative_at has_vector_derivative_minus vector_derivative_works [symmetric])
+
+lemma vector_derivative_add_at [simp]:
+  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+   \<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"
+  by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric])
+
+lemma vector_derivative_diff_at [simp]:
+  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
+   \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
+  by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
+
 lemma vector_derivative_within_closed_interval:
   assumes "a < b"
     and "x \<in> cbox a b"