--- 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 ***
--- 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: "\<bar>Im x\<bar> \<le> cmod x"
by (cases x) simp
+
+lemma abs_sqrt_wlog:
+ fixes x::"'a::linordered_idom"
+ assumes "\<And>x::'a. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
+by (metis abs_ge_zero assms power2_abs)
+
+lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> 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 "((\<lambda>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 \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
+proof -
+ have f: "f = (\<lambda>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 \<Rightarrow> 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) = (\<Sum>x\<in>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) = (\<Prod>x\<in>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: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
+ by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
+
+lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (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 \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
+ unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
+
+lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
+ unfolding sums_complex_iff by blast
+
+lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
+ unfolding sums_complex_iff by blast
+
+lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and> summable (\<lambda>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 (\<lambda>n. complex_of_real (f n)) \<longleftrightarrow> summable f"
+ unfolding summable_complex_iff by simp
+
+lemma summable_Re: "summable f \<Longrightarrow> summable (\<lambda>x. Re (f x))"
+ unfolding summable_complex_iff by blast
+
+lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>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 \<in> \<real> \<longleftrightarrow> 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 \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
by (metis Re_complex_of_real Reals_cases norm_of_real)
+lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
+ by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
+
+lemma series_comparison_complex:
+ fixes f:: "nat \<Rightarrow> 'a::banach"
+ assumes sg: "summable g"
+ and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
+ and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
+ shows "summable f"
+proof -
+ have g: "\<And>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 = "\<lambda>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
--- 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 \<Longrightarrow> bounded_linear f'"
by (simp add: has_derivative_def)
+lemma has_derivative_linear: "(f has_derivative f') F \<Longrightarrow> linear f'"
+ using bounded_linear.linear[OF has_derivative_bounded_linear] .
+
lemma has_derivative_ident[has_derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
by (simp add: has_derivative_def tendsto_const)
--- 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\<ge>0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
-by (metis abs_ge_zero assms power2_abs)
-
-lemma complex_abs_le_norm: "abs(Re z) + abs(Im z) \<le> 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 \<in> open_segment w z \<Longrightarrow> u \<in> 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 \<in> \<real> \<longleftrightarrow> 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 (\<lambda>x. c * x)"
+ fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
by (auto simp: linearI distrib_left)
lemma bilinear_times:
- fixes c::"'a::{real_algebra,real_vector}" shows "bilinear (\<lambda>x y::'a. x*y)"
- unfolding bilinear_def
- by (auto simp: distrib_left distrib_right intro!: linearI)
+ fixes c::"'a::real_algebra" shows "bilinear (\<lambda>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 \<Rightarrow> 'b::real_normed_algebra"
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"
- by (metis bounded_linear.uniformly_continuous_on[of "\<lambda>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 \<Rightarrow> '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 "\<forall>x\<in>(s - k). DERIV f x :> 0"
obtains c where "\<And>x. x \<in> s \<Longrightarrow> 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} \<Rightarrow> 'a"
@@ -255,7 +213,7 @@
obtains c where "(f has_derivative (\<lambda>x. x * c)) F"
proof -
obtain c where "f' = (\<lambda>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:
"(\<lambda>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:
"(\<lambda>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 \<Longrightarrow> (\<lambda>z. -(f z)) complex_differentiable F"
@@ -484,10 +441,9 @@
by (metis DERIV_power)
lemma holomorphic_on_setsum:
- "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s)
- \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) holomorphic_on s"
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>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) \<longleftrightarrow>
(\<exists>g. (\<forall>w. f(w) - f(z) = g(w) * (w - z)) \<and> 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 \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s)
- \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) I) analytic_on s"
- by (induct I rule: finite_induct) (auto simp: analytic_on_const analytic_on_add)
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>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: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
- by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
-
-lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (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 "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
shows "l \<in> \<real>"
-proof (rule Lim_in_closed_set)
- show "closed (\<real>::complex set)"
- by (rule closed_complex_Reals)
+proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)])
show "eventually (\<lambda>x. f x \<in> \<real>) F"
using assms(3, 4) by (auto intro: eventually_mono)
-qed fact+
+qed
+
lemma real_lim_sequentially:
fixes l::complex
shows "(f ---> l) sequentially \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> \<real>) \<Longrightarrow> l \<in> \<real>"
@@ -1079,66 +1024,11 @@
using assms unfolding summable_def
by (blast intro: sums_vec_nth)
-lemma sums_Re:
- assumes "f sums a"
- shows "(\<lambda>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 "(\<lambda>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 (\<lambda>x. Re (f x))"
-using assms unfolding summable_def
-by (blast intro: sums_Re)
-
-lemma summable_Im:
- assumes "summable f"
- shows "summable (\<lambda>x. Im (f x))"
-using assms unfolding summable_def
-by (blast intro: sums_Im)
-
-lemma series_comparison_complex:
- fixes f:: "nat \<Rightarrow> 'a::banach"
- assumes sg: "summable g"
- and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
- and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
- shows "summable f"
-proof -
- have g: "\<And>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 = "\<lambda>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 (\<lambda>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 \<Rightarrow> 'a::ab_group_add"
shows "setsum f {0..n} = f 0 - f (Suc n) + setsum (\<lambda>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 "\<And>u. u \<in> closed_segment w z ==> (f has_field_derivative f'(u)) (at u)"
+ assumes "\<And>u. u \<in> closed_segment w z \<Longrightarrow> (f has_field_derivative f'(u)) (at u)"
shows "\<exists>u. u \<in> open_segment w z \<and> Re(f z) - Re(f w) = Re(f'(u) * (z - w))"
proof -
have twz: "\<And>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 (\<lambda>t. (1 - t) *\<^sub>R w + t *\<^sub>R z)"
"\<lambda>u. Re o (\<lambda>h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\<lambda>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 \<Rightarrow> 'a::real_normed_vector"
- assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm(a n) * r0^n \<le> M"
- shows "summable (\<lambda>n. norm(a(n)) * r^n)"
-proof (rule summable_comparison_test' [of "\<lambda>n. M * (r / r0)^n"])
- show "summable (\<lambda>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) \<le> 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
--- 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 \<Longrightarrow> 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 \<le> 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 \<in> open_segment w z \<Longrightarrow> u \<in> closed_segment w z"
+ by (auto simp add: closed_segment_def open_segment_def)
+
definition "starlike s \<longleftrightarrow> (\<exists>a\<in>s. \<forall>x\<in>s. closed_segment a x \<subseteq> s)"
lemma midpoint_refl: "midpoint x x = x"
--- 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 \<Longrightarrow> bounded_linear f'"
- unfolding has_derivative_def by auto
-
-lemma derivative_is_linear: "(f has_derivative f') net \<Longrightarrow> 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) \<longleftrightarrow> (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) \<and> isCont g x \<and> 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 \<Longrightarrow> 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 @@
(\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 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) \<longleftrightarrow> bounded_linear f' \<and>
(\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> 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) \<longleftrightarrow>
@@ -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) \<le> 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 "\<dots> \<le> 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 \<Rightarrow> 'b::real_inner"
assumes "convex s"
- and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
+ and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
shows "\<exists>c. \<forall>x\<in>s. f x = c"
proof -
{ fix x y assume "x \<in> s" "y \<in> s"
@@ -896,14 +875,34 @@
lemma has_derivative_zero_unique:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_inner"
assumes "convex s"
- and "a \<in> s"
- and "f a = c"
- and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
- and "x \<in> s"
- shows "f x = c"
- using has_derivative_zero_constant[OF assms(1,4)]
- using assms(2-3,5)
- by auto
+ and "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
+ and "x \<in> s" "y \<in> 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 \<Rightarrow> 'b::real_inner"
+ assumes "open s" "connected s"
+ assumes f: "\<And>x. x \<in> s \<Longrightarrow> (f has_derivative (\<lambda>x. 0)) (at x)"
+ assumes "x \<in> s" "y \<in> s"
+ shows "f x = f y"
+proof (rule connected_local_const[where f=f, OF `connected s` `x\<in>s` `y\<in>s`])
+ show "\<forall>a\<in>s. eventually (\<lambda>b. f a = f b) (at a within s)"
+ proof
+ fix a assume "a \<in> s"
+ with `open s` obtain e where "0 < e" "ball a e \<subseteq> s"
+ by (rule openE)
+ then have "\<exists>c. \<forall>x\<in>ball a e. f x = c"
+ by (intro has_derivative_zero_constant)
+ (auto simp: at_within_open[OF _ open_ball] f convex_ball)
+ with `0<e` have "\<forall>x\<in>ball a e. f a = f x"
+ by auto
+ then show "eventually (\<lambda>b. f a = f b) (at a within s)"
+ using `0<e` unfolding eventually_at_topological
+ by (intro exI[of _ "ball a e"]) auto
+ qed
+qed
+
subsection {* Differentiability of inverse function (most basic form) *}
@@ -1546,11 +1545,11 @@
apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
apply (rule has_derivative_at_within)
using assms(5) and `u \<in> s` `a \<in> s`
- apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] derivative_linear)
+ apply (auto intro!: has_derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
done
have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>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 \<in> s` `a \<in> 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\<in>s`,THEN derivative_linear]
+ note lin = assms(2)[rule_format,OF `x\<in>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
--- 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) \<le> (\<Sum>i\<in>A. norm (f i))"
by (induct A rule: infinite_finite_induct) (auto intro: norm_triangle_mono)
+lemma setsum_norm_le:
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+ assumes fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
+ shows "norm (setsum f S) \<le> 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 "\<bar>norm a\<bar> = 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:
--- 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 \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> 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 \<Rightarrow> 'a::real_normed_vector"
+ assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M"
+ shows "summable (\<lambda>n. norm (a n) * r^n)"
+proof (rule summable_comparison_test')
+ show "summable (\<lambda>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) \<le> 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: