# HG changeset patch # User paulson # Date 1450795295 0 # Node ID a759f69db1f6fd8ecb84cdea2a714136492757f6 # Parent 678c3648067cb5b708fdf90c6fed9b762873551f# Parent f0c894ab18c916830ec8d65705f810bd96dfb44c Merge diff -r 678c3648067c -r a759f69db1f6 NEWS --- a/NEWS Tue Dec 22 15:21:31 2015 +0100 +++ b/NEWS Tue Dec 22 14:41:35 2015 +0000 @@ -596,7 +596,8 @@ orders. * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals), -Cauchy's integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light +Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem, +Fundamental Theorem of Algebra. Ported from HOL Light * Multivariate_Analysis: Added topological concepts such as connected components, homotopic paths and the inside or outside of a set. diff -r 678c3648067c -r a759f69db1f6 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Dec 22 15:21:31 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Dec 22 14:41:35 2015 +0000 @@ -6025,4 +6025,354 @@ unfolding contour_integral_unique [OF *] by (simp add: divide_simps) qed +corollary Cauchy_contour_integral_circlepath: + assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \ ball z r" + shows "contour_integral(circlepath z r) (\u. f u/(u - w)^(Suc k)) = (2 * pi * ii) * (deriv ^^ k) f w / of_real(fact k)" +by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms]) + +corollary Cauchy_contour_integral_circlepath_2: + assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \ ball z r" + shows "contour_integral(circlepath z r) (\u. f u/(u - w)^2) = (2 * pi * ii) * deriv f w" + using Cauchy_contour_integral_circlepath [OF assms, of 1] + by (simp add: power2_eq_square) + + +subsection\A holomorphic function is analytic, i.e. has local power series.\ + +theorem holomorphic_power_series: + assumes holf: "f holomorphic_on ball z r" + and w: "w \ ball z r" + shows "((\n. (deriv ^^ n) f z / of_real(fact n) * (w - z)^n) sums f w)" +proof - + have fh': "f holomorphic_on cball z ((r + dist w z) / 2)" + apply (rule holomorphic_on_subset [OF holf]) + apply (clarsimp simp del: divide_const_simps) + apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w) + done + --\Replacing @{term r} and the original (weak) premises\ + obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \ ball z r" + apply (rule that [of "(r + dist w z) / 2"]) + apply (simp_all add: fh') + apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w) + apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w) + done + then have holf: "f holomorphic_on ball z r" and contf: "continuous_on (cball z r) f" + using ball_subset_cball holomorphic_on_subset apply blast + by (simp add: holfc holomorphic_on_imp_continuous_on) + have cint: "\k. (\u. f u / (u - z) ^ Suc k) contour_integrable_on circlepath z r" + apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf]) + apply (simp add: \0 < r\) + done + obtain B where "0 < B" and B: "\u. u \ cball z r \ norm(f u) \ B" + by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI) + obtain k where k: "0 < k" "k \ r" and wz_eq: "norm(w - z) = r - k" + and kle: "\u. norm(u - z) = r \ k \ norm(u - w)" + apply (rule_tac k = "r - dist z w" in that) + using w + apply (auto simp: dist_norm norm_minus_commute) + by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute) + have *: "\\<^sub>F n in sequentially. \x\path_image (circlepath z r). + norm ((\k (r - k) / r" "(r - k) / r < 1" using k by auto + obtain n where n: "((r - k) / r) ^ n < e / B * k" + using real_arch_pow_inv [of "e/B*k" "(r - k)/r"] \0 < e\ \0 < B\ k by force + have "norm ((\k N" and r: "r = dist z u" for N u + proof - + have N: "((r - k) / r) ^ N < e / B * k" + apply (rule le_less_trans [OF power_decreasing n]) + using \n \ N\ k by auto + have u [simp]: "(u \ z) \ (u \ w)" + using \0 < r\ r w by auto + have wzu_not1: "(w - z) / (u - z) \ 1" + by (metis (no_types) dist_norm divide_eq_1_iff less_irrefl mem_ball norm_minus_commute r w) + have "norm ((\kk0 < B\ + apply (auto simp: geometric_sum [OF wzu_not1]) + apply (simp add: field_simps norm_mult [symmetric]) + done + also have "... = norm ((u - z) ^ N * (w - u) - ((w - z) ^ N - (u - z) ^ N) * (u - w)) / (r ^ N * norm (u - w)) * norm (f u)" + using \0 < r\ r by (simp add: divide_simps norm_mult norm_divide norm_power dist_norm norm_minus_commute) + also have "... = norm ((w - z) ^ N * (w - u)) / (r ^ N * norm (u - w)) * norm (f u)" + by (simp add: algebra_simps) + also have "... = norm (w - z) ^ N * norm (f u) / r ^ N" + by (simp add: norm_mult norm_power norm_minus_commute) + also have "... \ (((r - k)/r)^N) * B" + using \0 < r\ w k + apply (simp add: divide_simps) + apply (rule mult_mono [OF power_mono]) + apply (auto simp: norm_divide wz_eq norm_power dist_norm norm_minus_commute B r) + done + also have "... < e * k" + using \0 < B\ N by (simp add: divide_simps) + also have "... \ e * norm (u - w)" + using r kle \0 < e\ by (simp add: dist_commute dist_norm) + finally show ?thesis + by (simp add: divide_simps norm_divide del: power_Suc) + qed + with \0 < r\ show ?thesis + by (auto simp: mult_ac less_imp_le eventually_sequentially Ball_def) + qed + have eq: "\\<^sub>F x in sequentially. + contour_integral (circlepath z r) (\u. \kku. f u / (u - z) ^ Suc k) * (w - z) ^ k)" + apply (rule eventuallyI) + apply (subst contour_integral_setsum, simp) + using contour_integrable_lmul [OF cint, of "(w - z) ^ a" for a] apply (simp add: field_simps) + apply (simp only: contour_integral_lmul cint algebra_simps) + done + have "(\k. contour_integral (circlepath z r) (\u. f u/(u - z)^(Suc k)) * (w - z)^k) + sums contour_integral (circlepath z r) (\u. f u/(u - w))" + unfolding sums_def + apply (rule Lim_transform_eventually [OF eq]) + apply (rule contour_integral_uniform_limit_circlepath [OF eventuallyI *]) + apply (rule contour_integrable_setsum, simp) + apply (rule contour_integrable_lmul) + apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf]) + using \0 < r\ + apply auto + done + then have "(\k. contour_integral (circlepath z r) (\u. f u/(u - z)^(Suc k)) * (w - z)^k) + sums (2 * of_real pi * ii * f w)" + using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]]) + then have "(\k. contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc k) * (w - z)^k / (\ * (of_real pi * 2))) + sums ((2 * of_real pi * ii * f w) / (\ * (complex_of_real pi * 2)))" + by (rule Series.sums_divide) + then have "(\n. (w - z) ^ n * contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc n) / (\ * (of_real pi * 2))) + sums f w" + by (simp add: field_simps) + then show ?thesis + by (simp add: field_simps \0 < r\ Cauchy_higher_derivative_integral_circlepath [OF contf holf]) +qed + + +subsection\The Liouville theorem and the Fundamental Theorem of Algebra.\ + +text\ These weak Liouville versions don't even need the derivative formula.\ + +lemma Liouville_weak_0: + assumes holf: "f holomorphic_on UNIV" and inf: "(f ---> 0) at_infinity" + shows "f z = 0" +proof (rule ccontr) + assume fz: "f z \ 0" + with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"] + obtain B where B: "\x. B \ cmod x \ norm (f x) * 2 < cmod (f z)" + by (auto simp: dist_norm) + def R \ "1 + abs B + norm z" + have "R > 0" unfolding R_def by (meson abs_add_one_gt_zero le_less_trans less_add_same_cancel2 norm_ge_zero) + have *: "((\u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \ * f z) (circlepath z R)" + apply (rule Cauchy_integral_circlepath) + using \R > 0\ apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+ + done + have "cmod (x - z) = R \ cmod (f x) * 2 \ cmod (f z)" for x + apply (simp add: R_def) + apply (rule less_imp_le) + apply (rule B) + using norm_triangle_ineq4 [of x z] + apply (auto simp:) + done + with \R > 0\ fz show False + using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"] + by (auto simp: norm_mult norm_divide divide_simps) +qed + +proposition Liouville_weak: + assumes "f holomorphic_on UNIV" and "(f ---> l) at_infinity" + shows "f z = l" + using Liouville_weak_0 [of "\z. f z - l"] + by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero) + + +proposition Liouville_weak_inverse: + assumes "f holomorphic_on UNIV" and unbounded: "\B. eventually (\x. norm (f x) \ B) at_infinity" + obtains z where "f z = 0" +proof - + { assume f: "\z. f z \ 0" + have 1: "(\x. 1 / f x) holomorphic_on UNIV" + by (simp add: holomorphic_on_divide holomorphic_on_const assms f) + have 2: "((\x. 1 / f x) ---> 0) at_infinity" + apply (rule tendstoI [OF eventually_mono]) + apply (rule_tac B="2/e" in unbounded) + apply (simp add: dist_norm norm_divide divide_simps mult_ac) + done + have False + using Liouville_weak_0 [OF 1 2] f by simp + } + then show ?thesis + using that by blast +qed + + +text\ In particular we get the Fundamental Theorem of Algebra.\ + +theorem fundamental_theorem_of_algebra: + fixes a :: "nat \ complex" + assumes "a 0 = 0 \ (\i \ {1..n}. a i \ 0)" + obtains z where "(\i\n. a i * z^i) = 0" +using assms +proof (elim disjE bexE) + assume "a 0 = 0" then show ?thesis + by (auto simp: that [of 0]) +next + fix i + assume i: "i \ {1..n}" and nz: "a i \ 0" + have 1: "(\z. \i\n. a i * z^i) holomorphic_on UNIV" + by (rule holomorphic_intros)+ + show ?thesis + apply (rule Liouville_weak_inverse [OF 1]) + apply (rule polyfun_extremal) + apply (rule nz) + using i that + apply (auto simp:) + done +qed + + +subsection\ Weierstrass convergence theorem.\ + +proposition holomorphic_uniform_limit: + assumes cont: "eventually (\n. continuous_on (cball z r) (f n) \ (f n) holomorphic_on ball z r) F" + and lim: "\e. 0 < e \ eventually (\n. \x \ cball z r. norm(f n x - g x) < e) F" + and F: "~ trivial_limit F" + obtains "continuous_on (cball z r) g" "g holomorphic_on ball z r" +proof (cases r "0::real" rule: linorder_cases) + case less then show ?thesis by (force simp add: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that) +next + case equal then show ?thesis + by (force simp add: holomorphic_on_def continuous_on_sing intro: that) +next + case greater + have contg: "continuous_on (cball z r) g" + using cont + by (fastforce simp: eventually_conj_iff dist_norm intro: eventually_mono [OF lim] continuous_uniform_limit [OF F]) + have 1: "continuous_on (path_image (circlepath z r)) (\x. 1 / (2 * complex_of_real pi * \) * g x)" + apply (rule continuous_intros continuous_on_subset [OF contg])+ + using \0 < r\ by auto + have 2: "((\u. 1 / (2 * of_real pi * \) * g u / (u - w) ^ 1) has_contour_integral g w) (circlepath z r)" + if w: "w \ ball z r" for w + proof - + def d \ "(r - norm(w - z))" + have "0 < d" "d \ r" using w by (auto simp: norm_minus_commute d_def dist_norm) + have dle: "\u. cmod (z - u) = r \ d \ cmod (u - w)" + unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute) + have ev_int: "\\<^sub>F n in F. (\u. f n u / (u - w)) contour_integrable_on circlepath z r" + apply (rule eventually_mono [OF cont]) + using w + apply (auto intro: Cauchy_higher_derivative_integral_circlepath [where k=0, simplified]) + done + have ev_less: "\\<^sub>F n in F. \x\path_image (circlepath z r). cmod (f n x / (x - w) - g x / (x - w)) < e" + if "e > 0" for e + using greater \0 < d\ \0 < e\ + apply (simp add: norm_divide diff_divide_distrib [symmetric] divide_simps) + apply (rule_tac e1="e * d" in eventually_mono [OF lim]) + apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+ + done + have g_cint: "(\u. g u/(u - w)) contour_integrable_on circlepath z r" + by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \0 < r\]) + have cif_tends_cig: "((\n. contour_integral(circlepath z r) (\u. f n u / (u - w))) ---> contour_integral(circlepath z r) (\u. g u/(u - w))) F" + by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \0 < r\]) + have f_tends_cig: "((\n. 2 * of_real pi * ii * f n w) ---> contour_integral (circlepath z r) (\u. g u / (u - w))) F" + apply (rule Lim_transform_eventually [where f = "\n. contour_integral (circlepath z r) (\u. f n u/(u - w))"]) + apply (rule eventually_mono [OF cont]) + apply (rule contour_integral_unique [OF Cauchy_integral_circlepath]) + using w + apply (auto simp: norm_minus_commute dist_norm cif_tends_cig) + done + have "((\n. 2 * of_real pi * \ * f n w) ---> 2 * of_real pi * \ * g w) F" + apply (rule tendsto_mult_left [OF tendstoI]) + apply (rule eventually_mono [OF lim], assumption) + using w + apply (force simp add: dist_norm) + done + then have "((\u. g u / (u - w)) has_contour_integral 2 * of_real pi * \ * g w) (circlepath z r)" + using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w + by (force simp add: dist_norm) + then have "((\u. g u / (2 * of_real pi * \ * (u - w))) has_contour_integral g w) (circlepath z r)" + using has_contour_integral_div [where c = "2 * of_real pi * \"] + by (force simp add: field_simps) + then show ?thesis + by (simp add: dist_norm) + qed + show ?thesis + using Cauchy_next_derivative_circlepath(2) [OF 1 2, simplified] + by (fastforce simp add: holomorphic_on_open contg intro: that) +qed + + +text\ Version showing that the limit is the limit of the derivatives.\ + +proposition has_complex_derivative_uniform_limit: + fixes z::complex + assumes cont: "eventually (\n. continuous_on (cball z r) (f n) \ + (\w \ ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F" + and lim: "\e. 0 < e \ eventually (\n. \x \ cball z r. norm(f n x - g x) < e) F" + and F: "~ trivial_limit F" and "0 < r" + obtains g' where + "continuous_on (cball z r) g" + "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) ---> g' w) F" +proof - + let ?conint = "contour_integral (circlepath z r)" + have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r" + by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F]; + auto simp: holomorphic_on_open complex_differentiable_def)+ + then obtain g' where g': "\x. x \ ball z r \ (g has_field_derivative g' x) (at x)" + using DERIV_deriv_iff_has_field_derivative + by (fastforce simp add: holomorphic_on_open) + then have derg: "\x. x \ ball z r \ deriv g x = g' x" + by (simp add: DERIV_imp_deriv) + have tends_f'n_g': "((\n. f' n w) ---> g' w) F" if w: "w \ ball z r" for w + proof - + have eq_f': "?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \)" + if cont_fn: "continuous_on (cball z r) (f n)" + and fnd: "\w. w \ ball z r \ (f n has_field_derivative f' n w) (at w)" for n + proof - + have hol_fn: "f n holomorphic_on ball z r" + using fnd by (force simp add: holomorphic_on_open) + have "(f n has_field_derivative 1 / (2 * of_real pi * \) * ?conint (\u. f n u / (u - w)\<^sup>2)) (at w)" + by (rule Cauchy_derivative_integral_circlepath [OF cont_fn hol_fn w]) + then have f': "f' n w = 1 / (2 * of_real pi * \) * ?conint (\u. f n u / (u - w)\<^sup>2)" + using DERIV_unique [OF fnd] w by blast + show ?thesis + by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps) + qed + def d \ "(r - norm(w - z))^2" + have "d > 0" + using w by (simp add: dist_commute dist_norm d_def) + have dle: "\y. r = cmod (z - y) \ d \ cmod ((y - w)\<^sup>2)" + apply (simp add: d_def norm_power) + apply (rule power_mono) + apply (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute) + apply (metis diff_ge_0_iff_ge dist_commute dist_norm less_eq_real_def mem_ball w) + done + have 1: "\\<^sub>F n in F. (\x. f n x / (x - w)\<^sup>2) contour_integrable_on circlepath z r" + by (force simp add: holomorphic_on_open intro: w Cauchy_derivative_integral_circlepath eventually_mono [OF cont]) + have 2: "0 < e \ \\<^sub>F n in F. \x \ path_image (circlepath z r). cmod (f n x / (x - w)\<^sup>2 - g x / (x - w)\<^sup>2) < e" for e + using \r > 0\ + apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def) + apply (rule eventually_mono [OF lim, of "e*d"]) + apply (simp add: \0 < d\) + apply (force simp add: dist_norm dle intro: less_le_trans) + done + have "((\n. contour_integral (circlepath z r) (\x. f n x / (x - w)\<^sup>2)) + ---> contour_integral (circlepath z r) ((\x. g x / (x - w)\<^sup>2))) F" + by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \0 < r\]) + then have tendsto_0: "((\n. 1 / (2 * of_real pi * \) * (?conint (\x. f n x / (x - w)\<^sup>2) - ?conint (\x. g x / (x - w)\<^sup>2))) ---> 0) F" + using Lim_null by (force intro!: tendsto_mult_right_zero) + have "((\n. f' n w - g' w) ---> 0) F" + apply (rule Lim_transform_eventually [OF _ tendsto_0]) + apply (force simp add: divide_simps intro: eq_f' eventually_mono [OF cont]) + done + then show ?thesis using Lim_null by blast + qed + obtain g' where "\w. w \ ball z r \ (g has_field_derivative (g' w)) (at w) \ ((\n. f' n w) ---> g' w) F" + by (blast intro: tends_f'n_g' g' ) + then show ?thesis using g + using that by blast +qed + end diff -r 678c3648067c -r a759f69db1f6 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 22 15:21:31 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 22 14:41:35 2015 +0000 @@ -2356,6 +2356,10 @@ lemma DERIV_imp_deriv: "DERIV f x :> f' \ deriv f x = f'" unfolding deriv_def by (metis some_equality DERIV_unique) +lemma DERIV_deriv_iff_has_field_derivative: + "DERIV f x :> deriv f x \ (\f'. (f has_field_derivative f') (at x))" + by (auto simp: has_field_derivative_def DERIV_imp_deriv) + lemma DERIV_deriv_iff_real_differentiable: fixes x :: real shows "DERIV f x :> deriv f x \ f differentiable at x" diff -r 678c3648067c -r a759f69db1f6 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Dec 22 15:21:31 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Dec 22 14:41:35 2015 +0000 @@ -855,6 +855,9 @@ lemma ball_subset_cball [simp,intro]: "ball x e \ cball x e" by (simp add: subset_eq) +lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" + by force + lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e" by (simp add: subset_eq) diff -r 678c3648067c -r a759f69db1f6 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Dec 22 15:21:31 2015 +0100 +++ b/src/HOL/Topological_Spaces.thy Tue Dec 22 14:41:35 2015 +0000 @@ -1449,6 +1449,12 @@ shows "closed (f -` s)" using closed_vimage_Int [OF assms] by simp +lemma continuous_on_empty: "continuous_on {} f" + by (simp add: continuous_on_def) + +lemma continuous_on_sing: "continuous_on {x} f" + by (simp add: continuous_on_def at_within_def) + lemma continuous_on_open_Union: "(\s. s \ S \ open s) \ (\s. s \ S \ continuous_on s f) \ continuous_on (\S) f" unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)