equal
deleted
inserted
replaced
336 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a" |
336 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a" |
337 by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) |
337 by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) |
338 |
338 |
339 lemmas real_sum_squared_expand = power2_sum [where 'a=real] |
339 lemmas real_sum_squared_expand = power2_sum [where 'a=real] |
340 |
340 |
|
341 lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x" |
|
342 by (cases x) simp |
|
343 |
|
344 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
|
345 by (cases x) simp |
341 |
346 |
342 subsection {* Completeness of the Complexes *} |
347 subsection {* Completeness of the Complexes *} |
343 |
348 |
344 interpretation Re: bounded_linear ["Re"] |
349 interpretation Re: bounded_linear ["Re"] |
345 apply (unfold_locales, simp, simp) |
350 apply (unfold_locales, simp, simp) |