src/HOL/Complex.thy
changeset 56369 2704ca85be98
parent 56331 bea2196627cb
child 56381 0556204bc230
     1.1 --- a/src/HOL/Complex.thy	Wed Apr 02 17:47:56 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Wed Apr 02 18:35:01 2014 +0200
     1.3 @@ -339,6 +339,21 @@
     1.4  lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
     1.5    by (cases x) simp
     1.6  
     1.7 +
     1.8 +lemma abs_sqrt_wlog:
     1.9 +  fixes x::"'a::linordered_idom"
    1.10 +  assumes "\<And>x::'a. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
    1.11 +by (metis abs_ge_zero assms power2_abs)
    1.12 +
    1.13 +lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> sqrt 2 * norm z"
    1.14 +  unfolding complex_norm_def
    1.15 +  apply (rule abs_sqrt_wlog [where x="Re z"])
    1.16 +  apply (rule abs_sqrt_wlog [where x="Im z"])
    1.17 +  apply (rule power2_le_imp_le)
    1.18 +  apply (simp_all add: power2_sum add_commute sum_squares_bound real_sqrt_mult [symmetric])
    1.19 +  done
    1.20 +
    1.21 +
    1.22  text {* Properties of complex signum. *}
    1.23  
    1.24  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
    1.25 @@ -370,6 +385,20 @@
    1.26  lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
    1.27  lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
    1.28  
    1.29 +lemma continuous_Re: "continuous_on X Re"
    1.30 +  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
    1.31 +            continuous_on_cong continuous_on_id)
    1.32 +
    1.33 +lemma continuous_Im: "continuous_on X Im"
    1.34 +  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
    1.35 +            continuous_on_cong continuous_on_id)
    1.36 +
    1.37 +lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
    1.38 +  by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const)
    1.39 +
    1.40 +lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
    1.41 +  by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const)
    1.42 +
    1.43  lemma tendsto_Complex [tendsto_intros]:
    1.44    assumes "(f ---> a) F" and "(g ---> b) F"
    1.45    shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
    1.46 @@ -387,6 +416,20 @@
    1.47         (simp add: dist_norm real_sqrt_sum_squares_less)
    1.48  qed
    1.49  
    1.50 +
    1.51 +lemma tendsto_complex_iff:
    1.52 +  "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
    1.53 +proof -
    1.54 +  have f: "f = (\<lambda>x. Complex (Re (f x)) (Im (f x)))" and x: "x = Complex (Re x) (Im x)"
    1.55 +    by simp_all
    1.56 +  show ?thesis
    1.57 +    apply (subst f)
    1.58 +    apply (subst x)
    1.59 +    apply (intro iffI tendsto_Complex conjI)
    1.60 +    apply (simp_all add: tendsto_Re tendsto_Im)
    1.61 +    done
    1.62 +qed
    1.63 +
    1.64  instance complex :: banach
    1.65  proof
    1.66    fix X :: "nat \<Rightarrow> complex"
    1.67 @@ -489,6 +532,9 @@
    1.68  lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
    1.69    by (simp add: complex_eq_iff)
    1.70  
    1.71 +lemma cnj_setsum: "cnj (setsum f s) = (\<Sum>x\<in>s. cnj (f x))"
    1.72 +  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_add)
    1.73 +
    1.74  lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
    1.75    by (simp add: complex_eq_iff)
    1.76  
    1.77 @@ -501,6 +547,9 @@
    1.78  lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
    1.79    by (simp add: complex_eq_iff)
    1.80  
    1.81 +lemma cnj_setprod: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
    1.82 +  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_mult)
    1.83 +
    1.84  lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
    1.85    by (simp add: complex_inverse_def)
    1.86  
    1.87 @@ -562,6 +611,12 @@
    1.88  lemmas isCont_cnj [simp] =
    1.89    bounded_linear.isCont [OF bounded_linear_cnj]
    1.90  
    1.91 +lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
    1.92 +  by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
    1.93 +
    1.94 +lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
    1.95 +  by (simp add: sums_def lim_cnj cnj_setsum [symmetric])
    1.96 +
    1.97  
    1.98  subsection{*Basic Lemmas*}
    1.99  
   1.100 @@ -641,31 +696,43 @@
   1.101    by (metis im_complex_div_gt_0 not_le)
   1.102  
   1.103  lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
   1.104 -apply (cases "finite s")
   1.105 -  by (induct s rule: finite_induct) auto
   1.106 +  by (induct s rule: infinite_finite_induct) auto
   1.107  
   1.108  lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
   1.109 -apply (cases "finite s")
   1.110 -  by (induct s rule: finite_induct) auto
   1.111 +  by (induct s rule: infinite_finite_induct) auto
   1.112 +
   1.113 +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)"
   1.114 +  unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
   1.115 +  
   1.116 +lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
   1.117 +  unfolding sums_complex_iff by blast
   1.118 +
   1.119 +lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
   1.120 +  unfolding sums_complex_iff by blast
   1.121 +
   1.122 +lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
   1.123 +  unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
   1.124 +
   1.125 +lemma summable_complex_of_real [simp]: "summable (\<lambda>n. complex_of_real (f n)) \<longleftrightarrow> summable f"
   1.126 +  unfolding summable_complex_iff by simp
   1.127 +
   1.128 +lemma summable_Re: "summable f \<Longrightarrow> summable (\<lambda>x. Re (f x))"
   1.129 +  unfolding summable_complex_iff by blast
   1.130 +
   1.131 +lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
   1.132 +  unfolding summable_complex_iff by blast
   1.133  
   1.134  lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
   1.135 -apply (cases "finite s")
   1.136 -  by (induct s rule: finite_induct) auto
   1.137 +  by (induct s rule: infinite_finite_induct) auto
   1.138  
   1.139  lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
   1.140    by (metis Complex_setsum')
   1.141  
   1.142 -lemma cnj_setsum: "cnj (setsum f s) = setsum (%x. cnj (f x)) s"
   1.143 -apply (cases "finite s")
   1.144 -  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
   1.145 -
   1.146  lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
   1.147 -apply (cases "finite s")
   1.148 -  by (induct s rule: finite_induct) auto
   1.149 +  by (induct s rule: infinite_finite_induct) auto
   1.150  
   1.151  lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
   1.152 -apply (cases "finite s")
   1.153 -  by (induct s rule: finite_induct) auto
   1.154 +  by (induct s rule: infinite_finite_induct) auto
   1.155  
   1.156  lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
   1.157  by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj 
   1.158 @@ -677,6 +744,27 @@
   1.159  lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
   1.160    by (metis Re_complex_of_real Reals_cases norm_of_real)
   1.161  
   1.162 +lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   1.163 +  by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
   1.164 +
   1.165 +lemma series_comparison_complex:
   1.166 +  fixes f:: "nat \<Rightarrow> 'a::banach"
   1.167 +  assumes sg: "summable g"
   1.168 +     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
   1.169 +     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
   1.170 +  shows "summable f"
   1.171 +proof -
   1.172 +  have g: "\<And>n. cmod (g n) = Re (g n)" using assms
   1.173 +    by (metis abs_of_nonneg in_Reals_norm)
   1.174 +  show ?thesis
   1.175 +    apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
   1.176 +    using sg
   1.177 +    apply (auto simp: summable_def)
   1.178 +    apply (rule_tac x="Re s" in exI)
   1.179 +    apply (auto simp: g sums_Re)
   1.180 +    apply (metis fg g)
   1.181 +    done
   1.182 +qed
   1.183  
   1.184  subsection{*Finally! Polar Form for Complex Numbers*}
   1.185  
   1.186 @@ -888,4 +976,5 @@
   1.187  lemmas complex_Re_Im_cancel_iff = complex_eq_iff
   1.188  lemmas complex_equality = complex_eqI
   1.189  
   1.190 +
   1.191  end