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
```