author hoelzl Mon Jun 16 17:52:33 2014 +0200 (2014-06-16) changeset 57259 3a448982a74a parent 57258 67d85a8aa6cc child 57260 8747af0d1012
add more derivative and continuity rules for complex-values functions
 src/HOL/Complex.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Derivative.thy file | annotate | diff | revisions src/HOL/Probability/Borel_Space.thy file | annotate | diff | revisions
```     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)]:
```