equal
deleted
inserted
replaced
333 by (cases x) simp |
333 by (cases x) simp |
334 |
334 |
335 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
335 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
336 by (cases x) simp |
336 by (cases x) simp |
337 |
337 |
|
338 text {* Properties of complex signum. *} |
|
339 |
|
340 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" |
|
341 by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute) |
|
342 |
|
343 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" |
|
344 by (simp add: complex_sgn_def divide_inverse) |
|
345 |
|
346 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" |
|
347 by (simp add: complex_sgn_def divide_inverse) |
|
348 |
338 |
349 |
339 subsection {* Completeness of the Complexes *} |
350 subsection {* Completeness of the Complexes *} |
340 |
351 |
341 lemma bounded_linear_Re: "bounded_linear Re" |
352 lemma bounded_linear_Re: "bounded_linear Re" |
342 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
353 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
533 |
544 |
534 lemmas isCont_cnj [simp] = |
545 lemmas isCont_cnj [simp] = |
535 bounded_linear.isCont [OF bounded_linear_cnj] |
546 bounded_linear.isCont [OF bounded_linear_cnj] |
536 |
547 |
537 |
548 |
538 subsection {* Complex Signum and Argument *} |
549 subsection {* Complex Argument *} |
539 |
550 |
540 definition arg :: "complex => real" where |
551 definition arg :: "complex => real" where |
541 "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)" |
552 "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)" |
542 |
|
543 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" |
|
544 by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute) |
|
545 |
|
546 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" |
|
547 by (simp add: complex_sgn_def divide_inverse) |
|
548 |
|
549 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" |
|
550 by (simp add: complex_sgn_def divide_inverse) |
|
551 |
553 |
552 (*----------------------------------------------------------------------------*) |
554 (*----------------------------------------------------------------------------*) |
553 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) |
555 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) |
554 (* many of the theorems are not used - so should they be kept? *) |
556 (* many of the theorems are not used - so should they be kept? *) |
555 (*----------------------------------------------------------------------------*) |
557 (*----------------------------------------------------------------------------*) |