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.17    by (simp add: complex_eq_iff)
    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.27    by (simp add: complex_eq_iff)
    1.28  
    1.29 @@ -259,6 +265,13 @@
    1.30  lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
    1.31    by (simp add: norm_complex_def)
    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.41    by (simp add: norm_complex_def)
    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"