add more derivative and continuity rules for complex-values functions
authorhoelzl
Mon Jun 16 17:52:33 2014 +0200 (2014-06-16)
changeset 572593a448982a74a
parent 57258 67d85a8aa6cc
child 57260 8747af0d1012
add more derivative and continuity rules for complex-values functions
src/HOL/Complex.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Probability/Borel_Space.thy
     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"
     2.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jun 16 16:21:52 2014 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Jun 16 17:52:33 2014 +0200
     2.3 @@ -1932,7 +1932,7 @@
     2.4  lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net"
     2.5    by (auto simp: has_vector_derivative_def)
     2.6  
     2.7 -lemma has_vector_derivative_neg[derivative_intros]:
     2.8 +lemma has_vector_derivative_minus[derivative_intros]:
     2.9    "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
    2.10    by (auto simp: has_vector_derivative_def)
    2.11  
    2.12 @@ -1941,14 +1941,19 @@
    2.13      ((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
    2.14    by (auto simp: has_vector_derivative_def scaleR_right_distrib)
    2.15  
    2.16 -lemma has_vector_derivative_sub[derivative_intros]:
    2.17 +lemma has_vector_derivative_setsum[derivative_intros]:
    2.18 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i has_vector_derivative f' i) net) \<Longrightarrow>
    2.19 +    ((\<lambda>x. \<Sum>i\<in>I. f i x) has_vector_derivative (\<Sum>i\<in>I. f' i)) net"
    2.20 +  by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_setsum_right intro!: derivative_eq_intros)
    2.21 +
    2.22 +lemma has_vector_derivative_diff[derivative_intros]:
    2.23    "(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
    2.24      ((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
    2.25    by (auto simp: has_vector_derivative_def scaleR_diff_right)
    2.26  
    2.27  lemma (in bounded_linear) has_vector_derivative:
    2.28 -  assumes "(g has_vector_derivative g') (at x within s)"
    2.29 -  shows "((\<lambda>x. f (g x)) has_vector_derivative f g') (at x within s)"
    2.30 +  assumes "(g has_vector_derivative g') F"
    2.31 +  shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F"
    2.32    using has_derivative[OF assms[unfolded has_vector_derivative_def]]
    2.33    by (simp add: has_vector_derivative_def scaleR)
    2.34  
    2.35 @@ -1970,6 +1975,24 @@
    2.36      ((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)"
    2.37    by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])
    2.38  
    2.39 +lemma has_vector_derivative_of_real[derivative_intros]:
    2.40 +  "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
    2.41 +  by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
    2.42 +     (simp add: has_field_derivative_iff_has_vector_derivative)
    2.43 +
    2.44 +lemma has_vector_derivative_continuous: "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
    2.45 +  by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
    2.46 +
    2.47 +lemma has_vector_derivative_mult_right[derivative_intros]:
    2.48 +  fixes a :: "'a :: real_normed_algebra"
    2.49 +  shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F"
    2.50 +  by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right])
    2.51 +
    2.52 +lemma has_vector_derivative_mult_left[derivative_intros]:
    2.53 +  fixes a :: "'a :: real_normed_algebra"
    2.54 +  shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F"
    2.55 +  by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])
    2.56 +
    2.57  definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
    2.58  
    2.59  lemma vector_derivative_unique_at:
     3.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon Jun 16 16:21:52 2014 +0200
     3.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Jun 16 17:52:33 2014 +0200
     3.3 @@ -921,6 +921,15 @@
     3.4  lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
     3.5    by (intro borel_measurable_continuous_on1 continuous_intros)
     3.6  
     3.7 +lemma borel_measurable_complex_iff:
     3.8 +  "f \<in> borel_measurable M \<longleftrightarrow>
     3.9 +    (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M"
    3.10 +  apply auto
    3.11 +  apply (subst fun_complex_eq)
    3.12 +  apply (intro borel_measurable_add)
    3.13 +  apply auto
    3.14 +  done
    3.15 +
    3.16  subsection "Borel space on the extended reals"
    3.17  
    3.18  lemma borel_measurable_ereal[measurable (raw)]: