# HG changeset patch
# User hoelzl
# Date 1396279057 -7200
# Node ID 289dd9166d04b9d794a5b245aa17f6be1f0d18a3
# Parent  bea2196627cb7babeb060eb1200fe0ccde7dea4a
tuned proofs

diff -r bea2196627cb -r 289dd9166d04 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 31 12:32:15 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 31 17:17:37 2014 +0200
@@ -6,7 +6,6 @@
 
 theory Complex_Analysis_Basics
 imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
-
 begin
 
 subsection {*Complex number lemmas *}
@@ -28,11 +27,11 @@
     done
 qed
 
-lemma continuous_Re: "continuous_on UNIV Re"
+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 UNIV Im"
+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)
 
@@ -52,95 +51,29 @@
   apply (simp add: algebra_simps of_nat_mult)
   done
 
-lemma open_halfspace_Re_lt: "open {z. Re(z) < b}"
-proof -
-  have "{z. Re(z) < b} = Re -`{..<b}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Re continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma open_halfspace_Re_gt: "open {z. Re(z) > b}"
-proof -
-  have "{z. Re(z) > b} = Re -`{b<..}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Re continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
-proof -
-  have "{z. Re(z) \<ge> b} = - {z. Re(z) < b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Re_lt)
-qed
-
-lemma closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
-proof -
-  have "{z. Re(z) \<le> b} = - {z. Re(z) > b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Re_gt)
-qed
-
-lemma closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
-proof -
-  have "{z. Re(z) = b} = {z. Re(z) \<le> b} \<inter> {z. Re(z) \<ge> b}"
-    by auto
-  then show ?thesis
-    by (auto simp: closed_Int closed_halfspace_Re_le closed_halfspace_Re_ge)
-qed
-
-lemma open_halfspace_Im_lt: "open {z. Im(z) < b}"
-proof -
-  have "{z. Im(z) < b} = Im -`{..<b}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Im continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma open_halfspace_Im_gt: "open {z. Im(z) > b}"
-proof -
-  have "{z. Im(z) > b} = Im -`{b<..}"
-    by blast
-  then show ?thesis
-    by (auto simp: continuous_Im continuous_imp_open_vimage [of UNIV])
-qed
-
-lemma closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
-proof -
-  have "{z. Im(z) \<ge> b} = - {z. Im(z) < b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Im_lt)
-qed
-
-lemma closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
-proof -
-  have "{z. Im(z) \<le> b} = - {z. Im(z) > b}"
-    by auto
-  then show ?thesis
-    by (simp add: closed_def open_halfspace_Im_gt)
-qed
-
-lemma closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
-proof -
-  have "{z. Im(z) = b} = {z. Im(z) \<le> b} \<inter> {z. Im(z) \<ge> b}"
-    by auto
-  then show ?thesis
-    by (auto simp: closed_Int closed_halfspace_Im_le closed_halfspace_Im_ge)
-qed
+lemma
+  shows open_halfspace_Re_lt: "open {z. Re(z) < b}"
+    and open_halfspace_Re_gt: "open {z. Re(z) > b}"
+    and closed_halfspace_Re_ge: "closed {z. Re(z) \<ge> b}"
+    and closed_halfspace_Re_le: "closed {z. Re(z) \<le> b}"
+    and closed_halfspace_Re_eq: "closed {z. Re(z) = b}"
+    and open_halfspace_Im_lt: "open {z. Im(z) < b}"
+    and open_halfspace_Im_gt: "open {z. Im(z) > b}"
+    and closed_halfspace_Im_ge: "closed {z. Im(z) \<ge> b}"
+    and closed_halfspace_Im_le: "closed {z. Im(z) \<le> b}"
+    and closed_halfspace_Im_eq: "closed {z. Im(z) = b}"
+  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} \<union> {z. 0 < Im(z)}"
+  have "(Reals :: complex set) = {z. Im z = 0}"
     by (auto simp: complex_is_Real_iff)
   then show ?thesis
-    by (metis closed_def open_Un open_halfspace_Im_gt open_halfspace_Im_lt)
+    by (metis closed_halfspace_Im_eq)
 qed
 
 
@@ -218,25 +151,8 @@
 
 lemma uniformly_continuous_on_cmul_right [continuous_on_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  assumes "uniformly_continuous_on s f"
-  shows "uniformly_continuous_on s (\<lambda>x. f x * c)"
-proof (cases "c=0")
-  case True then show ?thesis
-    by (simp add: uniformly_continuous_on_const)
-next
-  case False show ?thesis
-    apply (rule bounded_linear.uniformly_continuous_on)
-    apply (metis bounded_linear_ident)
-    using assms
-    apply (auto simp: uniformly_continuous_on_def dist_norm)
-    apply (drule_tac x = "e / norm c" in spec, auto)
-    apply (metis divide_pos_pos zero_less_norm_iff False)
-    apply (rule_tac x=d in exI, auto)
-    apply (drule_tac x = x in bspec, assumption)
-    apply (drule_tac x = "x'" in bspec)
-    apply (auto simp: False less_divide_eq)
-    by (metis dual_order.strict_trans2 left_diff_distrib norm_mult_ineq)
-qed
+  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) 
 
 lemma uniformly_continuous_on_cmul_left[continuous_on_intros]:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
@@ -259,62 +175,6 @@
 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
   by auto
 
-lemma has_derivative_zero_constant:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "convex s"
-      and d0: "\<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 (cases "s={}")
-  case False
-  then obtain x where "x \<in> s"
-    by auto
-  have d0': "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
-    by (metis d0)
-  have "\<And>y. y \<in> s \<Longrightarrow> f x = f y"
-  proof -
-    case goal1
-    then show ?case
-      using differentiable_bound[OF assms(1) d0', of 0 x y] and `x \<in> s`
-      unfolding onorm_zero
-      by auto
-  qed
-  then show ?thesis 
-    by metis
-next
-  case True
-  then show ?thesis by auto
-qed
-
-lemma has_derivative_zero_unique:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "convex s"
-      and "\<And>x. x\<in>s \<Longrightarrow> (f has_derivative (\<lambda>h. 0)) (at x within s)"
-      and "a \<in> s"
-      and "x \<in> s"
-    shows "f x = f a"
-  using assms
-  by (metis has_derivative_zero_constant)
-
-lemma has_derivative_zero_connected_constant:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
-  assumes "connected s"
-      and "open s"
-      and "finite k"
-      and "continuous_on s f"
-      and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
-    obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
-proof (cases "s = {}")
-  case True
-  then show ?thesis
-by (metis empty_iff that)
-next
-  case False
-  then obtain c where "c \<in> s"
-    by (metis equals0I)
-  then show ?thesis
-    by (metis has_derivative_zero_unique_strong_connected assms that)
-qed
-
 lemma DERIV_zero_connected_constant:
   fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
   assumes "connected s"
@@ -342,8 +202,8 @@
       and "a \<in> s"
       and "x \<in> s"
     shows "f x = f a"
-apply (rule has_derivative_zero_unique [where f=f, OF assms(1) _ assms(3,4)])
-by (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
+  by (rule has_derivative_zero_unique [where f=f, OF assms(1,3) refl _ assms(4)])
+     (metis d0 has_field_derivative_imp_has_derivative lambda_zero)
 
 lemma DERIV_zero_connected_unique:
   fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a"
@@ -353,7 +213,7 @@
       and "a \<in> s"
       and "x \<in> s"
     shows "f x = f a" 
-    apply (rule Integration.has_derivative_zero_unique_strong_connected [of s "{}" f])
+    apply (rule has_derivative_zero_unique_strong_connected [of s "{}" f])
     using assms
     apply auto
     apply (metis DERIV_continuous_on)
@@ -365,7 +225,7 @@
       and "\<And>x. x\<in>s \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x"
     shows "(g has_field_derivative f') (at a within s)"
   using assms unfolding has_field_derivative_def
-  by (blast intro: Derivative.has_derivative_transform_within)
+  by (blast intro: has_derivative_transform_within)
 
 lemma DERIV_transform_within_open:
   assumes "DERIV f a :> f'"
@@ -1177,21 +1037,18 @@
 lemma continuous_on_cnj: "continuous_on s cnj"
 by (metis bounded_linear_cnj linear_continuous_on)
 
-subsection{*Some limit theorems about real part of real series etc.*}
+subsection {*Some limit theorems about real part of real series etc.*}
 
 lemma real_lim:
   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>"
+  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 -
-  have 1: "((\<lambda>i. Im (f i)) ---> Im l) F"
-    by (metis assms(1) tendsto_Im) 
-  then have  "((\<lambda>i. Im (f i)) ---> 0) F" using assms
-    by (metis (mono_tags, lifting) Lim_eventually complex_is_Real_iff eventually_mono)
-  then show ?thesis using 1
-    by (metis 1 assms(2) complex_is_Real_iff tendsto_unique) 
-qed
-
+proof (rule Lim_in_closed_set)
+  show "closed (\<real>::complex set)"
+    by (rule closed_complex_Reals)
+  show "eventually (\<lambda>x. f x \<in> \<real>) F"
+    using assms(3, 4) by (auto intro: eventually_mono)
+qed fact+
 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>"
@@ -1209,14 +1066,6 @@
   by (metis Lim_null_comparison complex_Re_zero tendsto_Re)
 
 
-lemma norm_setsum_bound:
-  fixes n::nat
-  shows" \<lbrakk>\<And>n. N \<le> n \<Longrightarrow> norm (f n) \<le> g n; N \<le> m\<rbrakk>
-       \<Longrightarrow> norm (setsum f {m..<n}) \<le> setsum g {m..<n}"
-apply (induct n, auto)
-by (metis dual_order.trans le_cases le_neq_implies_less norm_triangle_mono)
-
-
 (*MOVE? But not to Finite_Cartesian_Product*)
 lemma sums_vec_nth :
   assumes "f sums a"
diff -r bea2196627cb -r 289dd9166d04 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 31 12:32:15 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 31 17:17:37 2014 +0200
@@ -883,25 +883,14 @@
   assumes "convex s"
     and "\<forall>x\<in>s. (f has_derivative (\<lambda>h. 0)) (at x within s)"
   shows "\<exists>c. \<forall>x\<in>s. f x = c"
-proof (cases "s={}")
-  case False
-  then obtain x where "x \<in> s"
-    by auto
-  have "\<And>y. y \<in> s \<Longrightarrow> f x = f y"
-  proof -
-    case goal1
-    then show ?case
-      using differentiable_bound[OF assms(1-2), of 0 x y] and `x \<in> s`
-      unfolding onorm_zero
-      by auto
-  qed
+proof -
+  { fix x y assume "x \<in> s" "y \<in> s"
+    then have "norm (f x - f y) \<le> 0 * norm (x - y)"
+      using assms by (intro differentiable_bound[of s]) (auto simp: onorm_zero)
+    then have "f x = f y"
+      by simp }
   then show ?thesis
-    apply (rule_tac x="f x" in exI)
-    apply auto
-    done
-next
-  case True
-  then show ?thesis by auto
+    by metis
 qed
 
 lemma has_derivative_zero_unique:
diff -r bea2196627cb -r 289dd9166d04 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 31 12:32:15 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Mar 31 17:17:37 2014 +0200
@@ -8869,6 +8869,26 @@
     using `x \<in> s` `f c = y` `c \<in> s` by auto
 qed
 
+lemma has_derivative_zero_connected_constant:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
+  assumes "connected s"
+      and "open s"
+      and "finite k"
+      and "continuous_on s f"
+      and "\<forall>x\<in>(s - k). (f has_derivative (\<lambda>h. 0)) (at x within s)"
+    obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c"
+proof (cases "s = {}")
+  case True
+  then show ?thesis
+by (metis empty_iff that)
+next
+  case False
+  then obtain c where "c \<in> s"
+    by (metis equals0I)
+  then show ?thesis
+    by (metis has_derivative_zero_unique_strong_connected assms that)
+qed
+
 
 subsection {* Integrating characteristic function of an interval *}