337 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
337 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
338 by (cases x) simp |
338 by (cases x) simp |
339 |
339 |
340 subsection {* Completeness of the Complexes *} |
340 subsection {* Completeness of the Complexes *} |
341 |
341 |
342 interpretation Re: bounded_linear "Re" |
342 lemma bounded_linear_Re: "bounded_linear Re" |
343 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
343 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
344 |
344 |
345 interpretation Im: bounded_linear "Im" |
345 lemma bounded_linear_Im: "bounded_linear Im" |
346 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
346 by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) |
|
347 |
|
348 lemmas tendsto_Re [tendsto_intros] = |
|
349 bounded_linear.tendsto [OF bounded_linear_Re] |
|
350 |
|
351 lemmas tendsto_Im [tendsto_intros] = |
|
352 bounded_linear.tendsto [OF bounded_linear_Im] |
|
353 |
|
354 lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re] |
|
355 lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im] |
|
356 lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re] |
|
357 lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im] |
347 |
358 |
348 lemma tendsto_Complex [tendsto_intros]: |
359 lemma tendsto_Complex [tendsto_intros]: |
349 assumes "(f ---> a) net" and "(g ---> b) net" |
360 assumes "(f ---> a) net" and "(g ---> b) net" |
350 shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net" |
361 shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) net" |
351 proof (rule tendstoI) |
362 proof (rule tendstoI) |
368 |
379 |
369 instance complex :: banach |
380 instance complex :: banach |
370 proof |
381 proof |
371 fix X :: "nat \<Rightarrow> complex" |
382 fix X :: "nat \<Rightarrow> complex" |
372 assume X: "Cauchy X" |
383 assume X: "Cauchy X" |
373 from Re.Cauchy [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))" |
384 from Cauchy_Re [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))" |
374 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
385 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
375 from Im.Cauchy [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))" |
386 from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))" |
376 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
387 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
377 have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))" |
388 have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))" |
378 using LIMSEQ_Complex [OF 1 2] by simp |
389 using LIMSEQ_Complex [OF 1 2] by simp |
379 thus "convergent X" |
390 thus "convergent X" |
380 by (rule convergentI) |
391 by (rule convergentI) |
509 by (simp add: complex_eq_iff power2_eq_square) |
520 by (simp add: complex_eq_iff power2_eq_square) |
510 |
521 |
511 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" |
522 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" |
512 by (simp add: norm_mult power2_eq_square) |
523 by (simp add: norm_mult power2_eq_square) |
513 |
524 |
514 interpretation cnj: bounded_linear "cnj" |
525 lemma bounded_linear_cnj: "bounded_linear cnj" |
515 using complex_cnj_add complex_cnj_scaleR |
526 using complex_cnj_add complex_cnj_scaleR |
516 by (rule bounded_linear_intro [where K=1], simp) |
527 by (rule bounded_linear_intro [where K=1], simp) |
|
528 |
|
529 lemmas tendsto_cnj [tendsto_intros] = |
|
530 bounded_linear.tendsto [OF bounded_linear_cnj] |
|
531 |
|
532 lemmas isCont_cnj [simp] = |
|
533 bounded_linear.isCont [OF bounded_linear_cnj] |
517 |
534 |
518 |
535 |
519 subsection{*The Functions @{term sgn} and @{term arg}*} |
536 subsection{*The Functions @{term sgn} and @{term arg}*} |
520 |
537 |
521 text {*------------ Argand -------------*} |
538 text {*------------ Argand -------------*} |