# HG changeset patch # User paulson # Date 1393345040 0 # Node ID 3f5b2745d65909eba25b512127b9b9b47be45c76 # Parent e6edd47f14831af58d0f801c18d791f8563a0155 More complex-related lemmas diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue Feb 25 15:02:54 2014 +0100 +++ b/src/HOL/Complex.thy Tue Feb 25 16:17:20 2014 +0000 @@ -557,6 +557,109 @@ bounded_linear.isCont [OF bounded_linear_cnj] +subsection{*Basic Lemmas*} + +lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0" + by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff) + +lemma complex_neq_0: "z\0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0" +by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff) + +lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z" +apply (cases z, auto) +by (metis complex_of_real_def of_real_add of_real_power power2_eq_square) + +lemma complex_div_eq_0: + "(Re(a / b) = 0 \ Re(a * cnj b) = 0) & (Im(a / b) = 0 \ Im(a * cnj b) = 0)" +proof (cases "b=0") + case True then show ?thesis by auto +next + case False + show ?thesis + proof (cases b) + case (Complex x y) + then have "x\<^sup>2 + y\<^sup>2 > 0" + by (metis Complex_eq_0 False sum_power2_gt_zero_iff) + then have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)" + by (metis add_divide_distrib) + with Complex False show ?thesis + by (auto simp: complex_divide_def) + qed +qed + +lemma re_complex_div_eq_0: "Re(a / b) = 0 \ Re(a * cnj b) = 0" + and im_complex_div_eq_0: "Im(a / b) = 0 \ Im(a * cnj b) = 0" +using complex_div_eq_0 by auto + + +lemma complex_div_gt_0: + "(Re(a / b) > 0 \ Re(a * cnj b) > 0) & (Im(a / b) > 0 \ Im(a * cnj b) > 0)" +proof (cases "b=0") + case True then show ?thesis by auto +next + case False + show ?thesis + proof (cases b) + case (Complex x y) + then have "x\<^sup>2 + y\<^sup>2 > 0" + by (metis Complex_eq_0 False sum_power2_gt_zero_iff) + moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)" + by (metis add_divide_distrib) + ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2` + apply (simp add: complex_divide_def zero_less_divide_iff less_divide_eq) + apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left) + done + qed +qed + +lemma re_complex_div_gt_0: "Re(a / b) > 0 \ Re(a * cnj b) > 0" + and im_complex_div_gt_0: "Im(a / b) > 0 \ Im(a * cnj b) > 0" +using complex_div_gt_0 by auto + +lemma re_complex_div_ge_0: "Re(a / b) \ 0 \ Re(a * cnj b) \ 0" + by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0) + +lemma im_complex_div_ge_0: "Im(a / b) \ 0 \ Im(a * cnj b) \ 0" + by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less) + +lemma re_complex_div_lt_0: "Re(a / b) < 0 \ Re(a * cnj b) < 0" + by (smt re_complex_div_eq_0 re_complex_div_gt_0) + +lemma im_complex_div_lt_0: "Im(a / b) < 0 \ Im(a * cnj b) < 0" + by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff) + +lemma re_complex_div_le_0: "Re(a / b) \ 0 \ Re(a * cnj b) \ 0" + by (metis not_le re_complex_div_gt_0) + +lemma im_complex_div_le_0: "Im(a / b) \ 0 \ Im(a * cnj b) \ 0" + by (metis im_complex_div_gt_0 not_le) + +lemma Re_setsum: "finite s \ Re(setsum f s) = setsum (%x. Re(f x)) s" + by (induct s rule: finite_induct) auto + +lemma Im_setsum: "finite s \ Im(setsum f s) = setsum (%x. Im(f x)) s" + by (induct s rule: finite_induct) auto + +lemma Complex_setsum': "finite s \ setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0" + by (induct s rule: finite_induct) auto + +lemma Complex_setsum: "finite s \ Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s" + by (metis Complex_setsum') + +lemma cnj_setsum: "finite s \ cnj (setsum f s) = setsum (%x. cnj (f x)) s" + by (induct s rule: finite_induct) (auto simp: complex_cnj_add) + +lemma Reals_cnj_iff: "z \ \ \ cnj z = z" +by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj + complex_of_real_def equal_neg_zero) + +lemma Complex_in_Reals: "Complex x 0 \ \" + by (metis Reals_of_real complex_of_real_def) + +lemma in_Reals_norm: "z \ \ \ norm(z) = abs(Re z)" + by (metis Re_complex_of_real Reals_cases norm_of_real) + + subsection{*Finally! Polar Form for Complex Numbers*} subsubsection {* $\cos \theta + i \sin \theta$ *} diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Feb 25 15:02:54 2014 +0100 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Feb 25 16:17:20 2014 +0000 @@ -7,6 +7,7 @@ begin subsection {* Square root of complex numbers *} + definition csqrt :: "complex \ complex" where "csqrt z = (if Im z = 0 then if 0 \ Re z then Complex (sqrt(Re z)) 0 @@ -54,6 +55,39 @@ ultimately show ?thesis by blast qed +lemma csqrt_Complex: "x \ 0 \ csqrt (Complex x 0) = Complex (sqrt x) 0" + by (simp add: csqrt_def) + +lemma csqrt_0 [simp]: "csqrt 0 = 0" + by (simp add: csqrt_def) + +lemma csqrt_1 [simp]: "csqrt 1 = 1" + by (simp add: csqrt_def) + +lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \ Im(csqrt(z))" +proof (cases z) + case (Complex x y) + then show ?thesis + using real_sqrt_sum_squares_ge1 [of "x" y] + real_sqrt_sum_squares_ge1 [of "-x" y] + real_sqrt_sum_squares_eq_cancel [of x y] + apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le) + apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1) + by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel) +qed + +lemma Re_csqrt: "0 \ Re(csqrt z)" + by (metis csqrt_principal le_less) + +lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \ Im z) \ csqrt (z^2) = z" + using csqrt [of "z^2"] csqrt_principal [of "z^2"] + by (cases z) (auto simp: power2_eq_iff) + +lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0" + by auto (metis csqrt power_eq_0_iff) + +lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1" + by auto (metis csqrt power2_eq_1_iff) subsection{* More lemmas about module of complex numbers *} diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Topological_Spaces.thy --- a/src/HOL/Topological_Spaces.thy Tue Feb 25 15:02:54 2014 +0100 +++ b/src/HOL/Topological_Spaces.thy Tue Feb 25 16:17:20 2014 +0000 @@ -1706,6 +1706,11 @@ unfolding continuous_on_open_invariant by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s]) +corollary continuous_imp_open_vimage: + assumes "continuous_on s f" "open s" "open B" "f -` B \ s" + shows "open (f -` B)" +by (metis assms continuous_on_open_vimage le_iff_inf) + lemma continuous_on_closed_invariant: "continuous_on s f \ (\B. closed B \ (\A. closed A \ A \ s = f -` B \ s))" proof - diff -r e6edd47f1483 -r 3f5b2745d659 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Feb 25 15:02:54 2014 +0100 +++ b/src/HOL/Transcendental.thy Tue Feb 25 16:17:20 2014 +0000 @@ -52,6 +52,12 @@ finally show ?case . qed +corollary power_diff_sumr2: --{*COMPLEX_POLYFUN in HOL Light*} + fixes x :: "'a::{comm_ring,monoid_mult}" + shows "x^n - y^n = (x - y) * (\i=0..p=0..p=0..