--- a/src/HOL/Complex.thy Mon Jun 16 16:21:52 2014 +0200
+++ b/src/HOL/Complex.thy Mon Jun 16 17:52:33 2014 +0200
@@ -168,6 +168,15 @@
"Re ii = 0"
| "Im ii = 1"
+lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
+ by (simp add: complex_eq_iff)
+
+lemma complex_eq: "a = Re a + \<i> * Im a"
+ by (simp add: complex_eq_iff)
+
+lemma fun_complex_eq: "f = (\<lambda>x. Re (f x) + \<i> * Im (f x))"
+ by (simp add: fun_eq_iff complex_eq)
+
lemma i_squared [simp]: "ii * ii = -1"
by (simp add: complex_eq_iff)
@@ -183,9 +192,6 @@
lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
by (simp add: mult_assoc [symmetric])
-lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
- by (simp add: complex_eq_iff)
-
lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
by (simp add: complex_eq_iff)
@@ -259,6 +265,13 @@
lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
by (simp add: norm_complex_def)
+lemma cmod_le: "cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>"
+ apply (subst complex_eq)
+ apply (rule order_trans)
+ apply (rule norm_triangle_ineq)
+ apply (simp add: norm_mult)
+ done
+
lemma cmod_eq_Re: "Im z = 0 \<Longrightarrow> cmod z = \<bar>Re z\<bar>"
by (simp add: norm_complex_def)
@@ -336,6 +349,24 @@
unfolding complex.collapse .
qed (auto intro: tendsto_intros)
+lemma continuous_complex_iff: "continuous F f \<longleftrightarrow>
+ continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
+ unfolding continuous_def tendsto_complex_iff ..
+
+lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
+ ((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
+ ((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
+ unfolding has_vector_derivative_def has_field_derivative_def has_derivative_def tendsto_complex_iff
+ by (simp add: field_simps bounded_linear_scaleR_left bounded_linear_mult_right)
+
+lemma has_field_derivative_Re[derivative_intros]:
+ "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F"
+ unfolding has_vector_derivative_complex_iff by safe
+
+lemma has_field_derivative_Im[derivative_intros]:
+ "(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Im (f x)) has_field_derivative (Im D)) F"
+ unfolding has_vector_derivative_complex_iff by safe
+
instance complex :: banach
proof
fix X :: "nat \<Rightarrow> complex"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jun 16 16:21:52 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Jun 16 17:52:33 2014 +0200
@@ -1932,7 +1932,7 @@
lemma has_vector_derivative_id[simp, derivative_intros]: "((\<lambda>x. x) has_vector_derivative 1) net"
by (auto simp: has_vector_derivative_def)
-lemma has_vector_derivative_neg[derivative_intros]:
+lemma has_vector_derivative_minus[derivative_intros]:
"(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. - f x) has_vector_derivative (- f')) net"
by (auto simp: has_vector_derivative_def)
@@ -1941,14 +1941,19 @@
((\<lambda>x. f x + g x) has_vector_derivative (f' + g')) net"
by (auto simp: has_vector_derivative_def scaleR_right_distrib)
-lemma has_vector_derivative_sub[derivative_intros]:
+lemma has_vector_derivative_setsum[derivative_intros]:
+ "(\<And>i. i \<in> I \<Longrightarrow> (f i has_vector_derivative f' i) net) \<Longrightarrow>
+ ((\<lambda>x. \<Sum>i\<in>I. f i x) has_vector_derivative (\<Sum>i\<in>I. f' i)) net"
+ by (auto simp: has_vector_derivative_def fun_eq_iff scaleR_setsum_right intro!: derivative_eq_intros)
+
+lemma has_vector_derivative_diff[derivative_intros]:
"(f has_vector_derivative f') net \<Longrightarrow> (g has_vector_derivative g') net \<Longrightarrow>
((\<lambda>x. f x - g x) has_vector_derivative (f' - g')) net"
by (auto simp: has_vector_derivative_def scaleR_diff_right)
lemma (in bounded_linear) has_vector_derivative:
- assumes "(g has_vector_derivative g') (at x within s)"
- shows "((\<lambda>x. f (g x)) has_vector_derivative f g') (at x within s)"
+ assumes "(g has_vector_derivative g') F"
+ shows "((\<lambda>x. f (g x)) has_vector_derivative f g') F"
using has_derivative[OF assms[unfolded has_vector_derivative_def]]
by (simp add: has_vector_derivative_def scaleR)
@@ -1970,6 +1975,24 @@
((\<lambda>x. f x * g x) has_vector_derivative (f x * g' + f' * g x :: 'a :: real_normed_algebra)) (at x within s)"
by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_mult])
+lemma has_vector_derivative_of_real[derivative_intros]:
+ "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
+ by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
+ (simp add: has_field_derivative_iff_has_vector_derivative)
+
+lemma has_vector_derivative_continuous: "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
+ by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
+
+lemma has_vector_derivative_mult_right[derivative_intros]:
+ fixes a :: "'a :: real_normed_algebra"
+ shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F"
+ by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_right])
+
+lemma has_vector_derivative_mult_left[derivative_intros]:
+ fixes a :: "'a :: real_normed_algebra"
+ shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. f x * a) has_vector_derivative (x * a)) F"
+ by (rule bounded_linear.has_vector_derivative[OF bounded_linear_mult_left])
+
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
lemma vector_derivative_unique_at:
--- a/src/HOL/Probability/Borel_Space.thy Mon Jun 16 16:21:52 2014 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Mon Jun 16 17:52:33 2014 +0200
@@ -921,6 +921,15 @@
lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
by (intro borel_measurable_continuous_on1 continuous_intros)
+lemma borel_measurable_complex_iff:
+ "f \<in> borel_measurable M \<longleftrightarrow>
+ (\<lambda>x. Re (f x)) \<in> borel_measurable M \<and> (\<lambda>x. Im (f x)) \<in> borel_measurable M"
+ apply auto
+ apply (subst fun_complex_eq)
+ apply (intro borel_measurable_add)
+ apply auto
+ done
+
subsection "Borel space on the extended reals"
lemma borel_measurable_ereal[measurable (raw)]: