# HG changeset patch # User paulson # Date 1487689441 0 # Node ID ab7e11730ad8515e4e320d857c2ba4a52d51bcf3 # Parent b46fe5138cb008e16ffd03e1d59d34dc45968365 Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Tue Feb 21 15:04:01 2017 +0000 @@ -190,9 +190,9 @@ have "g \ bcontfun" \ \The limit function is bounded and continuous\ proof (intro bcontfunI) show "continuous_on UNIV g" - using bcontfunE[OF Rep_bcontfun] limit_function - by (intro continuous_uniform_limit[where f="\n. Rep_bcontfun (f n)" and F="sequentially"]) - (auto simp add: eventually_sequentially trivial_limit_def dist_norm) + apply (rule bcontfunE[OF Rep_bcontfun]) + using limit_function + by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\n. Rep_bcontfun (f n)" and F="sequentially"]) next fix x from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1" diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Feb 21 15:04:01 2017 +0000 @@ -82,7 +82,7 @@ apply (blast intro: continuous_on_compose2) apply (rename_tac A B) apply (rule_tac x="A \ (\x\B. s \ f-`{x})" in exI) - apply (blast intro: differentiable_chain_within) + apply (blast intro!: differentiable_chain_within) done lemma piecewise_differentiable_affine: @@ -5172,7 +5172,7 @@ proposition contour_integral_uniform_limit: assumes ev_fint: "eventually (\n::'a. (f n) contour_integrable_on \) F" - and ev_no: "\e. 0 < e \ eventually (\n. \x \ path_image \. norm(f n x - l x) < e) F" + and ul_f: "uniform_limit (path_image \) f l F" and noleB: "\t. t \ {0..1} \ norm (vector_derivative \ (at t)) \ B" and \: "valid_path \" and [simp]: "~ (trivial_limit F)" @@ -5181,10 +5181,13 @@ have "0 \ B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one) { fix e::real assume "0 < e" - then have eB: "0 < e / (\B\ + 1)" by simp + then have "0 < e / (\B\ + 1)" by simp + then have "\\<^sub>F n in F. \x\path_image \. cmod (f n x - l x) < e / (\B\ + 1)" + using ul_f [unfolded uniform_limit_iff dist_norm] by auto + with ev_fint obtain a where fga: "\x. x \ {0..1} \ cmod (f a (\ x) - l (\ x)) < e / (\B\ + 1)" and inta: "(\t. f a (\ t) * vector_derivative \ (at t)) integrable_on {0..1}" - using eventually_happens [OF eventually_conj [OF ev_no [OF eB] ev_fint]] + using eventually_happens [OF eventually_conj] by (fastforce simp: contour_integrable_on path_image_def) have Ble: "B * e / (\B\ + 1) \ e" using \0 \ B\ \0 < e\ by (simp add: divide_simps) @@ -5209,7 +5212,8 @@ have B': "B' > 0" "B' > B" using \0 \ B\ by (auto simp: B'_def) assume "0 < e" then have ev_no': "\\<^sub>F n in F. \x\path_image \. 2 * cmod (f n x - l x) < e / B'" - using ev_no [of "e / B' / 2"] B' by (simp add: field_simps) + using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B' / 2"] B' + by (simp add: field_simps) have ie: "integral {0..1::real} (\x. e / 2) < e" using \0 < e\ by simp have *: "cmod (f x (\ t) * vector_derivative \ (at t) - l (\ t) * vector_derivative \ (at t)) \ e / 2" if t: "t\{0..1}" and leB': "2 * cmod (f x (\ t) - l (\ t)) < e / B'" for x t @@ -5235,12 +5239,13 @@ by (rule tendstoI) qed -proposition contour_integral_uniform_limit_circlepath: - assumes ev_fint: "eventually (\n::'a. (f n) contour_integrable_on (circlepath z r)) F" - and ev_no: "\e. 0 < e \ eventually (\n. \x \ path_image (circlepath z r). norm(f n x - l x) < e) F" - and [simp]: "~ (trivial_limit F)" "0 < r" - shows "l contour_integrable_on (circlepath z r)" "((\n. contour_integral (circlepath z r) (f n)) \ contour_integral (circlepath z r) l) F" -by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms) +corollary contour_integral_uniform_limit_circlepath: + assumes "\\<^sub>F n::'a in F. (f n) contour_integrable_on (circlepath z r)" + and "uniform_limit (sphere z r) f l F" + and "~ (trivial_limit F)" "0 < r" + shows "l contour_integrable_on (circlepath z r)" + "((\n. contour_integral (circlepath z r) (f n)) \ contour_integral (circlepath z r) l) F" + using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit) subsection\ General stepping result for derivative formulas.\ @@ -5371,11 +5376,11 @@ apply (force simp: \d > 0\ dist_norm that simp del: power_Suc intro: *) done qed - have 2: "\\<^sub>F n in at w. - \x\path_image \. - cmod (f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k - f' x / (x - w) ^ Suc k) < e" - if "0 < e" for e - proof - + have 2: "uniform_limit (path_image \) (\n x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k) (\x. f' x / (x - w) ^ Suc k) (at w)" + unfolding uniform_limit_iff dist_norm + proof clarify + fix e::real + assume "0 < e" have *: "cmod (f' (\ x) * (inverse (\ x - u) ^ k - inverse (\ x - w) ^ k) / ((u - w) * k) - f' (\ x) / ((\ x - w) * (\ x - w) ^ k)) < e" if ec: "cmod ((inverse (\ x - u) ^ k - inverse (\ x - w) ^ k) / ((u - w) * k) - @@ -5402,8 +5407,10 @@ by (metis False \0 < e\ frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff) finally show ?thesis . qed - show ?thesis - using twom [OF divide_pos_pos [OF that \C > 0\]] unfolding path_image_def + show "\\<^sub>F n in at w. + \x\path_image \. + cmod (f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k - f' x / (x - w) ^ Suc k) < e" + using twom [OF divide_pos_pos [OF \0 < e\ \C > 0\]] unfolding path_image_def by (force intro: * elim: eventually_mono) qed show "(\u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \" @@ -6017,10 +6024,11 @@ 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 ((\kn x. (\kx. f x / (x - w)) sequentially" + unfolding uniform_limit_iff dist_norm + proof clarify + fix e::real + assume "0 < e" have rr: "0 \ (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 @@ -6061,7 +6069,8 @@ finally show ?thesis by (simp add: divide_simps norm_divide del: power_Suc) qed - with \0 < r\ show ?thesis + with \0 < r\ show "\\<^sub>F n in sequentially. \x\sphere z r. + norm ((\k\<^sub>F x in sequentially. @@ -6076,7 +6085,7 @@ 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_integral_uniform_limit_circlepath [OF eventuallyI ul]) apply (rule contour_integrable_sum, simp) apply (rule contour_integrable_lmul) apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf]) @@ -6189,7 +6198,7 @@ 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 ulim: "uniform_limit (cball z r) f g 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) @@ -6200,8 +6209,7 @@ 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]) + using cont uniform_limit_theorem [OF eventually_mono ulim F] by blast 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 @@ -6217,17 +6225,16 @@ 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)+ + have ul_less: "uniform_limit (sphere z r) (\n x. f n x / (x - w)) (\x. g x / (x - w)) F" + using greater \0 < d\ + apply (clarsimp simp add: uniform_limit_iff dist_norm norm_divide diff_divide_distrib [symmetric] divide_simps) + apply (rule_tac e1="e * d" in eventually_mono [OF uniform_limitD [OF ulim]]) + 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\]) + by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_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\]) + by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \0 < r\]) have f_tends_cig: "((\n. 2 * of_real pi * \ * 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]) @@ -6237,7 +6244,7 @@ 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) + apply (rule eventually_mono [OF uniform_limitD [OF ulim]], assumption) using w apply (force simp add: dist_norm) done @@ -6262,7 +6269,7 @@ 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 ulim: "uniform_limit (cball z r) f g F" and F: "~ trivial_limit F" and "0 < r" obtains g' where "continuous_on (cball z r) g" @@ -6270,7 +6277,7 @@ 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]; + by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] ulim F]; auto simp: holomorphic_on_open field_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 @@ -6303,13 +6310,19 @@ 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 2: "uniform_limit (sphere z r) (\n x. f n x / (x - w)\<^sup>2) (\x. g x / (x - w)\<^sup>2) F" + unfolding uniform_limit_iff + proof clarify + fix e::real + assume "0 < e" + with \r > 0\ + show "\\<^sub>F n in F. \x\sphere z r. dist (f n x / (x - w)\<^sup>2) (g x / (x - w)\<^sup>2) < e" + apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def dist_norm) + apply (rule eventually_mono [OF uniform_limitD [OF ulim], of "e*d"]) + apply (simp add: \0 < d\) + apply (force simp add: dist_norm dle intro: less_le_trans) + done + qed 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 contour_integral_uniform_limit_circlepath [OF 1 2 F \0 < r\]) @@ -6331,18 +6344,16 @@ subsection\Some more simple/convenient versions for applications.\ lemma holomorphic_uniform_sequence: - assumes s: "open s" - and hol_fn: "\n. (f n) holomorphic_on s" - and to_g: "\x. x \ s - \ \d. 0 < d \ cball x d \ s \ - (\e. 0 < e \ eventually (\n. \y \ cball x d. norm(f n y - g y) < e) sequentially)" - shows "g holomorphic_on s" + assumes S: "open S" + and hol_fn: "\n. (f n) holomorphic_on S" + and ulim_g: "\x. x \ S \ \d. 0 < d \ cball x d \ S \ uniform_limit (cball x d) f g sequentially" + shows "g holomorphic_on S" proof - - have "\f'. (g has_field_derivative f') (at z)" if "z \ s" for z + have "\f'. (g has_field_derivative f') (at z)" if "z \ S" for z proof - - obtain r where "0 < r" and r: "cball z r \ s" - and fg: "\e. 0 < e \ eventually (\n. \y \ cball z r. norm(f n y - g y) < e) sequentially" - using to_g [OF \z \ s\] by blast + obtain r where "0 < r" and r: "cball z r \ S" + and ul: "uniform_limit (cball z r) f g sequentially" + using ulim_g [OF \z \ S\] by blast have *: "\\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \ f n holomorphic_on ball z r" apply (intro eventuallyI conjI) using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r apply blast @@ -6350,37 +6361,36 @@ done show ?thesis apply (rule holomorphic_uniform_limit [OF *]) - using \0 < r\ centre_in_ball fg + using \0 < r\ centre_in_ball ul apply (auto simp: holomorphic_on_open) done qed - with s show ?thesis + with S show ?thesis by (simp add: holomorphic_on_open) qed lemma has_complex_derivative_uniform_sequence: - fixes s :: "complex set" - assumes s: "open s" - and hfd: "\n x. x \ s \ ((f n) has_field_derivative f' n x) (at x)" - and to_g: "\x. x \ s - \ \d. 0 < d \ cball x d \ s \ - (\e. 0 < e \ eventually (\n. \y \ cball x d. norm(f n y - g y) < e) sequentially)" - shows "\g'. \x \ s. (g has_field_derivative g' x) (at x) \ ((\n. f' n x) \ g' x) sequentially" + fixes S :: "complex set" + assumes S: "open S" + and hfd: "\n x. x \ S \ ((f n) has_field_derivative f' n x) (at x)" + and ulim_g: "\x. x \ S + \ \d. 0 < d \ cball x d \ S \ uniform_limit (cball x d) f g sequentially" + shows "\g'. \x \ S. (g has_field_derivative g' x) (at x) \ ((\n. f' n x) \ g' x) sequentially" proof - - have y: "\y. (g has_field_derivative y) (at z) \ (\n. f' n z) \ y" if "z \ s" for z + have y: "\y. (g has_field_derivative y) (at z) \ (\n. f' n z) \ y" if "z \ S" for z proof - - obtain r where "0 < r" and r: "cball z r \ s" - and fg: "\e. 0 < e \ eventually (\n. \y \ cball z r. norm(f n y - g y) < e) sequentially" - using to_g [OF \z \ s\] by blast + obtain r where "0 < r" and r: "cball z r \ S" + and ul: "uniform_limit (cball z r) f g sequentially" + using ulim_g [OF \z \ S\] by blast have *: "\\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \ (\w \ ball z r. ((f n) has_field_derivative (f' n w)) (at w))" apply (intro eventuallyI conjI) - apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r s) + apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r S) using ball_subset_cball hfd r apply blast done show ?thesis apply (rule has_complex_derivative_uniform_limit [OF *, of g]) - using \0 < r\ centre_in_ball fg + using \0 < r\ centre_in_ball ul apply force+ done qed @@ -6390,67 +6400,67 @@ subsection\On analytic functions defined by a series.\ - + lemma series_and_derivative_comparison: - fixes s :: "complex set" - assumes s: "open s" + fixes S :: "complex set" + assumes S: "open S" and h: "summable h" - and hfd: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" - and to_g: "\n x. \N \ n; x \ s\ \ norm(f n x) \ h n" - obtains g g' where "\x \ s. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" + and hfd: "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" + and to_g: "\\<^sub>F n in sequentially. \x\S. norm (f n x) \ h n" + obtains g g' where "\x \ S. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" proof - - obtain g where g: "\e. e>0 \ \N. \n x. N \ n \ x \ s \ dist (\nd>0. cball x d \ s \ (\e>0. \\<^sub>F n in sequentially. \y\cball x d. cmod ((\a s" for x + obtain g where g: "uniform_limit S (\n x. \id>0. cball x d \ S \ uniform_limit (cball x d) (\n x. \i S" for x proof - - obtain d where "d>0" and d: "cball x d \ s" - using open_contains_cball [of "s"] \x \ s\ s by blast + obtain d where "d>0" and d: "cball x d \ S" + using open_contains_cball [of "S"] \x \ S\ S by blast then show ?thesis apply (rule_tac x=d in exI) - apply (auto simp: dist_norm eventually_sequentially) - apply (metis g contra_subsetD dist_norm) - done + using g uniform_limit_on_subset + apply (force simp: dist_norm eventually_sequentially) + done qed - have "(\x\s. (\n. \i g x)" - using g by (force simp add: lim_sequentially) - moreover have "\g'. \x\s. (g has_field_derivative g' x) (at x) \ (\n. \i g' x" - by (rule has_complex_derivative_uniform_sequence [OF s]) (auto intro: * hfd DERIV_sum)+ + have "\x. x \ S \ (\n. \i g x" + by (metis tendsto_uniform_limitI [OF g]) + moreover have "\g'. \x\S. (g has_field_derivative g' x) (at x) \ (\n. \i g' x" + by (rule has_complex_derivative_uniform_sequence [OF S]) (auto intro: * hfd DERIV_sum)+ ultimately show ?thesis - by (force simp add: sums_def conj_commute intro: that) + by (metis sums_def that) qed text\A version where we only have local uniform/comparative convergence.\ lemma series_and_derivative_comparison_local: - fixes s :: "complex set" - assumes s: "open s" - and hfd: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" - and to_g: "\x. x \ s \ - \d h N. 0 < d \ summable h \ (\n y. N \ n \ y \ ball x d \ norm(f n y) \ h n)" - shows "\g g'. \x \ s. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" + fixes S :: "complex set" + assumes S: "open S" + and hfd: "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" + and to_g: "\x. x \ S \ \d h. 0 < d \ summable h \ (\\<^sub>F n in sequentially. \y\ball x d \ S. norm (f n y) \ h n)" + shows "\g g'. \x \ S. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" proof - have "\y. (\n. f n z) sums (\n. f n z) \ (\n. f' n z) sums y \ ((\x. \n. f n x) has_field_derivative y) (at z)" - if "z \ s" for z + if "z \ S" for z proof - - obtain d h N where "0 < d" "summable h" and le_h: "\n y. \N \ n; y \ ball z d\ \ norm(f n y) \ h n" - using to_g \z \ s\ by meson - then obtain r where "r>0" and r: "ball z r \ ball z d \ s" using \z \ s\ s + obtain d h where "0 < d" "summable h" and le_h: "\\<^sub>F n in sequentially. \y\ball z d \ S. norm (f n y) \ h n" + using to_g \z \ S\ by meson + then obtain r where "r>0" and r: "ball z r \ ball z d \ S" using \z \ S\ S by (metis Int_iff open_ball centre_in_ball open_Int open_contains_ball_eq) - have 1: "open (ball z d \ s)" - by (simp add: open_Int s) - have 2: "\n x. x \ ball z d \ s \ (f n has_field_derivative f' n x) (at x)" + have 1: "open (ball z d \ S)" + by (simp add: open_Int S) + have 2: "\n x. x \ ball z d \ S \ (f n has_field_derivative f' n x) (at x)" by (auto simp: hfd) - obtain g g' where gg': "\x \ ball z d \ s. ((\n. f n x) sums g x) \ + obtain g g' where gg': "\x \ ball z d \ S. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" by (auto intro: le_h series_and_derivative_comparison [OF 1 \summable h\ hfd]) then have "(\n. f' n z) sums g' z" by (meson \0 < r\ centre_in_ball contra_subsetD r) moreover have "(\n. f n z) sums (\n. f n z)" - by (metis summable_comparison_test' summable_sums centre_in_ball \0 < d\ \summable h\ le_h) + using summable_sums centre_in_ball \0 < d\ \summable h\ le_h + by (metis (full_types) Int_iff gg' summable_def that) moreover have "((\x. \n. f n x) has_field_derivative g' z) (at z)" apply (rule_tac f=g in DERIV_transform_at [OF _ \0 < r\]) - apply (simp add: gg' \z \ s\ \0 < d\) + apply (simp add: gg' \z \ S\ \0 < d\) apply (metis (full_types) contra_subsetD dist_commute gg' mem_ball r sums_unique) done ultimately show ?thesis by auto @@ -6463,21 +6473,16 @@ text\Sometimes convenient to compare with a complex series of positive reals. (?)\ lemma series_and_derivative_comparison_complex: - fixes s :: "complex set" - assumes s: "open s" - and hfd: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" - and to_g: "\x. x \ s \ - \d h N. 0 < d \ summable h \ range h \ nonneg_Reals \ (\n y. N \ n \ y \ ball x d \ cmod(f n y) \ cmod (h n))" - shows "\g g'. \x \ s. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" -apply (rule series_and_derivative_comparison_local [OF s hfd], assumption) -apply (frule to_g) -apply (erule ex_forward) + fixes S :: "complex set" + assumes S: "open S" + and hfd: "\n x. x \ S \ (f n has_field_derivative f' n x) (at x)" + and to_g: "\x. x \ S \ \d h. 0 < d \ summable h \ range h \ \\<^sub>\\<^sub>0 \ (\\<^sub>F n in sequentially. \y\ball x d \ S. cmod(f n y) \ cmod (h n))" + shows "\g g'. \x \ S. ((\n. f n x) sums g x) \ ((\n. f' n x) sums g' x) \ (g has_field_derivative g' x) (at x)" +apply (rule series_and_derivative_comparison_local [OF S hfd], assumption) +apply (rule ex_forward [OF to_g], assumption) apply (erule exE) apply (rule_tac x="Re o h" in exI) -apply (erule ex_forward) -apply (simp add: summable_Re o_def ) -apply (elim conjE all_forward) -apply (simp add: nonneg_Reals_cmod_eq_Re image_subset_iff) +apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff) done @@ -6512,12 +6517,12 @@ apply (simp add: dist_norm) apply (rule_tac x="\n. of_real(norm(a n)*((r + norm z)/2)^n)" in exI) using \r > 0\ - apply (auto simp: sum nonneg_Reals_divide_I) + apply (auto simp: sum eventually_sequentially norm_mult norm_divide norm_power) apply (rule_tac x=0 in exI) - apply (force simp: norm_mult norm_divide norm_power intro!: mult_left_mono power_mono y_le) + apply (force simp: dist_norm intro!: mult_left_mono power_mono y_le) done then show ?thesis - by (simp add: dist_0_norm ball_def) + by (simp add: ball_def) next case False then show ?thesis apply (simp add: not_less) @@ -6833,7 +6838,6 @@ qed - subsection\General, homology form of Cauchy's theorem.\ text\Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\ @@ -7196,28 +7200,34 @@ then have A1: "\\<^sub>F n in sequentially. d (a n) contour_integrable_on \" by (meson U contour_integrable_on_def eventuallyI) obtain dd where "dd>0" and dd: "cball x dd \ u" using open_contains_cball u x by force - have A2: "\\<^sub>F n in sequentially. \xa\path_image \. cmod (d (a n) xa - d x xa) < ee" if "0 < ee" for ee - proof - - let ?ddpa = "{(w,z) |w z. w \ cball x dd \ z \ path_image \}" - have "uniformly_continuous_on ?ddpa (\(x,y). d x y)" - apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]]) - using dd pasz \valid_path \\ - apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball) - done - then obtain kk where "kk>0" + have A2: "uniform_limit (path_image \) (\n. d (a n)) (d x) sequentially" + unfolding uniform_limit_iff dist_norm + proof clarify + fix ee::real + assume "0 < ee" + show "\\<^sub>F n in sequentially. \\\path_image \. cmod (d (a n) \ - d x \) < ee" + proof - + let ?ddpa = "{(w,z) |w z. w \ cball x dd \ z \ path_image \}" + have "uniformly_continuous_on ?ddpa (\(x,y). d x y)" + apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]]) + using dd pasz \valid_path \\ + apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball) + done + then obtain kk where "kk>0" and kk: "\x x'. \x\?ddpa; x'\?ddpa; dist x' x < kk\ \ dist ((\(x,y). d x y) x') ((\(x,y). d x y) x) < ee" - apply (rule uniformly_continuous_onE [where e = ee]) - using \0 < ee\ by auto - have kk: "\norm (w - x) \ dd; z \ path_image \; norm ((w, z) - (x, z)) < kk\ \ norm (d w z - d x z) < ee" - for w z - using \dd>0\ kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm) - show ?thesis - using ax unfolding lim_sequentially eventually_sequentially - apply (drule_tac x="min dd kk" in spec) - using \dd > 0\ \kk > 0\ - apply (fastforce simp: kk dist_norm) - done + apply (rule uniformly_continuous_onE [where e = ee]) + using \0 < ee\ by auto + have kk: "\norm (w - x) \ dd; z \ path_image \; norm ((w, z) - (x, z)) < kk\ \ norm (d w z - d x z) < ee" + for w z + using \dd>0\ kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm) + show ?thesis + using ax unfolding lim_sequentially eventually_sequentially + apply (drule_tac x="min dd kk" in spec) + using \dd > 0\ \kk > 0\ + apply (fastforce simp: kk dist_norm) + done + qed qed have tendsto_hx: "(\n. contour_integral \ (d (a n))) \ h x" apply (simp add: contour_integral_unique [OF U, symmetric] x) @@ -7285,87 +7295,87 @@ theorem Cauchy_integral_formula_global: - assumes s: "open s" and holf: "f holomorphic_on s" - and z: "z \ s" and vpg: "valid_path \" - and pasz: "path_image \ \ s - {z}" and loop: "pathfinish \ = pathstart \" - and zero: "\w. w \ s \ winding_number \ w = 0" + assumes S: "open S" and holf: "f holomorphic_on S" + and z: "z \ S" and vpg: "valid_path \" + and pasz: "path_image \ \ S - {z}" and loop: "pathfinish \ = pathstart \" + and zero: "\w. w \ S \ winding_number \ w = 0" shows "((\w. f w / (w - z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \" proof - have "path \" using vpg by (blast intro: valid_path_imp_path) - have hols: "(\w. f w / (w - z)) holomorphic_on s - {z}" "(\w. 1 / (w - z)) holomorphic_on s - {z}" + have hols: "(\w. f w / (w - z)) holomorphic_on S - {z}" "(\w. 1 / (w - z)) holomorphic_on S - {z}" by (rule holomorphic_intros holomorphic_on_subset [OF holf] | force)+ then have cint_fw: "(\w. f w / (w - z)) contour_integrable_on \" - by (meson contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on open_delete s vpg pasz) + by (meson contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on open_delete S vpg pasz) obtain d where "d>0" and d: "\g h. \valid_path g; valid_path h; \t\{0..1}. cmod (g t - \ t) < d \ cmod (h t - \ t) < d; pathstart h = pathstart g \ pathfinish h = pathfinish g\ - \ path_image h \ s - {z} \ (\f. f holomorphic_on s - {z} \ contour_integral h f = contour_integral g f)" - using contour_integral_nearby_ends [OF _ \path \\ pasz] s by (simp add: open_Diff) metis + \ path_image h \ S - {z} \ (\f. f holomorphic_on S - {z} \ contour_integral h f = contour_integral g f)" + using contour_integral_nearby_ends [OF _ \path \\ pasz] S by (simp add: open_Diff) metis obtain p where polyp: "polynomial_function p" and ps: "pathstart p = pathstart \" and pf: "pathfinish p = pathfinish \" and led: "\t\{0..1}. cmod (p t - \ t) < d" using path_approx_polynomial_function [OF \path \\ \d > 0\] by blast then have ploop: "pathfinish p = pathstart p" using loop by auto have vpp: "valid_path p" using polyp valid_path_polynomial_function by blast have [simp]: "z \ path_image \" using pasz by blast - have paps: "path_image p \ s - {z}" and cint_eq: "(\f. f holomorphic_on s - {z} \ contour_integral p f = contour_integral \ f)" + have paps: "path_image p \ S - {z}" and cint_eq: "(\f. f holomorphic_on S - {z} \ contour_integral p f = contour_integral \ f)" using pf ps led d [OF vpg vpp] \d > 0\ by auto have wn_eq: "winding_number p z = winding_number \ z" using vpp paps by (simp add: subset_Diff_insert vpg valid_path_polynomial_function winding_number_valid_path cint_eq hols) - have "winding_number p w = winding_number \ w" if "w \ s" for w + have "winding_number p w = winding_number \ w" if "w \ S" for w proof - - have hol: "(\v. 1 / (v - w)) holomorphic_on s - {z}" + have hol: "(\v. 1 / (v - w)) holomorphic_on S - {z}" using that by (force intro: holomorphic_intros holomorphic_on_subset [OF holf]) have "w \ path_image p" "w \ path_image \" using paps pasz that by auto then show ?thesis using vpp vpg by (simp add: subset_Diff_insert valid_path_polynomial_function winding_number_valid_path cint_eq [OF hol]) qed - then have wn0: "\w. w \ s \ winding_number p w = 0" + then have wn0: "\w. w \ S \ winding_number p w = 0" by (simp add: zero) show ?thesis - using Cauchy_integral_formula_global_weak [OF s holf z polyp paps ploop wn0] hols + using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq) qed theorem Cauchy_theorem_global: - assumes s: "open s" and holf: "f holomorphic_on s" + assumes S: "open S" and holf: "f holomorphic_on S" and vpg: "valid_path \" and loop: "pathfinish \ = pathstart \" - and pas: "path_image \ \ s" - and zero: "\w. w \ s \ winding_number \ w = 0" + and pas: "path_image \ \ S" + and zero: "\w. w \ S \ winding_number \ w = 0" shows "(f has_contour_integral 0) \" proof - - obtain z where "z \ s" and znot: "z \ path_image \" + obtain z where "z \ S" and znot: "z \ path_image \" proof - have "compact (path_image \)" using compact_valid_path_image vpg by blast - then have "path_image \ \ s" - by (metis (no_types) compact_open path_image_nonempty s) + then have "path_image \ \ S" + by (metis (no_types) compact_open path_image_nonempty S) with pas show ?thesis by (blast intro: that) qed - then have pasz: "path_image \ \ s - {z}" using pas by blast - have hol: "(\w. (w - z) * f w) holomorphic_on s" + then have pasz: "path_image \ \ S - {z}" using pas by blast + have hol: "(\w. (w - z) * f w) holomorphic_on S" by (rule holomorphic_intros holf)+ show ?thesis - using Cauchy_integral_formula_global [OF s hol \z \ s\ vpg pasz loop zero] + using Cauchy_integral_formula_global [OF S hol \z \ S\ vpg pasz loop zero] by (auto simp: znot elim!: has_contour_integral_eq) qed corollary Cauchy_theorem_global_outside: - assumes "open s" "f holomorphic_on s" "valid_path \" "pathfinish \ = pathstart \" "path_image \ \ s" - "\w. w \ s \ w \ outside(path_image \)" + assumes "open S" "f holomorphic_on S" "valid_path \" "pathfinish \ = pathstart \" "path_image \ \ S" + "\w. w \ S \ w \ outside(path_image \)" shows "(f has_contour_integral 0) \" by (metis Cauchy_theorem_global assms winding_number_zero_in_outside valid_path_imp_path) lemma simply_connected_imp_winding_number_zero: - assumes "simply_connected s" "path g" - "path_image g \ s" "pathfinish g = pathstart g" "z \ s" + assumes "simply_connected S" "path g" + "path_image g \ S" "pathfinish g = pathstart g" "z \ S" shows "winding_number g z = 0" proof - have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z" apply (rule winding_number_homotopic_paths) apply (rule homotopic_loops_imp_homotopic_paths_null [where a = "pathstart g"]) - apply (rule homotopic_loops_subset [of s]) + apply (rule homotopic_loops_subset [of S]) using assms apply (auto simp: homotopic_paths_imp_homotopic_loops path_defs simply_connected_eq_contractible_path) done @@ -7375,8 +7385,8 @@ qed lemma Cauchy_theorem_simply_connected: - assumes "open s" "simply_connected s" "f holomorphic_on s" "valid_path g" - "path_image g \ s" "pathfinish g = pathstart g" + assumes "open S" "simply_connected S" "f holomorphic_on S" "valid_path g" + "path_image g \ S" "pathfinish g = pathstart g" shows "(f has_contour_integral 0) g" using assms apply (simp add: simply_connected_eq_contractible_path) diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 21 15:04:01 2017 +0000 @@ -1386,7 +1386,7 @@ else Ln(z) - \ * of_real(3 * pi/2))" using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z] - by (auto simp: Ln_times) + by (simp add: Ln_times) auto lemma Ln_of_nat: "0 < n \ Ln (of_nat n) = of_real (ln (of_nat n))" by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Feb 21 15:04:01 2017 +0000 @@ -14,8 +14,8 @@ lemma Cauchy_higher_deriv_bound: assumes holf: "f holomorphic_on (ball z r)" and contf: "continuous_on (cball z r) f" + and fin : "\w. w \ ball z r \ f w \ ball y B0" and "0 < r" and "0 < n" - and fin : "\w. w \ ball z r \ f w \ ball y B0" shows "norm ((deriv ^^ n) f z) \ (fact n) * B0 / r^n" proof - have "0 < B0" using \0 < r\ fin [of z] diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Feb 21 15:04:01 2017 +0000 @@ -1369,19 +1369,6 @@ by (auto simp add:norm_minus_commute) qed -lemma norm_minus_eqI: "x = - y \ norm x = norm y" by auto - -lemma Min_grI: - assumes "finite A" "A \ {}" "\a\A. x < a" - shows "x < Min A" - unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto - -lemma norm_lt: "norm x < norm y \ inner x x < inner y y" - unfolding norm_eq_sqrt_inner by simp - -lemma norm_le: "norm x \ norm y \ inner x x \ inner y y" - unfolding norm_eq_sqrt_inner by simp - subsection \Affine set and affine hull\ @@ -8474,19 +8461,8 @@ assume as: "\i\Basis. 0 < x \ i" "sum (op \ x) Basis < 1" obtain a :: 'b where "a \ UNIV" using UNIV_witness .. let ?d = "(1 - sum (op \ x) Basis) / real (DIM('a))" - have "Min ((op \ x) ` Basis) > 0" - apply (rule Min_grI) - using as(1) - apply auto - done - moreover have "?d > 0" - using as(2) by (auto simp: Suc_le_eq DIM_positive) - ultimately show "\e>0. \y. dist x y < e \ (\i\Basis. 0 \ y \ i) \ sum (op \ y) Basis \ 1" - apply (rule_tac x="min (Min ((op \ x) ` Basis)) D" for D in exI) - apply rule - defer - apply (rule, rule) - proof - + show "\e>0. \y. dist x y < e \ (\i\Basis. 0 \ y \ i) \ sum (op \ y) Basis \ 1" + proof (rule_tac x="min (Min ((op \ x) ` Basis)) D" for D in exI, intro conjI impI allI) fix y assume y: "dist x y < min (Min (op \ x ` Basis)) ?d" have "sum (op \ y) Basis \ sum (\i. x\i + ?d) Basis" @@ -8505,7 +8481,8 @@ also have "\ \ 1" unfolding sum.distrib sum_constant by (auto simp add: Suc_le_eq) - finally show "(\i\Basis. 0 \ y \ i) \ sum (op \ y) Basis \ 1" + finally show "sum (op \ y) Basis \ 1" . + show "(\i\Basis. 0 \ y \ i)" proof safe fix i :: 'a assume i: "i \ Basis" @@ -8519,7 +8496,14 @@ using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format, OF i] by (auto simp: inner_simps) qed - qed auto + next + have "Min ((op \ x) ` Basis) > 0" + using as by simp + moreover have "?d > 0" + using as by (auto simp: Suc_le_eq) + ultimately show "0 < min (Min (op \ x ` Basis)) ((1 - sum (op \ x) Basis) / real DIM('a))" + by linarith + qed qed lemma interior_std_simplex_nonempty: @@ -8655,7 +8639,7 @@ have "0 < card d" using \d \ {}\ \finite d\ by (simp add: card_gt_0_iff) have "Min ((op \ x) ` d) > 0" - using as \d \ {}\ \finite d\ by (simp add: Min_grI) + using as \d \ {}\ \finite d\ by (simp add: Min_gr_iff) moreover have "?d > 0" using as using \0 < card d\ by auto ultimately have h3: "min (Min ((op \ x) ` d)) ?d > 0" by auto diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Finite_Product_Measure.thy --- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy Tue Feb 21 15:04:01 2017 +0000 @@ -1135,7 +1135,7 @@ proof (intro PiM_eqI) fix A assume A: "\ia. ia \ {i} \ A ia \ sets (M ia)" then have "(\x. \i\{i}. x) -` Pi\<^sub>E {i} A \ space (M i) = A i" - by (auto dest: sets.sets_into_space) + by (fastforce dest: sets.sets_into_space) with A show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\x. \i\{i}. x)) (Pi\<^sub>E {i} A) = (\i\{i}. emeasure (M i) (A i))" by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict) qed simp_all diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Function_Topology.thy Tue Feb 21 15:04:01 2017 +0000 @@ -967,7 +967,7 @@ by blast define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \ I}" have "m > 0" if "I\{}" - unfolding m_def apply (rule Min_grI) using \finite I\ \I \ {}\ \\i. e i > 0\ by auto + unfolding m_def Min_gr_iff using \finite I\ \I \ {}\ \\i. e i > 0\ by auto moreover have "{y. dist x y < m} \ U" proof (auto) fix y assume "dist x y < m" diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Feb 21 15:04:01 2017 +0000 @@ -9,10 +9,7 @@ Lebesgue_Measure Tagged_Division begin -(* BEGIN MOVE *) -lemma norm_minus2: "norm (x1-x2, y1-y2) = norm (x2-x1, y2-y1)" - by (simp add: norm_minus_eqI) - +(* try instead structured proofs below *) lemma norm_diff2: "\y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \ e1; norm(y2 - x2) \ e2\ \ norm(y - x) \ e" using norm_triangle_mono [of "y1 - x1" "e1" "y2 - x2" "e2"] @@ -7696,10 +7693,12 @@ assume xuvwz: "x1 \ cbox u v" "x2 \ cbox w z" then have x: "x1 \ cbox a b" "x2 \ cbox c d" using uwvz_sub by auto - have "norm (x1 - t1, x2 - t2) < k" + have "norm (x1 - t1, x2 - t2) = norm (t1 - x1, t2 - x2)" + by (simp add: norm_Pair norm_minus_commute) + also have "norm (t1 - x1, t2 - x2) < k" using xuvwz ls uwvz_sub unfolding ball_def - by (force simp add: cbox_Pair_eq dist_norm norm_minus2) - then have "norm (f (x1,x2) - f (t1,t2)) \ e / content ?CBOX / 2" + by (force simp add: cbox_Pair_eq dist_norm ) + finally have "norm (f (x1,x2) - f (t1,t2)) \ e / content ?CBOX / 2" using nf [OF t x] by simp } note nf' = this have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)" @@ -7852,7 +7851,7 @@ finally show ?thesis . qed (insert a, simp_all add: integral_f) thus "bounded {integral {c..} (f k) |k. True}" - by (intro bounded_realI[of _ "exp (-a*c)/a"]) auto + by (intro boundedI[of _ "exp (-a*c)/a"]) auto qed (auto simp: f_def) from eventually_gt_at_top[of "nat \c\"] have "eventually (\k. of_nat k > c) sequentially" @@ -7945,7 +7944,7 @@ finally have "abs (F k) \ c powr (a + 1) / (a + 1)" . } thus "bounded {integral {0..c} (f k) |k. True}" - by (intro bounded_realI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f) + by (intro boundedI[of _ "c powr (a+1) / (a+1)"]) (auto simp: integral_f) qed from False c have "c > 0" by simp diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Feb 21 15:04:01 2017 +0000 @@ -92,12 +92,6 @@ "finite I \ (\i. i \ I \ countable (F i)) \ countable (Pi\<^sub>E I F)" by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) -lemma continuous_on_cases: - "closed s \ closed t \ continuous_on s f \ continuous_on t g \ - \x. (x\s \ \ P x) \ (x \ t \ P x) \ f x = g x \ - continuous_on (s \ t) (\x. if P x then f x else g x)" - by (rule continuous_on_If) auto - lemma open_sums: fixes T :: "('b::real_normed_vector) set" assumes "open S \ open T" @@ -3946,11 +3940,10 @@ lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X" by (simp add: bounded_iff bdd_above_def) -lemma bounded_realI: - assumes "\x\s. \x::real\ \ B" - shows "bounded s" - unfolding bounded_def dist_real_def - by (metis abs_minus_commute assms diff_0_right) +lemma boundedI: + assumes "\x. x \ S \ norm x \ B" + shows "bounded S" + using assms bounded_iff by blast lemma bounded_empty [simp]: "bounded {}" by (simp add: bounded_def) @@ -5100,7 +5093,7 @@ "compact (s :: 'a::metric_space set) \ seq_compact s" using compact_imp_seq_compact seq_compact_imp_heine_borel by blast -lemma compact_def: +lemma compact_def: --\this is the definition of compactness in HOL Light\ "compact (S :: 'a::metric_space set) \ (\f. (\n. f n \ S) \ (\l\S. \r. subseq r \ (f \ r) \ l))" unfolding compact_eq_seq_compact_metric seq_compact_def by auto @@ -7576,48 +7569,6 @@ qed (insert D, auto) qed auto -text \A uniformly convergent limit of continuous functions is continuous.\ - -lemma continuous_uniform_limit: - fixes f :: "'a \ 'b::metric_space \ 'c::metric_space" - assumes "\ trivial_limit F" - and "eventually (\n. continuous_on s (f n)) F" - and "\e>0. eventually (\n. \x\s. dist (f n x) (g x) < e) F" - shows "continuous_on s g" -proof - - { - fix x and e :: real - assume "x\s" "e>0" - have "eventually (\n. \x\s. dist (f n x) (g x) < e / 3) F" - using \e>0\ assms(3)[THEN spec[where x="e/3"]] by auto - from eventually_happens [OF eventually_conj [OF this assms(2)]] - obtain n where n:"\x\s. dist (f n x) (g x) < e / 3" "continuous_on s (f n)" - using assms(1) by blast - have "e / 3 > 0" using \e>0\ by auto - then obtain d where "d>0" and d:"\x'\s. dist x' x < d \ dist (f n x') (f n x) < e / 3" - using n(2)[unfolded continuous_on_iff, THEN bspec[where x=x], OF \x\s\, THEN spec[where x="e/3"]] by blast - { - fix y - assume "y \ s" and "dist y x < d" - then have "dist (f n y) (f n x) < e / 3" - by (rule d [rule_format]) - then have "dist (f n y) (g x) < 2 * e / 3" - using dist_triangle [of "f n y" "g x" "f n x"] - using n(1)[THEN bspec[where x=x], OF \x\s\] - by auto - then have "dist (g y) (g x) < e" - using n(1)[THEN bspec[where x=y], OF \y\s\] - using dist_triangle3 [of "g y" "g x" "f n y"] - by auto - } - then have "\d>0. \x'\s. dist x' x < d \ dist (g x') (g x) < e" - using \d>0\ by auto - } - then show ?thesis - unfolding continuous_on_iff by auto -qed - - subsection \Topological stuff about the set of Reals\ lemma open_real: diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Analysis/Uniform_Limit.thy --- a/src/HOL/Analysis/Uniform_Limit.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Analysis/Uniform_Limit.thy Tue Feb 21 15:04:01 2017 +0000 @@ -472,6 +472,73 @@ bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult] bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR] +lemma uniform_lim_mult: + fixes f :: "'a \ 'b \ 'c::real_normed_algebra" + assumes f: "uniform_limit S f l F" + and g: "uniform_limit S g m F" + and l: "bounded (l ` S)" + and m: "bounded (m ` S)" + shows "uniform_limit S (\a b. f a b * g a b) (\a. l a * m a) F" + by (intro bounded_bilinear_bounded_uniform_limit_intros assms) + +lemma uniform_lim_inverse: + fixes f :: "'a \ 'b \ 'c::real_normed_field" + assumes f: "uniform_limit S f l F" + and b: "\x. x \ S \ b \ norm(l x)" + and "b > 0" + shows "uniform_limit S (\x y. inverse (f x y)) (inverse \ l) F" +proof (rule uniform_limitI) + fix e::real + assume "e > 0" + have lte: "dist (inverse (f x y)) ((inverse \ l) y) < e" + if "b/2 \ norm (f x y)" "norm (f x y - l y) < e * b\<^sup>2 / 2" "y \ S" + for x y + proof - + have [simp]: "l y \ 0" "f x y \ 0" + using \b > 0\ that b [OF \y \ S\] by fastforce+ + have "norm (l y - f x y) < e * b\<^sup>2 / 2" + by (metis norm_minus_commute that(2)) + also have "... \ e * (norm (f x y) * norm (l y))" + using \e > 0\ that b [OF \y \ S\] apply (simp add: power2_eq_square) + by (metis \b > 0\ less_eq_real_def mult.left_commute mult_mono') + finally show ?thesis + by (auto simp: dist_norm divide_simps norm_mult norm_divide) + qed + have "\\<^sub>F n in F. \x\S. dist (f n x) (l x) < b/2" + using uniform_limitD [OF f, of "b/2"] by (simp add: \b > 0\) + then have "\\<^sub>F x in F. \y\S. b/2 \ norm (f x y)" + apply (rule eventually_mono) + using b apply (simp only: dist_norm) + by (metis (no_types, hide_lams) diff_zero dist_commute dist_norm norm_triangle_half_l not_less) + then have "\\<^sub>F x in F. \y\S. b/2 \ norm (f x y) \ norm (f x y - l y) < e * b\<^sup>2 / 2" + apply (simp only: ball_conj_distrib dist_norm [symmetric]) + apply (rule eventually_conj, assumption) + apply (rule uniform_limitD [OF f, of "e * b ^ 2 / 2"]) + using \b > 0\ \e > 0\ by auto + then show "\\<^sub>F x in F. \y\S. dist (inverse (f x y)) ((inverse \ l) y) < e" + using lte by (force intro: eventually_mono) +qed + +lemma uniform_lim_div: + fixes f :: "'a \ 'b \ 'c::real_normed_field" + assumes f: "uniform_limit S f l F" + and g: "uniform_limit S g m F" + and l: "bounded (l ` S)" + and b: "\x. x \ S \ b \ norm(m x)" + and "b > 0" + shows "uniform_limit S (\a b. f a b / g a b) (\a. l a / m a) F" +proof - + have m: "bounded ((inverse \ m) ` S)" + using b \b > 0\ + apply (simp add: bounded_iff) + by (metis le_imp_inverse_le norm_inverse) + have "uniform_limit S (\a b. f a b * inverse (g a b)) + (\a. l a * (inverse \ m) a) F" + by (rule uniform_lim_mult [OF f uniform_lim_inverse [OF g b \b > 0\] l m]) + then show ?thesis + by (simp add: field_class.field_divide_inverse) +qed + lemma uniform_limit_null_comparison: assumes "\\<^sub>F x in F. \a\S. norm (f x a) \ g x a" assumes "uniform_limit S g (\_. 0) F" @@ -482,7 +549,7 @@ using assms(1) by (rule eventually_mono) (force simp add: dist_norm) qed -lemma uniform_limit_on_union: +lemma uniform_limit_on_Un: "uniform_limit I f g F \ uniform_limit J f g F \ uniform_limit (I \ J) f g F" by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2) @@ -495,7 +562,7 @@ assumes "\s. s \ S \ uniform_limit (h s) f g F" shows "uniform_limit (UNION S h) f g F" using assms - by induct (auto intro: uniform_limit_on_empty uniform_limit_on_union) + by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un) lemma uniform_limit_on_Union: assumes "finite I" @@ -523,7 +590,6 @@ unfolding uniformly_convergent_on_def by (blast dest: bounded_linear_uniform_limit_intros(13)) - subsection\Power series and uniform convergence\ proposition powser_uniformly_convergent: diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Limits.thy Tue Feb 21 15:04:01 2017 +0000 @@ -1696,7 +1696,7 @@ unfolding tendsto_def eventually_sequentially by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute) -lemma Bseq_inverse_lemma: "r \ norm x \ 0 < r \ norm (inverse x) \ inverse r" +lemma norm_inverse_le_norm: "r \ norm x \ 0 < r \ norm (inverse x) \ inverse r" for x :: "'a::real_normed_div_algebra" apply (subst nonzero_norm_inverse, clarsimp) apply (erule (1) le_imp_inverse_le) diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Tue Feb 21 15:04:01 2017 +0000 @@ -1128,6 +1128,18 @@ lemma dist_triangle_half_r: "dist y x1 < e / 2 \ dist y x2 < e / 2 \ dist x1 x2 < e" by (rule dist_triangle_half_l) (simp_all add: dist_commute) +lemma dist_triangle_third: + assumes "dist x1 x2 < e/3" "dist x2 x3 < e/3" "dist x3 x4 < e/3" + shows "dist x1 x4 < e" +proof - + have "dist x1 x3 < e/3 + e/3" + by (metis assms(1) assms(2) dist_commute dist_triangle_less_add) + then have "dist x1 x4 < (e/3 + e/3) + e/3" + by (metis assms(3) dist_commute dist_triangle_less_add) + then show ?thesis + by simp +qed + subclass uniform_space proof fix E x diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Topological_Spaces.thy Tue Feb 21 15:04:01 2017 +0000 @@ -468,9 +468,9 @@ "eventually P (nhds a) \ (\S. open S \ a \ S \ (\x\S. P x))" unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal) -lemma eventually_eventually: +lemma eventually_eventually: "eventually (\y. eventually P (nhds y)) (nhds x) = eventually P (nhds x)" - by (auto simp: eventually_nhds) + by (auto simp: eventually_nhds) lemma (in topological_space) eventually_nhds_in_open: "open s \ x \ s \ eventually (\y. y \ s) (nhds x)" @@ -1050,6 +1050,12 @@ definition subseq :: "(nat \ nat) \ bool" where "subseq f \ (\m. \n>m. f m < f n)" +lemma subseq_le_mono: "subseq r \ m \ n \ r m \ r n" + by (simp add: less_mono_imp_le_mono subseq_def) + +lemma subseq_id: "subseq id" + by (simp add: subseq_def) + lemma incseq_SucI: "(\n. X n \ X (Suc n)) \ incseq X" using lift_Suc_mono_le[of X] by (auto simp: incseq_def) @@ -1818,6 +1824,12 @@ by (rule continuous_on_closed_Un) qed +lemma continuous_on_cases: + "closed s \ closed t \ continuous_on s f \ continuous_on t g \ + \x. (x\s \ \ P x) \ (x \ t \ P x) \ f x = g x \ + continuous_on (s \ t) (\x. if P x then f x else g x)" + by (rule continuous_on_If) auto + lemma continuous_on_id[continuous_intros]: "continuous_on s (\x. x)" unfolding continuous_on_def by fast diff -r b46fe5138cb0 -r ab7e11730ad8 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Sun Feb 19 11:58:51 2017 +0100 +++ b/src/HOL/Transcendental.thy Tue Feb 21 15:04:01 2017 +0000 @@ -3194,6 +3194,12 @@ lemma diffs_cos_coeff: "diffs cos_coeff = (\n. - sin_coeff n)" by (simp add: diffs_def cos_coeff_Suc del: of_nat_Suc) +lemma sin_int_times_real: "sin (of_int m * of_real x) = of_real (sin (of_int m * x))" + by (metis sin_of_real of_real_mult of_real_of_int_eq) + +lemma cos_int_times_real: "cos (of_int m * of_real x) = of_real (cos (of_int m * x))" + by (metis cos_of_real of_real_mult of_real_of_int_eq) + text \Now at last we can get the derivatives of exp, sin and cos.\ lemma DERIV_sin [simp]: "DERIV sin x :> cos x" @@ -4077,6 +4083,9 @@ using dvd_triv_left apply fastforce done +lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0" + by (simp add: sin_zero_iff_int2) + lemma cos_monotone_0_pi: assumes "0 \ y" and "y < x" and "x \ pi" shows "cos x < cos y" @@ -4271,13 +4280,23 @@ by (metis cos_2npi cos_minus mult.assoc mult.left_commute) qed -lemma cos_one_2pi_int: "cos x = 1 \ (\n::int. x = n * 2 * pi)" - apply auto (* FIXME simproc bug? *) - apply (auto simp: cos_one_2pi) - apply (metis of_int_of_nat_eq) - apply (metis mult_minus_right of_int_minus of_int_of_nat_eq) - apply (metis mult_minus_right of_int_of_nat) - done +lemma cos_one_2pi_int: "cos x = 1 \ (\n::int. x = n * 2 * pi)" (is "?lhs = ?rhs") +proof + assume "cos x = 1" + then show ?rhs + apply (auto simp: cos_one_2pi) + apply (metis of_int_of_nat_eq) + apply (metis mult_minus_right of_int_minus of_int_of_nat_eq) + done +next + assume ?rhs + then show "cos x = 1" + by (clarsimp simp add: cos_one_2pi) (metis mult_minus_right of_int_of_nat) +qed + +lemma cos_npi_int [simp]: + fixes n::int shows "cos (pi * of_int n) = (if even n then 1 else -1)" + by (auto simp: algebra_simps cos_one_2pi_int elim!: oddE evenE) lemma sin_cos_sqrt: "0 \ sin x \ sin x = sqrt (1 - (cos(x) ^ 2))" using sin_squared_eq real_sqrt_unique by fastforce