54 "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)" |
54 "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)" |
55 |
55 |
56 |
56 |
57 subsection {* Bounded Sequences *} |
57 subsection {* Bounded Sequences *} |
58 |
58 |
59 lemma BseqI: assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
59 lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X" |
60 unfolding Bseq_def |
60 unfolding Bseq_def |
61 proof (intro exI conjI allI) |
61 proof (intro exI conjI allI) |
62 show "0 < max K 1" by simp |
62 show "0 < max K 1" by simp |
63 next |
63 next |
64 fix n::nat |
64 fix n::nat |
65 have "norm (X n) \<le> K" by (rule K) |
65 have "norm (X n) \<le> K" by (rule K) |
66 thus "norm (X n) \<le> max K 1" by simp |
66 thus "norm (X n) \<le> max K 1" by simp |
67 qed |
67 qed |
68 |
68 |
69 lemma BseqD: "Bseq X \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K" |
|
70 unfolding Bseq_def by simp |
|
71 |
|
72 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
69 lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
73 unfolding Bseq_def by auto |
70 unfolding Bseq_def by auto |
74 |
71 |
75 lemma BseqI2: assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
72 lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
76 proof (rule BseqI) |
73 proof (rule BseqI') |
77 let ?A = "norm ` X ` {..N}" |
74 let ?A = "norm ` X ` {..N}" |
78 have 1: "finite ?A" by simp |
75 have 1: "finite ?A" by simp |
79 have 2: "?A \<noteq> {}" by auto |
76 have 2: "?A \<noteq> {}" by auto |
80 fix n::nat |
77 fix n::nat |
81 show "norm (X n) \<le> max K (Max ?A)" |
78 show "norm (X n) \<le> max K (Max ?A)" |
94 lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
91 lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
95 unfolding Bseq_def by auto |
92 unfolding Bseq_def by auto |
96 |
93 |
97 lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
94 lemma Bseq_offset: "Bseq (\<lambda>n. X (n + k)) \<Longrightarrow> Bseq X" |
98 apply (erule BseqE) |
95 apply (erule BseqE) |
99 apply (rule_tac N="k" and K="K" in BseqI2) |
96 apply (rule_tac N="k" and K="K" in BseqI2') |
100 apply clarify |
97 apply clarify |
101 apply (drule_tac x="n - k" in spec, simp) |
98 apply (drule_tac x="n - k" in spec, simp) |
102 done |
99 done |
103 |
100 |
104 |
101 |
411 hence "\<exists>r>0. r < norm a" by (rule dense) |
408 hence "\<exists>r>0. r < norm a" by (rule dense) |
412 then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
409 then obtain r where r1: "0 < r" and r2: "r < norm a" by fast |
413 obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r" |
410 obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (X n - a) < r" |
414 using LIMSEQ_D [OF X r1] by fast |
411 using LIMSEQ_D [OF X r1] by fast |
415 show ?thesis |
412 show ?thesis |
416 proof (rule BseqI2 [rule_format]) |
413 proof (rule BseqI2' [rule_format]) |
417 fix n assume n: "N \<le> n" |
414 fix n assume n: "N \<le> n" |
418 hence 1: "norm (X n - a) < r" by (rule N) |
415 hence 1: "norm (X n - a) < r" by (rule N) |
419 hence 2: "X n \<noteq> 0" using r2 by auto |
416 hence 2: "X n \<noteq> 0" using r2 by auto |
420 hence "norm (inverse (X n)) = inverse (norm (X n))" |
417 hence "norm (inverse (X n)) = inverse (norm (X n))" |
421 by (rule nonzero_norm_inverse) |
418 by (rule nonzero_norm_inverse) |