new lemmas about vector_derivative, complex numbers, paths, etc.
authorpaulson
Thu Sep 03 20:27:53 2015 +0100 (2015-09-03)
changeset 611043c2d4636cebc
parent 61098 e1b4b24f2ebd
child 61105 44baf4d5e375
new lemmas about vector_derivative, complex numbers, paths, etc.
src/HOL/Complex.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 02 23:31:41 2015 +0200
     1.2 +++ b/src/HOL/Complex.thy	Thu Sep 03 20:27:53 2015 +0100
     1.3 @@ -527,6 +527,9 @@
     1.4     (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
     1.5           simp del: of_real_power)
     1.6  
     1.7 +lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)^2"
     1.8 +  using complex_norm_square by auto
     1.9 +
    1.10  lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
    1.11    by (auto simp add: Re_divide)
    1.12  
    1.13 @@ -567,6 +570,18 @@
    1.14  lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
    1.15    by (metis Im_complex_div_gt_0 not_le)
    1.16  
    1.17 +lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"
    1.18 +  by (simp add: Re_divide power2_eq_square)
    1.19 +
    1.20 +lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
    1.21 +  by (simp add: Im_divide power2_eq_square)
    1.22 +
    1.23 +lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
    1.24 +  by (metis Re_divide_of_real of_real_Re)
    1.25 +
    1.26 +lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
    1.27 +  by (metis Im_divide_of_real of_real_Re)
    1.28 +
    1.29  lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
    1.30    by (induct s rule: infinite_finite_induct) auto
    1.31  
    1.32 @@ -588,6 +603,12 @@
    1.33  lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
    1.34    unfolding summable_complex_iff by blast
    1.35  
    1.36 +lemma complex_is_Nat_iff: "z \<in> \<nat> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_nat i)"
    1.37 +  by (auto simp: Nats_def complex_eq_iff)
    1.38 +
    1.39 +lemma complex_is_Int_iff: "z \<in> \<int> \<longleftrightarrow> Im z = 0 \<and> (\<exists>i. Re z = of_int i)"
    1.40 +  by (auto simp: Ints_def complex_eq_iff)
    1.41 +
    1.42  lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
    1.43    by (auto simp: Reals_def complex_eq_iff)
    1.44  
     2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Wed Sep 02 23:31:41 2015 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 03 20:27:53 2015 +0100
     2.3 @@ -1140,10 +1140,6 @@
     2.4  
     2.5  subsection "Derivative"
     2.6  
     2.7 -lemma differentiable_at_imp_differentiable_on:
     2.8 -  "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
     2.9 -  by (metis differentiable_at_withinI differentiable_on_def)
    2.10 -
    2.11  definition "jacobian f net = matrix(frechet_derivative f net)"
    2.12  
    2.13  lemma jacobian_works:
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Sep 02 23:31:41 2015 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Thu Sep 03 20:27:53 2015 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  section \<open>Complex path integrals and Cauchy's integral theorem\<close>
     3.5  
     3.6  theory Cauchy_Integral_Thm
     3.7 -imports Complex_Transcendental Path_Connected
     3.8 +imports Complex_Transcendental Weierstrass
     3.9  begin
    3.10  
    3.11  
    3.12 @@ -2512,13 +2512,14 @@
    3.13    apply (rule path_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g])
    3.14    using fh  by (simp add: complex_differentiable_def holomorphic_on_open os)
    3.15  
    3.16 -lemma path_integrable_inversediff:
    3.17 +lemma continuous_on_inversediff:
    3.18 +  fixes z:: "'a::real_normed_field" shows "z \<notin> s \<Longrightarrow> continuous_on s (\<lambda>w. 1 / (w - z))"
    3.19 +  by (rule continuous_intros | force)+
    3.20 +
    3.21 +corollary path_integrable_inversediff:
    3.22      "\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) path_integrable_on g"
    3.23 -apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}"])
    3.24 -    apply (rule continuous_intros | simp)+
    3.25 - apply blast
    3.26 -apply (simp add: holomorphic_on_open open_delete)
    3.27 -apply (force intro: derivative_eq_intros)
    3.28 +apply (rule path_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff])
    3.29 +apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
    3.30  done
    3.31  
    3.32  text{*Key fact that path integral is the same for a "nearby" path. This is the
    3.33 @@ -2688,7 +2689,7 @@
    3.34                   \<subseteq> ball (p t) (ee (p t))"
    3.35              apply (intro subset_path_image_join pi_hgn pi_ghn')
    3.36              using `N>0` Suc.prems
    3.37 -            apply (auto simp: dist_norm field_simps ptgh_ee)
    3.38 +            apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
    3.39              done
    3.40            have pi0: "(f has_path_integral 0)
    3.41                         (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
    3.42 @@ -2778,4 +2779,64 @@
    3.43    using path_integral_nearby [OF assms, where Ends=False]
    3.44    by simp_all
    3.45  
    3.46 +lemma valid_path_polynomial_function:
    3.47 +  fixes p :: "real \<Rightarrow> 'b::euclidean_space"
    3.48 +  shows "polynomial_function p \<Longrightarrow> valid_path p"
    3.49 +apply (simp add: valid_path_def)
    3.50 +apply (rule differentiable_on_imp_piecewise_differentiable [OF differentiable_at_imp_differentiable_on])
    3.51 +using differentiable_def has_vector_derivative_def
    3.52 +apply (blast intro: dest: has_vector_derivative_polynomial_function)
    3.53 +done
    3.54 +
    3.55 +lemma path_integral_bound_exists:
    3.56 +assumes s: "open s"
    3.57 +    and g: "valid_path g"
    3.58 +    and pag: "path_image g \<subseteq> s"
    3.59 +  shows "\<exists>L. 0 < L \<and>
    3.60 +	     (\<forall>f B. f holomorphic_on s \<and> (\<forall>z \<in> s. norm(f z) \<le> B)
    3.61 +		     \<longrightarrow> norm(path_integral g f) \<le> L*B)"
    3.62 +proof -
    3.63 +have "path g" using g
    3.64 +  by (simp add: valid_path_imp_path)
    3.65 +then obtain d::real and p
    3.66 +  where d: "0 < d"
    3.67 +    and p: "polynomial_function p" "path_image p \<subseteq> s"
    3.68 +    and pi: "\<And>f. f holomorphic_on s \<Longrightarrow> path_integral g f = path_integral p f"
    3.69 +  using path_integral_nearby_ends [OF s `path g` pag]
    3.70 +  apply clarify
    3.71 +  apply (drule_tac x=g in spec)
    3.72 +  apply (simp only: assms)
    3.73 +  apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
    3.74 +  done
    3.75 +then obtain p' where p': "polynomial_function p'"
    3.76 +	       "\<And>x. (p has_vector_derivative (p' x)) (at x)"
    3.77 +  using has_vector_derivative_polynomial_function by force
    3.78 +then have "bounded(p' ` {0..1})"
    3.79 +  using continuous_on_polymonial_function
    3.80 +  by (force simp: intro!: compact_imp_bounded compact_continuous_image)
    3.81 +then obtain L where L: "L>0" and nop': "\<And>x. x \<in> {0..1} \<Longrightarrow> norm (p' x) \<le> L"
    3.82 +  by (force simp: bounded_pos)
    3.83 +{ fix f B
    3.84 +  assume f: "f holomorphic_on s"
    3.85 +     and B: "\<And>z. z\<in>s \<Longrightarrow> cmod (f z) \<le> B"
    3.86 +  then have "f path_integrable_on p \<and> valid_path p"
    3.87 +    using p s
    3.88 +    by (blast intro: valid_path_polynomial_function path_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
    3.89 +  moreover have "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (vector_derivative p (at x)) * cmod (f (p x)) \<le> L * B"
    3.90 +    apply (rule mult_mono)
    3.91 +    apply (subst Derivative.vector_derivative_at; force intro: p' nop')
    3.92 +    using L B p
    3.93 +    apply (auto simp: path_image_def image_subset_iff)
    3.94 +    done
    3.95 +  ultimately have "cmod (path_integral g f) \<le> L * B"
    3.96 +    apply (simp add: pi [OF f])
    3.97 +    apply (simp add: path_integral_integral)
    3.98 +    apply (rule order_trans [OF integral_norm_bound_integral])
    3.99 +    apply (auto simp: mult.commute integral_norm_bound_integral path_integrable_on [symmetric] norm_mult)
   3.100 +    done
   3.101 +} then
   3.102 +show ?thesis
   3.103 +  by (force simp: L path_integral_integral)
   3.104 +qed
   3.105 +
   3.106  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Sep 02 23:31:41 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Sep 03 20:27:53 2015 +0100
     4.3 @@ -6375,7 +6375,7 @@
     4.4    using segment_furthest_le[OF assms, of b]
     4.5    by (auto simp add:norm_minus_commute)
     4.6  
     4.7 -lemma segment_refl: "closed_segment a a = {a}"
     4.8 +lemma segment_refl [simp]: "closed_segment a a = {a}"
     4.9    unfolding segment by (auto simp add: algebra_simps)
    4.10  
    4.11  lemma closed_segment_commute: "closed_segment a b = closed_segment b a"
     5.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Sep 02 23:31:41 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Sep 03 20:27:53 2015 +0100
     5.3 @@ -138,7 +138,7 @@
     5.4  qed
     5.5  
     5.6  lemma DERIV_caratheodory_within:
     5.7 -  "(f has_field_derivative l) (at x within s) \<longleftrightarrow> 
     5.8 +  "(f has_field_derivative l) (at x within s) \<longleftrightarrow>
     5.9     (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> continuous (at x within s) g \<and> g x = l)"
    5.10        (is "?lhs = ?rhs")
    5.11  proof
    5.12 @@ -209,6 +209,15 @@
    5.13    using has_derivative_at_within
    5.14    by blast
    5.15  
    5.16 +lemma differentiable_at_imp_differentiable_on:
    5.17 +  "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
    5.18 +  by (metis differentiable_at_withinI differentiable_on_def)
    5.19 +
    5.20 +corollary differentiable_iff_scaleR:
    5.21 +  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
    5.22 +  shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
    5.23 +  by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
    5.24 +
    5.25  lemma differentiable_within_open: (* TODO: delete *)
    5.26    assumes "a \<in> s"
    5.27      and "open s"
    5.28 @@ -2241,6 +2250,24 @@
    5.29    apply auto
    5.30    done
    5.31  
    5.32 +lemma has_vector_derivative_id_at [simp]: "vector_derivative (\<lambda>x. x) (at a) = 1"
    5.33 +  by (simp add: vector_derivative_at)
    5.34 +
    5.35 +lemma vector_derivative_minus_at [simp]:
    5.36 +  "f differentiable at a
    5.37 +   \<Longrightarrow> vector_derivative (\<lambda>x. - f x) (at a) = - vector_derivative f (at a)"
    5.38 +  by (simp add: vector_derivative_at has_vector_derivative_minus vector_derivative_works [symmetric])
    5.39 +
    5.40 +lemma vector_derivative_add_at [simp]:
    5.41 +  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    5.42 +   \<Longrightarrow> vector_derivative (\<lambda>x. f x + g x) (at a) = vector_derivative f (at a) + vector_derivative g (at a)"
    5.43 +  by (simp add: vector_derivative_at has_vector_derivative_add vector_derivative_works [symmetric])
    5.44 +
    5.45 +lemma vector_derivative_diff_at [simp]:
    5.46 +  "\<lbrakk>f differentiable at a; g differentiable at a\<rbrakk>
    5.47 +   \<Longrightarrow> vector_derivative (\<lambda>x. f x - g x) (at a) = vector_derivative f (at a) - vector_derivative g (at a)"
    5.48 +  by (simp add: vector_derivative_at has_vector_derivative_diff vector_derivative_works [symmetric])
    5.49 +
    5.50  lemma vector_derivative_within_closed_interval:
    5.51    assumes "a < b"
    5.52      and "x \<in> cbox a b"