author paulson Thu Sep 03 20:27:53 2015 +0100 (2015-09-03) changeset 61104 3c2d4636cebc parent 61098 e1b4b24f2ebd child 61105 44baf4d5e375
new lemmas about vector_derivative, complex numbers, paths, etc.
```     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.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.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 +