src/HOL/Complex.thy
 changeset 57259 3a448982a74a parent 56889 48a745e1bde7 child 57512 cc97b347b301
```     1.1 --- a/src/HOL/Complex.thy	Mon Jun 16 16:21:52 2014 +0200
1.2 +++ b/src/HOL/Complex.thy	Mon Jun 16 17:52:33 2014 +0200
1.3 @@ -168,6 +168,15 @@
1.4    "Re ii = 0"
1.5  | "Im ii = 1"
1.6
1.7 +lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
1.8 +  by (simp add: complex_eq_iff)
1.9 +
1.10 +lemma complex_eq: "a = Re a + \<i> * Im a"
1.11 +  by (simp add: complex_eq_iff)
1.12 +
1.13 +lemma fun_complex_eq: "f = (\<lambda>x. Re (f x) + \<i> * Im (f x))"
1.14 +  by (simp add: fun_eq_iff complex_eq)
1.15 +
1.16  lemma i_squared [simp]: "ii * ii = -1"
1.18
1.19 @@ -183,9 +192,6 @@
1.20  lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
1.21    by (simp add: mult_assoc [symmetric])
1.22
1.23 -lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
1.24 -  by (simp add: complex_eq_iff)
1.25 -
1.26  lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
1.28
1.29 @@ -259,6 +265,13 @@
1.30  lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
1.32
1.33 +lemma cmod_le: "cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>"
1.34 +  apply (subst complex_eq)
1.35 +  apply (rule order_trans)
1.36 +  apply (rule norm_triangle_ineq)
1.37 +  apply (simp add: norm_mult)
1.38 +  done
1.39 +
1.40  lemma cmod_eq_Re: "Im z = 0 \<Longrightarrow> cmod z = \<bar>Re z\<bar>"
1.42
1.43 @@ -336,6 +349,24 @@
1.44      unfolding complex.collapse .
1.45  qed (auto intro: tendsto_intros)
1.46
1.47 +lemma continuous_complex_iff: "continuous F f \<longleftrightarrow>
1.48 +    continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
1.49 +  unfolding continuous_def tendsto_complex_iff ..
1.50 +
1.51 +lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
1.52 +    ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
1.53 +    ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
1.54 +  unfolding has_vector_derivative_def has_field_derivative_def has_derivative_def tendsto_complex_iff
1.55 +  by (simp add: field_simps bounded_linear_scaleR_left bounded_linear_mult_right)
1.56 +
1.57 +lemma has_field_derivative_Re[derivative_intros]:
1.58 +  "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F"
1.59 +  unfolding has_vector_derivative_complex_iff by safe
1.60 +
1.61 +lemma has_field_derivative_Im[derivative_intros]:
1.62 +  "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_field_derivative (Im D)) F"
1.63 +  unfolding has_vector_derivative_complex_iff by safe
1.64 +
1.65  instance complex :: banach
1.66  proof
1.67    fix X :: "nat \<Rightarrow> complex"
```