# HG changeset patch # User hoelzl # Date 1402933953 -7200 # Node ID 3a448982a74a0547c56787e4bcbc0da0daa54a58 # Parent 67d85a8aa6cc1a276bc6e6eeb9420060ace839cd add more derivative and continuity rules for complex-values functions diff -r 67d85a8aa6cc -r 3a448982a74a src/HOL/Complex.thy --- 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 + \ * b" + by (simp add: complex_eq_iff) + +lemma complex_eq: "a = Re a + \ * Im a" + by (simp add: complex_eq_iff) + +lemma fun_complex_eq: "f = (\x. Re (f x) + \ * 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 + \ * b" - by (simp add: complex_eq_iff) - lemma complex_i_not_zero [simp]: "ii \ 0" by (simp add: complex_eq_iff) @@ -259,6 +265,13 @@ lemma abs_Im_le_cmod: "\Im x\ \ cmod x" by (simp add: norm_complex_def) +lemma cmod_le: "cmod z \ \Re z\ + \Im z\" + 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 \ cmod z = \Re z\" 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 \ + continuous F (\x. Re (f x)) \ continuous F (\x. Im (f x))" + unfolding continuous_def tendsto_complex_iff .. + +lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \ + ((\x. Re (f x)) has_field_derivative (Re x)) F \ + ((\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 \ ((\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 \ ((\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 \ complex" diff -r 67d85a8aa6cc -r 3a448982a74a src/HOL/Multivariate_Analysis/Derivative.thy --- 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]: "((\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 \ ((\x. - f x) has_vector_derivative (- f')) net" by (auto simp: has_vector_derivative_def) @@ -1941,14 +1941,19 @@ ((\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]: + "(\i. i \ I \ (f i has_vector_derivative f' i) net) \ + ((\x. \i\I. f i x) has_vector_derivative (\i\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 \ (g has_vector_derivative g') net \ ((\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 "((\x. f (g x)) has_vector_derivative f g') (at x within s)" + assumes "(g has_vector_derivative g') F" + shows "((\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 @@ ((\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 \ ((\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) \ 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 \ ((\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 \ ((\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: diff -r 67d85a8aa6cc -r 3a448982a74a src/HOL/Probability/Borel_Space.thy --- 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 \ borel_measurable borel" by (intro borel_measurable_continuous_on1 continuous_intros) +lemma borel_measurable_complex_iff: + "f \ borel_measurable M \ + (\x. Re (f x)) \ borel_measurable M \ (\x. Im (f x)) \ 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)]: