# HG changeset patch # User hoelzl # Date 1396456501 -7200 # Node ID 2704ca85be986fe7d134cc871d4083da749360ca # Parent 0646f63a02b7b0647695af89bbce084f6c190ce3 moved generic theorems from Complex_Analysis_Basic; fixed some theorem names diff -r 0646f63a02b7 -r 2704ca85be98 NEWS --- a/NEWS Wed Apr 02 17:47:56 2014 +0200 +++ b/NEWS Wed Apr 02 18:35:01 2014 +0200 @@ -563,6 +563,11 @@ explicit set-comprehensions with eucl_less for other (half-) open intervals. + - renamed theorems: + derivative_linear ~> has_derivative_bounded_linear + derivative_is_linear ~> has_derivative_linear + bounded_linear_imp_linear ~> bounded_linear.linear + *** Scala *** diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Complex.thy Wed Apr 02 18:35:01 2014 +0200 @@ -339,6 +339,21 @@ lemma abs_Im_le_cmod: "\Im x\ \ cmod x" by (cases x) simp + +lemma abs_sqrt_wlog: + fixes x::"'a::linordered_idom" + assumes "\x::'a. x \ 0 \ P x (x\<^sup>2)" shows "P \x\ (x\<^sup>2)" +by (metis abs_ge_zero assms power2_abs) + +lemma complex_abs_le_norm: "\Re z\ + \Im z\ \ sqrt 2 * norm z" + unfolding complex_norm_def + apply (rule abs_sqrt_wlog [where x="Re z"]) + apply (rule abs_sqrt_wlog [where x="Im z"]) + apply (rule power2_le_imp_le) + apply (simp_all add: power2_sum add_commute sum_squares_bound real_sqrt_mult [symmetric]) + done + + text {* Properties of complex signum. *} lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" @@ -370,6 +385,20 @@ lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re] lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im] +lemma continuous_Re: "continuous_on X Re" + by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re + continuous_on_cong continuous_on_id) + +lemma continuous_Im: "continuous_on X Im" + by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im + continuous_on_cong continuous_on_id) + +lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F" + by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const) + +lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F" + by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const) + lemma tendsto_Complex [tendsto_intros]: assumes "(f ---> a) F" and "(g ---> b) F" shows "((\x. Complex (f x) (g x)) ---> Complex a b) F" @@ -387,6 +416,20 @@ (simp add: dist_norm real_sqrt_sum_squares_less) qed + +lemma tendsto_complex_iff: + "(f ---> x) F \ (((\x. Re (f x)) ---> Re x) F \ ((\x. Im (f x)) ---> Im x) F)" +proof - + have f: "f = (\x. Complex (Re (f x)) (Im (f x)))" and x: "x = Complex (Re x) (Im x)" + by simp_all + show ?thesis + apply (subst f) + apply (subst x) + apply (intro iffI tendsto_Complex conjI) + apply (simp_all add: tendsto_Re tendsto_Im) + done +qed + instance complex :: banach proof fix X :: "nat \ complex" @@ -489,6 +532,9 @@ lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y" by (simp add: complex_eq_iff) +lemma cnj_setsum: "cnj (setsum f s) = (\x\s. cnj (f x))" + by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_add) + lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y" by (simp add: complex_eq_iff) @@ -501,6 +547,9 @@ lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y" by (simp add: complex_eq_iff) +lemma cnj_setprod: "cnj (setprod f s) = (\x\s. cnj (f x))" + by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_mult) + lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)" by (simp add: complex_inverse_def) @@ -562,6 +611,12 @@ lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj] +lemma lim_cnj: "((\x. cnj(f x)) ---> cnj l) F \ (f ---> l) F" + by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric]) + +lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)" + by (simp add: sums_def lim_cnj cnj_setsum [symmetric]) + subsection{*Basic Lemmas*} @@ -641,31 +696,43 @@ by (metis im_complex_div_gt_0 not_le) lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s" -apply (cases "finite s") - by (induct s rule: finite_induct) auto + by (induct s rule: infinite_finite_induct) auto lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s" -apply (cases "finite s") - by (induct s rule: finite_induct) auto + by (induct s rule: infinite_finite_induct) auto + +lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)" + unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum .. + +lemma sums_Re: "f sums a \ (\x. Re (f x)) sums Re a" + unfolding sums_complex_iff by blast + +lemma sums_Im: "f sums a \ (\x. Im (f x)) sums Im a" + unfolding sums_complex_iff by blast + +lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))" + unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps) + +lemma summable_complex_of_real [simp]: "summable (\n. complex_of_real (f n)) \ summable f" + unfolding summable_complex_iff by simp + +lemma summable_Re: "summable f \ summable (\x. Re (f x))" + unfolding summable_complex_iff by blast + +lemma summable_Im: "summable f \ summable (\x. Im (f x))" + unfolding summable_complex_iff by blast lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0" -apply (cases "finite s") - by (induct s rule: finite_induct) auto + by (induct s rule: infinite_finite_induct) auto lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s" by (metis Complex_setsum') -lemma cnj_setsum: "cnj (setsum f s) = setsum (%x. cnj (f x)) s" -apply (cases "finite s") - by (induct s rule: finite_induct) (auto simp: complex_cnj_add) - lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s" -apply (cases "finite s") - by (induct s rule: finite_induct) auto + by (induct s rule: infinite_finite_induct) auto lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s" -apply (cases "finite s") - by (induct s rule: finite_induct) auto + by (induct s rule: infinite_finite_induct) auto lemma Reals_cnj_iff: "z \ \ \ cnj z = z" by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj @@ -677,6 +744,27 @@ lemma in_Reals_norm: "z \ \ \ norm(z) = abs(Re z)" by (metis Re_complex_of_real Reals_cases norm_of_real) +lemma complex_is_Real_iff: "z \ \ \ Im z = 0" + by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj) + +lemma series_comparison_complex: + fixes f:: "nat \ 'a::banach" + assumes sg: "summable g" + and "\n. g n \ \" "\n. Re (g n) \ 0" + and fg: "\n. n \ N \ norm(f n) \ norm(g n)" + shows "summable f" +proof - + have g: "\n. cmod (g n) = Re (g n)" using assms + by (metis abs_of_nonneg in_Reals_norm) + show ?thesis + apply (rule summable_comparison_test' [where g = "\n. norm (g n)" and N=N]) + using sg + apply (auto simp: summable_def) + apply (rule_tac x="Re s" in exI) + apply (auto simp: g sums_Re) + apply (metis fg g) + done +qed subsection{*Finally! Polar Form for Complex Numbers*} @@ -888,4 +976,5 @@ lemmas complex_Re_Im_cancel_iff = complex_eq_iff lemmas complex_equality = complex_eqI + end diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Deriv.thy Wed Apr 02 18:35:01 2014 +0200 @@ -61,6 +61,9 @@ lemma has_derivative_bounded_linear: "(f has_derivative f') F \ bounded_linear f'" by (simp add: has_derivative_def) +lemma has_derivative_linear: "(f has_derivative f') F \ linear f'" + using bounded_linear.linear[OF has_derivative_bounded_linear] . + lemma has_derivative_ident[has_derivative_intros, simp]: "((\x. x) has_derivative (\x. x)) F" by (simp add: has_derivative_def tendsto_const) diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 02 18:35:01 2014 +0200 @@ -10,46 +10,10 @@ subsection {*Complex number lemmas *} -lemma abs_sqrt_wlog: - fixes x::"'a::linordered_idom" - assumes "!!x::'a. x\0 \ P x (x\<^sup>2)" shows "P \x\ (x\<^sup>2)" -by (metis abs_ge_zero assms power2_abs) - -lemma complex_abs_le_norm: "abs(Re z) + abs(Im z) \ sqrt(2) * norm z" -proof (cases z) - case (Complex x y) - show ?thesis - apply (rule power2_le_imp_le) - apply (auto simp: real_sqrt_mult [symmetric] Complex) - apply (rule abs_sqrt_wlog [where x=x]) - apply (rule abs_sqrt_wlog [where x=y]) - apply (simp add: power2_sum add_commute sum_squares_bound) - done -qed - -lemma continuous_Re: "continuous_on X Re" - by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re - continuous_on_cong continuous_on_id) - -lemma continuous_Im: "continuous_on X Im" - by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im - continuous_on_cong continuous_on_id) - -lemma open_closed_segment: "u \ open_segment w z \ u \ closed_segment w z" - by (auto simp add: closed_segment_def open_segment_def) - -lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F" - by (auto simp add: has_derivative_def bounded_linear_Re) - -lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F" - by (auto simp add: has_derivative_def bounded_linear_Im) - lemma fact_cancel: fixes c :: "'a::real_field" shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)" - apply (subst frac_eq_eq [OF of_nat_fact_not_zero of_nat_fact_not_zero]) - apply (simp add: algebra_simps of_nat_mult) - done + by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps) lemma shows open_halfspace_Re_lt: "open {z. Re(z) < b}" @@ -65,9 +29,6 @@ by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re isCont_Im isCont_ident isCont_const)+ -lemma complex_is_Real_iff: "z \ \ \ Im z = 0" - by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj) - lemma closed_complex_Reals: "closed (Reals :: complex set)" proof - have "(Reals :: complex set) = {z. Im z = 0}" @@ -78,16 +39,15 @@ lemma linear_times: - fixes c::"'a::{real_algebra,real_vector}" shows "linear (\x. c * x)" + fixes c::"'a::real_algebra" shows "linear (\x. c * x)" by (auto simp: linearI distrib_left) lemma bilinear_times: - fixes c::"'a::{real_algebra,real_vector}" shows "bilinear (\x y::'a. x*y)" - unfolding bilinear_def - by (auto simp: distrib_left distrib_right intro!: linearI) + fixes c::"'a::real_algebra" shows "bilinear (\x y::'a. x*y)" + by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) lemma linear_cnj: "linear cnj" - by (auto simp: linearI cnj_def) + using bounded_linear.linear[OF bounded_linear_cnj] . lemma tendsto_mult_left: fixes c::"'a::real_normed_algebra" @@ -152,7 +112,7 @@ lemma uniformly_continuous_on_cmul_right [continuous_on_intros]: fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. f x * c)" - by (metis bounded_linear.uniformly_continuous_on[of "\x. x * c"] bounded_linear_mult_left) + using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . lemma uniformly_continuous_on_cmul_left[continuous_on_intros]: fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" @@ -164,8 +124,7 @@ by (rule continuous_norm [OF continuous_ident]) lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm" - by (metis continuous_on_eq continuous_on_id continuous_on_norm) - + by (intro continuous_on_id continuous_on_norm) subsection{*DERIV stuff*} @@ -184,8 +143,7 @@ and "\x\(s - k). DERIV f x :> 0" obtains c where "\x. x \ s \ f(x) = c" using has_derivative_zero_connected_constant [OF assms(1-4)] assms -by (metis DERIV_const Derivative.has_derivative_const Diff_iff at_within_open - frechet_derivative_at has_field_derivative_def) +by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def) lemma DERIV_zero_constant: fixes f :: "'a::{real_normed_field,euclidean_space} \ 'a" @@ -255,7 +213,7 @@ obtains c where "(f has_derivative (\x. x * c)) F" proof - obtain c where "f' = (\x. x * c)" - by (metis assms derivative_linear real_bounded_linear) + by (metis assms has_derivative_bounded_linear real_bounded_linear) then show ?thesis by (metis assms that) qed @@ -336,15 +294,14 @@ lemma complex_differentiable_const: "(\z. c) complex_differentiable F" unfolding complex_differentiable_def has_field_derivative_def - apply (rule exI [where x=0]) - by (metis Derivative.has_derivative_const lambda_zero) + by (rule exI [where x=0]) + (metis has_derivative_const lambda_zero) lemma complex_differentiable_id: "(\z. z) complex_differentiable F" unfolding complex_differentiable_def has_field_derivative_def - apply (rule exI [where x=1]) - apply (simp add: lambda_one [symmetric]) - done + by (rule exI [where x=1]) + (simp add: lambda_one [symmetric]) lemma complex_differentiable_minus: "f complex_differentiable F \ (\z. -(f z)) complex_differentiable F" @@ -484,10 +441,9 @@ by (metis DERIV_power) lemma holomorphic_on_setsum: - "finite I \ (\i. i \ I \ (f i) holomorphic_on s) - \ (\x. setsum (\i. f i x) I) holomorphic_on s" + "(\i. i \ I \ (f i) holomorphic_on s) \ (\x. setsum (\i. f i x) I) holomorphic_on s" unfolding holomorphic_on_def - apply (induct I rule: finite_induct) + apply (induct I rule: infinite_finite_induct) apply (force intro: DERIV_const DERIV_add)+ done @@ -580,9 +536,6 @@ subsection{*Caratheodory characterization.*} -(*REPLACE the original version. BUT IN WHICH FILE??*) -thm Deriv.CARAT_DERIV - lemma complex_differentiable_caratheodory_at: "f complex_differentiable (at z) \ (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z) g)" @@ -796,9 +749,8 @@ by (induct n) (auto simp: analytic_on_const analytic_on_mult) lemma analytic_on_setsum: - "finite I \ (\i. i \ I \ (f i) analytic_on s) - \ (\x. setsum (\i. f i x) I) analytic_on s" - by (induct I rule: finite_induct) (auto simp: analytic_on_const analytic_on_add) + "(\i. i \ I \ (f i) analytic_on s) \ (\x. setsum (\i. f i x) I) analytic_on s" + by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add) subsection{*analyticity at a point.*} @@ -1025,12 +977,6 @@ subsection{*Further useful properties of complex conjugation*} -lemma lim_cnj: "((\x. cnj(f x)) ---> cnj l) F \ (f ---> l) F" - by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric]) - -lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)" - by (simp add: sums_def lim_cnj cnj_setsum [symmetric]) - lemma continuous_within_cnj: "continuous (at z within s) cnj" by (metis bounded_linear_cnj linear_continuous_within) @@ -1043,12 +989,11 @@ fixes l::complex assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\a. P a \ f a \ \" shows "l \ \" -proof (rule Lim_in_closed_set) - show "closed (\::complex set)" - by (rule closed_complex_Reals) +proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)]) show "eventually (\x. f x \ \) F" using assms(3, 4) by (auto intro: eventually_mono) -qed fact+ +qed + lemma real_lim_sequentially: fixes l::complex shows "(f ---> l) sequentially \ (\N. \n\N. f n \ \) \ l \ \" @@ -1079,66 +1024,11 @@ using assms unfolding summable_def by (blast intro: sums_vec_nth) -lemma sums_Re: - assumes "f sums a" - shows "(\x. Re (f x)) sums Re a" -using assms -by (auto simp: sums_def Re_setsum [symmetric] isCont_tendsto_compose [of a Re]) - -lemma sums_Im: - assumes "f sums a" - shows "(\x. Im (f x)) sums Im a" -using assms -by (auto simp: sums_def Im_setsum [symmetric] isCont_tendsto_compose [of a Im]) - -lemma summable_Re: - assumes "summable f" - shows "summable (\x. Re (f x))" -using assms unfolding summable_def -by (blast intro: sums_Re) - -lemma summable_Im: - assumes "summable f" - shows "summable (\x. Im (f x))" -using assms unfolding summable_def -by (blast intro: sums_Im) - -lemma series_comparison_complex: - fixes f:: "nat \ 'a::banach" - assumes sg: "summable g" - and "\n. g n \ \" "\n. Re (g n) \ 0" - and fg: "\n. n \ N \ norm(f n) \ norm(g n)" - shows "summable f" -proof - - have g: "\n. cmod (g n) = Re (g n)" using assms - by (metis abs_of_nonneg in_Reals_norm) - show ?thesis - apply (rule summable_comparison_test' [where g = "\n. norm (g n)" and N=N]) - using sg - apply (auto simp: summable_def) - apply (rule_tac x="Re s" in exI) - apply (auto simp: g sums_Re) - apply (metis fg g) - done -qed - -lemma summable_complex_of_real [simp]: - "summable (\n. complex_of_real (f n)) = summable f" -apply (auto simp: Series.summable_Cauchy) -apply (drule_tac x = e in spec, auto) -apply (rule_tac x=N in exI) -apply (auto simp: of_real_setsum [symmetric]) -done - - - - lemma setsum_Suc_reindex: fixes f :: "nat \ 'a::ab_group_add" shows "setsum f {0..n} = f 0 - f (Suc n) + setsum (\i. f (Suc i)) {0..n}" by (induct n) auto - text{*A kind of complex Taylor theorem.*} lemma complex_taylor: assumes s: "convex s" @@ -1238,22 +1128,22 @@ text{* Something more like the traditional MVT for real components.*} lemma complex_mvt_line: - assumes "\u. u \ closed_segment w z ==> (f has_field_derivative f'(u)) (at u)" + assumes "\u. u \ closed_segment w z \ (f has_field_derivative f'(u)) (at u)" shows "\u. u \ open_segment w z \ Re(f z) - Re(f w) = Re(f'(u) * (z - w))" proof - have twz: "\t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)" by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) + note assms[unfolded has_field_derivative_def, has_derivative_intros] show ?thesis apply (cut_tac mvt_simple [of 0 1 "Re o f o (\t. (1 - t) *\<^sub>R w + t *\<^sub>R z)" "\u. Re o (\h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\t. t *\<^sub>R (z - w))"]) apply auto apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI) - apply (simp add: open_segment_def) - apply (auto simp add: twz) - apply (rule has_derivative_at_within) - apply (intro has_derivative_intros has_derivative_add [OF has_derivative_const, simplified])+ - apply (rule assms [unfolded has_field_derivative_def]) + apply (auto simp add: open_segment_def twz) [] + apply (intro has_derivative_eq_intros has_derivative_at_within) + apply simp_all + apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib) apply (force simp add: twz closed_segment_def) done qed @@ -1309,24 +1199,4 @@ done qed -text{*Relations among convergence and absolute convergence for power series.*} -lemma abel_lemma: - fixes a :: "nat \ 'a::real_normed_vector" - assumes r: "0 \ r" and r0: "r < r0" and M: "\n. norm(a n) * r0^n \ M" - shows "summable (\n. norm(a(n)) * r^n)" -proof (rule summable_comparison_test' [of "\n. M * (r / r0)^n"]) - show "summable (\n. M * (r / r0) ^ n)" - using assms - by (auto simp add: summable_mult summable_geometric) - next - fix n - show "norm (norm (a n) * r ^ n) \ M * (r / r0) ^ n" - using r r0 M [of n] - apply (auto simp add: abs_mult field_simps power_divide) - apply (cases "r=0", simp) - apply (cases n, auto) - done -qed - - end diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 02 18:35:01 2014 +0200 @@ -5875,14 +5875,6 @@ by (induct set: finite, simp, simp add: convex_hull_set_plus) qed simp -lemma bounded_linear_imp_linear: "bounded_linear f \ linear f" (* TODO: move elsewhere *) -proof - - assume "bounded_linear f" - then interpret f: bounded_linear f . - show "linear f" - by (simp add: f.add f.scaleR linear_iff) -qed - lemma convex_hull_eq_real_cbox: fixes x y :: real assumes "x \ y" shows "convex hull {x, y} = cbox x y" @@ -6295,6 +6287,9 @@ lemmas segment = open_segment_def closed_segment_def +lemma open_closed_segment: "u \ open_segment w z \ u \ closed_segment w z" + by (auto simp add: closed_segment_def open_segment_def) + definition "starlike s \ (\a\s. \x\s. closed_segment a x \ s)" lemma midpoint_refl: "midpoint x x = x" diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Apr 02 18:35:01 2014 +0200 @@ -9,16 +9,6 @@ imports Brouwer_Fixpoint Operator_Norm begin -lemma bounded_linear_imp_linear: (* TODO: move elsewhere *) - assumes "bounded_linear f" - shows "linear f" -proof - - interpret f: bounded_linear f - using assms . - show ?thesis - by (simp add: f.add f.scaleR linear_iff) -qed - lemma netlimit_at_vector: (* TODO: move *) fixes a :: "'a::real_normed_vector" shows "netlimit (at a) = a" @@ -37,22 +27,15 @@ (* Because I do not want to type this all the time *) lemmas linear_linear = linear_conv_bounded_linear[symmetric] -lemma derivative_linear[dest]: "(f has_derivative f') net \ bounded_linear f'" - unfolding has_derivative_def by auto - -lemma derivative_is_linear: "(f has_derivative f') net \ linear f'" - by (rule derivative_linear [THEN bounded_linear_imp_linear]) +declare has_derivative_bounded_linear[dest] subsection {* Derivatives *} subsubsection {* Combining theorems. *} lemmas has_derivative_id = has_derivative_ident -lemmas has_derivative_const = has_derivative_const lemmas has_derivative_neg = has_derivative_minus -lemmas has_derivative_add = has_derivative_add lemmas has_derivative_sub = has_derivative_diff -lemmas has_derivative_setsum = has_derivative_setsum lemmas scaleR_right_has_derivative = has_derivative_scaleR_right lemmas scaleR_left_has_derivative = has_derivative_scaleR_left lemmas inner_right_has_derivative = has_derivative_inner_right @@ -176,11 +159,6 @@ by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within) qed -lemma CARAT_DERIV: (*FIXME: REPLACES THE ONE IN Deriv.thy*) - "(DERIV f x :> l) \ (\g. (\z. f z - f x = g z * (z - x)) \ isCont g x \ g x = l)" -by (rule DERIV_caratheodory_within) - - subsubsection {* Limit transformation for derivatives *} lemma has_derivative_transform_within: @@ -275,7 +253,7 @@ lemma linear_frechet_derivative: "f differentiable net \ linear (frechet_derivative f net)" unfolding frechet_derivative_works has_derivative_def - by (auto intro: bounded_linear_imp_linear) + by (auto intro: bounded_linear.linear) subsection {* Differentiability implies continuity *} @@ -322,14 +300,14 @@ (\e>0. \d>0. \y\s. norm(y - x) < d \ norm (f y - f x - f' (y - x)) \ e * norm (y - x))" unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap eventually_at dist_norm diff_add_eq_diff_diff - by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq) + by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq) lemma has_derivative_within_alt2: "(f has_derivative f') (at x within s) \ bounded_linear f' \ (\e>0. eventually (\y. norm (f y - f x - f' (y - x)) \ e * norm (y - x)) (at x within s))" unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap eventually_at dist_norm diff_add_eq_diff_diff - by (force simp add: linear_0 bounded_linear_imp_linear pos_divide_le_eq) + by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq) lemma has_derivative_at_alt: "(f has_derivative f') (at x) \ @@ -372,6 +350,7 @@ subsection {* Uniqueness of derivative *} + text {* The general result is a bit messy because we need approachability of the limit point from any direction. But OK for nontrivial intervals etc. @@ -854,7 +833,7 @@ proof - case goal1 have "norm (f' x y) \ onorm (f' x) * norm y" - by (rule onorm[OF derivative_linear[OF assms(2)[rule_format,OF goal1]]]) + by (rule onorm[OF has_derivative_bounded_linear[OF assms(2)[rule_format,OF goal1]]]) also have "\ \ B * norm y" apply (rule mult_right_mono) using assms(3)[rule_format,OF goal1] @@ -881,7 +860,7 @@ lemma has_derivative_zero_constant: fixes f :: "'a::real_normed_vector \ 'b::real_inner" assumes "convex s" - and "\x\s. (f has_derivative (\h. 0)) (at x within s)" + and "\x. x \ s \ (f has_derivative (\h. 0)) (at x within s)" shows "\c. \x\s. f x = c" proof - { fix x y assume "x \ s" "y \ s" @@ -896,14 +875,34 @@ lemma has_derivative_zero_unique: fixes f :: "'a::real_normed_vector \ 'b::real_inner" assumes "convex s" - and "a \ s" - and "f a = c" - and "\x\s. (f has_derivative (\h. 0)) (at x within s)" - and "x \ s" - shows "f x = c" - using has_derivative_zero_constant[OF assms(1,4)] - using assms(2-3,5) - by auto + and "\x. x \ s \ (f has_derivative (\h. 0)) (at x within s)" + and "x \ s" "y \ s" + shows "f x = f y" + using has_derivative_zero_constant[OF assms(1,2)] assms(3-) by force + +lemma has_derivative_zero_unique_connected: + fixes f :: "'a::real_normed_vector \ 'b::real_inner" + assumes "open s" "connected s" + assumes f: "\x. x \ s \ (f has_derivative (\x. 0)) (at x)" + assumes "x \ s" "y \ s" + shows "f x = f y" +proof (rule connected_local_const[where f=f, OF `connected s` `x\s` `y\s`]) + show "\a\s. eventually (\b. f a = f b) (at a within s)" + proof + fix a assume "a \ s" + with `open s` obtain e where "0 < e" "ball a e \ s" + by (rule openE) + then have "\c. \x\ball a e. f x = c" + by (intro has_derivative_zero_constant) + (auto simp: at_within_open[OF _ open_ball] f convex_ball) + with `0x\ball a e. f a = f x" + by auto + then show "eventually (\b. f a = f b) (at a within s)" + using `0 s` `a \ s` - apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\x. x"] derivative_linear) + apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\x. x"] has_derivative_bounded_linear) done have **: "bounded_linear (\x. f' u x - f' a x)" "bounded_linear (\x. f' a x - f' u x)" apply (rule_tac[!] bounded_linear_sub) - apply (rule_tac[!] derivative_linear) + apply (rule_tac[!] has_derivative_bounded_linear) using assms(5) `u \ s` `a \ s` apply auto done @@ -1773,18 +1772,18 @@ proof fix x' y z :: 'a fix c :: real - note lin = assms(2)[rule_format,OF `x\s`,THEN derivative_linear] + note lin = assms(2)[rule_format,OF `x\s`,THEN has_derivative_bounded_linear] show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply (rule tendsto_unique[OF trivial_limit_sequentially]) apply (rule lem3[rule_format]) - unfolding lin[THEN bounded_linear_imp_linear, THEN linear_cmul] + unfolding lin[THEN bounded_linear.linear, THEN linear_cmul] apply (intro tendsto_intros) apply (rule lem3[rule_format]) done show "g' x (y + z) = g' x y + g' x z" apply (rule tendsto_unique[OF trivial_limit_sequentially]) apply (rule lem3[rule_format]) - unfolding lin[THEN bounded_linear_imp_linear, THEN linear_add] + unfolding lin[THEN bounded_linear.linear, THEN linear_add] apply (rule tendsto_add) apply (rule lem3[rule_format])+ done diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Apr 02 18:35:01 2014 +0200 @@ -752,6 +752,12 @@ shows "norm (setsum f A) \ (\i\A. norm (f i))" by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono) +lemma setsum_norm_le: + fixes f :: "'a \ 'b::real_normed_vector" + assumes fg: "\x \ S. norm (f x) \ g x" + shows "norm (setsum f S) \ setsum g S" + by (rule order_trans [OF norm_setsum setsum_mono]) (simp add: fg) + lemma abs_norm_cancel [simp]: fixes a :: "'a::real_normed_vector" shows "\norm a\ = norm a" @@ -1158,6 +1164,8 @@ show ?thesis by (auto intro: order_less_imp_le) qed +lemma linear: "linear f" .. + end lemma bounded_linear_intro: diff -r 0646f63a02b7 -r 2704ca85be98 src/HOL/Series.thy --- a/src/HOL/Series.thy Wed Apr 02 17:47:56 2014 +0200 +++ b/src/HOL/Series.thy Wed Apr 02 18:35:01 2014 +0200 @@ -463,7 +463,7 @@ (*A better argument order*) lemma summable_comparison_test': "summable g \ (\n. n \ N \ norm(f n) \ g n) \ summable f" -by (rule summable_comparison_test) auto + by (rule summable_comparison_test) auto subsection {* The Ratio Test*} @@ -502,6 +502,27 @@ end +text{*Relations among convergence and absolute convergence for power series.*} + +lemma abel_lemma: + fixes a :: "nat \ 'a::real_normed_vector" + assumes r: "0 \ r" and r0: "r < r0" and M: "\n. norm (a n) * r0^n \ M" + shows "summable (\n. norm (a n) * r^n)" +proof (rule summable_comparison_test') + show "summable (\n. M * (r / r0) ^ n)" + using assms + by (auto simp add: summable_mult summable_geometric) +next + fix n + show "norm (norm (a n) * r ^ n) \ M * (r / r0) ^ n" + using r r0 M [of n] + apply (auto simp add: abs_mult field_simps power_divide) + apply (cases "r=0", simp) + apply (cases n, auto) + done +qed + + text{*Summability of geometric series for real algebras*} lemma complete_algebra_summable_geometric: