# HG changeset patch # User paulson # Date 1441308473 -3600 # Node ID 3c2d4636cebcf91b3c27d7b2c74384af2fbdcbf3 # Parent e1b4b24f2ebd924870e1f9dc4aab8a2f94e83a24 new lemmas about vector_derivative, complex numbers, paths, etc. diff -r e1b4b24f2ebd -r 3c2d4636cebc src/HOL/Complex.thy --- 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 \ Re (a * cnj b) = 0" by (auto simp add: Re_divide) @@ -567,6 +570,18 @@ lemma Im_complex_div_le_0: "Im(a / b) \ 0 \ Im(a * cnj b) \ 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 \ Reals \ Re (z / r) = Re z / Re r" + by (metis Re_divide_of_real of_real_Re) + +lemma Im_divide_Reals: "r \ Reals \ Im (z / r) = Im z / Re r" + by (metis Im_divide_of_real of_real_Re) + lemma Re_setsum[simp]: "Re (setsum f s) = (\x\s. Re (f x))" by (induct s rule: infinite_finite_induct) auto @@ -588,6 +603,12 @@ lemma summable_Im: "summable f \ summable (\x. Im (f x))" unfolding summable_complex_iff by blast +lemma complex_is_Nat_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_nat i)" + by (auto simp: Nats_def complex_eq_iff) + +lemma complex_is_Int_iff: "z \ \ \ Im z = 0 \ (\i. Re z = of_int i)" + by (auto simp: Ints_def complex_eq_iff) + lemma complex_is_Real_iff: "z \ \ \ Im z = 0" by (auto simp: Reals_def complex_eq_iff) diff -r e1b4b24f2ebd -r 3c2d4636cebc src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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: - "(\x\(s::(real^'n) set). f differentiable at x) \ f differentiable_on s" - by (metis differentiable_at_withinI differentiable_on_def) - definition "jacobian f net = matrix(frechet_derivative f net)" lemma jacobian_works: diff -r e1b4b24f2ebd -r 3c2d4636cebc src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- 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 \Complex path integrals and Cauchy's integral theorem\ 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 \ s \ continuous_on s (\w. 1 / (w - z))" + by (rule continuous_intros | force)+ + +corollary path_integrable_inversediff: "\valid_path g; z \ path_image g\ \ (\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 @@ \ 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 \ 'b::euclidean_space" + shows "polynomial_function p \ 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 \ s" + shows "\L. 0 < L \ + (\f B. f holomorphic_on s \ (\z \ s. norm(f z) \ B) + \ norm(path_integral g f) \ 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 \ s" + and pi: "\f. f holomorphic_on s \ 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'" + "\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': "\x. x \ {0..1} \ norm (p' x) \ L" + by (force simp: bounded_pos) +{ fix f B + assume f: "f holomorphic_on s" + and B: "\z. z\s \ cmod (f z) \ B" + then have "f path_integrable_on p \ valid_path p" + using p s + by (blast intro: valid_path_polynomial_function path_integrable_holomorphic_simple holomorphic_on_imp_continuous_on) + moreover have "\x. x \ {0..1} \ cmod (vector_derivative p (at x)) * cmod (f (p x)) \ 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) \ 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 diff -r e1b4b24f2ebd -r 3c2d4636cebc src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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" diff -r e1b4b24f2ebd -r 3c2d4636cebc src/HOL/Multivariate_Analysis/Derivative.thy --- 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) \ + "(f has_field_derivative l) (at x within s) \ (\g. (\z. f z - f x = g z * (z - x)) \ continuous (at x within s) g \ g x = l)" (is "?lhs = ?rhs") proof @@ -209,6 +209,15 @@ using has_derivative_at_within by blast +lemma differentiable_at_imp_differentiable_on: + "(\x. x \ s \ f differentiable at x) \ f differentiable_on s" + by (metis differentiable_at_withinI differentiable_on_def) + +corollary differentiable_iff_scaleR: + fixes f :: "real \ 'a::real_normed_vector" + shows "f differentiable F \ (\d. (f has_derivative (\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 \ s" and "open s" @@ -2241,6 +2250,24 @@ apply auto done +lemma has_vector_derivative_id_at [simp]: "vector_derivative (\x. x) (at a) = 1" + by (simp add: vector_derivative_at) + +lemma vector_derivative_minus_at [simp]: + "f differentiable at a + \ vector_derivative (\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]: + "\f differentiable at a; g differentiable at a\ + \ vector_derivative (\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]: + "\f differentiable at a; g differentiable at a\ + \ vector_derivative (\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 \ cbox a b"