src/HOL/SEQ.thy
 author chaieb Mon Mar 02 12:33:12 2009 +0000 (2009-03-02) changeset 30196 6ffaa79c352c parent 30082 43c5b7bfc791 child 30242 aea5d7fa7ef5 permissions -rw-r--r--
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
 paulson@10751 ` 1` ```(* Title : SEQ.thy ``` paulson@10751 ` 2` ``` Author : Jacques D. Fleuriot ``` paulson@10751 ` 3` ``` Copyright : 1998 University of Cambridge ``` paulson@10751 ` 4` ``` Description : Convergence of sequences and series ``` paulson@15082 ` 5` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` huffman@22608 ` 6` ``` Additional contributions by Jeremy Avigad and Brian Huffman ``` paulson@15082 ` 7` ```*) ``` paulson@10751 ` 8` huffman@22631 ` 9` ```header {* Sequences and Convergence *} ``` huffman@17439 ` 10` nipkow@15131 ` 11` ```theory SEQ ``` haftmann@29197 ` 12` ```imports RealVector RComplete ``` nipkow@15131 ` 13` ```begin ``` paulson@10751 ` 14` wenzelm@19765 ` 15` ```definition ``` huffman@22608 ` 16` ``` Zseq :: "[nat \ 'a::real_normed_vector] \ bool" where ``` huffman@22608 ` 17` ``` --{*Standard definition of sequence converging to zero*} ``` haftmann@28562 ` 18` ``` [code del]: "Zseq X = (\r>0. \no. \n\no. norm (X n) < r)" ``` huffman@22608 ` 19` huffman@22608 ` 20` ```definition ``` huffman@20552 ` 21` ``` LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool" ``` wenzelm@21404 ` 22` ``` ("((_)/ ----> (_))" [60, 60] 60) where ``` paulson@15082 ` 23` ``` --{*Standard definition of convergence of sequence*} ``` haftmann@28562 ` 24` ``` [code del]: "X ----> L = (\r. 0 < r --> (\no. \n. no \ n --> norm (X n - L) < r))" ``` paulson@10751 ` 25` wenzelm@21404 ` 26` ```definition ``` wenzelm@21404 ` 27` ``` lim :: "(nat => 'a::real_normed_vector) => 'a" where ``` paulson@15082 ` 28` ``` --{*Standard definition of limit using choice operator*} ``` huffman@20682 ` 29` ``` "lim X = (THE L. X ----> L)" ``` paulson@10751 ` 30` wenzelm@21404 ` 31` ```definition ``` wenzelm@21404 ` 32` ``` convergent :: "(nat => 'a::real_normed_vector) => bool" where ``` paulson@15082 ` 33` ``` --{*Standard definition of convergence*} ``` huffman@20682 ` 34` ``` "convergent X = (\L. X ----> L)" ``` paulson@10751 ` 35` wenzelm@21404 ` 36` ```definition ``` wenzelm@21404 ` 37` ``` Bseq :: "(nat => 'a::real_normed_vector) => bool" where ``` paulson@15082 ` 38` ``` --{*Standard definition for bounded sequence*} ``` haftmann@28562 ` 39` ``` [code del]: "Bseq X = (\K>0.\n. norm (X n) \ K)" ``` paulson@10751 ` 40` wenzelm@21404 ` 41` ```definition ``` wenzelm@21404 ` 42` ``` monoseq :: "(nat=>real)=>bool" where ``` paulson@15082 ` 43` ``` --{*Definition for monotonicity*} ``` haftmann@28562 ` 44` ``` [code del]: "monoseq X = ((\m. \n\m. X m \ X n) | (\m. \n\m. X n \ X m))" ``` paulson@10751 ` 45` wenzelm@21404 ` 46` ```definition ``` wenzelm@21404 ` 47` ``` subseq :: "(nat => nat) => bool" where ``` paulson@15082 ` 48` ``` --{*Definition of subsequence*} ``` haftmann@28562 ` 49` ``` [code del]: "subseq f = (\m. \n>m. (f m) < (f n))" ``` paulson@10751 ` 50` wenzelm@21404 ` 51` ```definition ``` wenzelm@21404 ` 52` ``` Cauchy :: "(nat => 'a::real_normed_vector) => bool" where ``` paulson@15082 ` 53` ``` --{*Standard definition of the Cauchy condition*} ``` haftmann@28562 ` 54` ``` [code del]: "Cauchy X = (\e>0. \M. \m \ M. \n \ M. norm (X m - X n) < e)" ``` paulson@10751 ` 55` paulson@15082 ` 56` huffman@22608 ` 57` ```subsection {* Bounded Sequences *} ``` huffman@22608 ` 58` wenzelm@26312 ` 59` ```lemma BseqI': assumes K: "\n. norm (X n) \ K" shows "Bseq X" ``` huffman@22608 ` 60` ```unfolding Bseq_def ``` huffman@22608 ` 61` ```proof (intro exI conjI allI) ``` huffman@22608 ` 62` ``` show "0 < max K 1" by simp ``` huffman@22608 ` 63` ```next ``` huffman@22608 ` 64` ``` fix n::nat ``` huffman@22608 ` 65` ``` have "norm (X n) \ K" by (rule K) ``` huffman@22608 ` 66` ``` thus "norm (X n) \ max K 1" by simp ``` huffman@22608 ` 67` ```qed ``` huffman@22608 ` 68` huffman@22608 ` 69` ```lemma BseqE: "\Bseq X; \K. \0 < K; \n. norm (X n) \ K\ \ Q\ \ Q" ``` huffman@22608 ` 70` ```unfolding Bseq_def by auto ``` huffman@22608 ` 71` wenzelm@26312 ` 72` ```lemma BseqI2': assumes K: "\n\N. norm (X n) \ K" shows "Bseq X" ``` wenzelm@26312 ` 73` ```proof (rule BseqI') ``` huffman@22608 ` 74` ``` let ?A = "norm ` X ` {..N}" ``` huffman@22608 ` 75` ``` have 1: "finite ?A" by simp ``` huffman@22608 ` 76` ``` fix n::nat ``` huffman@22608 ` 77` ``` show "norm (X n) \ max K (Max ?A)" ``` huffman@22608 ` 78` ``` proof (cases rule: linorder_le_cases) ``` huffman@22608 ` 79` ``` assume "n \ N" ``` huffman@22608 ` 80` ``` hence "norm (X n) \ K" using K by simp ``` huffman@22608 ` 81` ``` thus "norm (X n) \ max K (Max ?A)" by simp ``` huffman@22608 ` 82` ``` next ``` huffman@22608 ` 83` ``` assume "n \ N" ``` huffman@22608 ` 84` ``` hence "norm (X n) \ ?A" by simp ``` haftmann@26757 ` 85` ``` with 1 have "norm (X n) \ Max ?A" by (rule Max_ge) ``` huffman@22608 ` 86` ``` thus "norm (X n) \ max K (Max ?A)" by simp ``` huffman@22608 ` 87` ``` qed ``` huffman@22608 ` 88` ```qed ``` huffman@22608 ` 89` huffman@22608 ` 90` ```lemma Bseq_ignore_initial_segment: "Bseq X \ Bseq (\n. X (n + k))" ``` huffman@22608 ` 91` ```unfolding Bseq_def by auto ``` huffman@22608 ` 92` huffman@22608 ` 93` ```lemma Bseq_offset: "Bseq (\n. X (n + k)) \ Bseq X" ``` huffman@22608 ` 94` ```apply (erule BseqE) ``` wenzelm@26312 ` 95` ```apply (rule_tac N="k" and K="K" in BseqI2') ``` huffman@22608 ` 96` ```apply clarify ``` huffman@22608 ` 97` ```apply (drule_tac x="n - k" in spec, simp) ``` huffman@22608 ` 98` ```done ``` huffman@22608 ` 99` huffman@22608 ` 100` huffman@22608 ` 101` ```subsection {* Sequences That Converge to Zero *} ``` huffman@22608 ` 102` huffman@22608 ` 103` ```lemma ZseqI: ``` huffman@22608 ` 104` ``` "(\r. 0 < r \ \no. \n\no. norm (X n) < r) \ Zseq X" ``` huffman@22608 ` 105` ```unfolding Zseq_def by simp ``` huffman@22608 ` 106` huffman@22608 ` 107` ```lemma ZseqD: ``` huffman@22608 ` 108` ``` "\Zseq X; 0 < r\ \ \no. \n\no. norm (X n) < r" ``` huffman@22608 ` 109` ```unfolding Zseq_def by simp ``` huffman@22608 ` 110` huffman@22608 ` 111` ```lemma Zseq_zero: "Zseq (\n. 0)" ``` huffman@22608 ` 112` ```unfolding Zseq_def by simp ``` huffman@22608 ` 113` huffman@22608 ` 114` ```lemma Zseq_const_iff: "Zseq (\n. k) = (k = 0)" ``` huffman@22608 ` 115` ```unfolding Zseq_def by force ``` huffman@22608 ` 116` huffman@22608 ` 117` ```lemma Zseq_norm_iff: "Zseq (\n. norm (X n)) = Zseq (\n. X n)" ``` huffman@22608 ` 118` ```unfolding Zseq_def by simp ``` huffman@22608 ` 119` huffman@22608 ` 120` ```lemma Zseq_imp_Zseq: ``` huffman@22608 ` 121` ``` assumes X: "Zseq X" ``` huffman@22608 ` 122` ``` assumes Y: "\n. norm (Y n) \ norm (X n) * K" ``` huffman@22608 ` 123` ``` shows "Zseq (\n. Y n)" ``` huffman@22608 ` 124` ```proof (cases) ``` huffman@22608 ` 125` ``` assume K: "0 < K" ``` huffman@22608 ` 126` ``` show ?thesis ``` huffman@22608 ` 127` ``` proof (rule ZseqI) ``` huffman@22608 ` 128` ``` fix r::real assume "0 < r" ``` huffman@22608 ` 129` ``` hence "0 < r / K" ``` huffman@22608 ` 130` ``` using K by (rule divide_pos_pos) ``` huffman@22608 ` 131` ``` then obtain N where "\n\N. norm (X n) < r / K" ``` huffman@22608 ` 132` ``` using ZseqD [OF X] by fast ``` huffman@22608 ` 133` ``` hence "\n\N. norm (X n) * K < r" ``` huffman@22608 ` 134` ``` by (simp add: pos_less_divide_eq K) ``` huffman@22608 ` 135` ``` hence "\n\N. norm (Y n) < r" ``` huffman@22608 ` 136` ``` by (simp add: order_le_less_trans [OF Y]) ``` huffman@22608 ` 137` ``` thus "\N. \n\N. norm (Y n) < r" .. ``` huffman@22608 ` 138` ``` qed ``` huffman@22608 ` 139` ```next ``` huffman@22608 ` 140` ``` assume "\ 0 < K" ``` huffman@22608 ` 141` ``` hence K: "K \ 0" by (simp only: linorder_not_less) ``` huffman@22608 ` 142` ``` { ``` huffman@22608 ` 143` ``` fix n::nat ``` huffman@22608 ` 144` ``` have "norm (Y n) \ norm (X n) * K" by (rule Y) ``` huffman@22608 ` 145` ``` also have "\ \ norm (X n) * 0" ``` huffman@22608 ` 146` ``` using K norm_ge_zero by (rule mult_left_mono) ``` huffman@22608 ` 147` ``` finally have "norm (Y n) = 0" by simp ``` huffman@22608 ` 148` ``` } ``` huffman@22608 ` 149` ``` thus ?thesis by (simp add: Zseq_zero) ``` huffman@22608 ` 150` ```qed ``` huffman@22608 ` 151` huffman@22608 ` 152` ```lemma Zseq_le: "\Zseq Y; \n. norm (X n) \ norm (Y n)\ \ Zseq X" ``` huffman@22608 ` 153` ```by (erule_tac K="1" in Zseq_imp_Zseq, simp) ``` huffman@22608 ` 154` huffman@22608 ` 155` ```lemma Zseq_add: ``` huffman@22608 ` 156` ``` assumes X: "Zseq X" ``` huffman@22608 ` 157` ``` assumes Y: "Zseq Y" ``` huffman@22608 ` 158` ``` shows "Zseq (\n. X n + Y n)" ``` huffman@22608 ` 159` ```proof (rule ZseqI) ``` huffman@22608 ` 160` ``` fix r::real assume "0 < r" ``` huffman@22608 ` 161` ``` hence r: "0 < r / 2" by simp ``` huffman@22608 ` 162` ``` obtain M where M: "\n\M. norm (X n) < r/2" ``` huffman@22608 ` 163` ``` using ZseqD [OF X r] by fast ``` huffman@22608 ` 164` ``` obtain N where N: "\n\N. norm (Y n) < r/2" ``` huffman@22608 ` 165` ``` using ZseqD [OF Y r] by fast ``` huffman@22608 ` 166` ``` show "\N. \n\N. norm (X n + Y n) < r" ``` huffman@22608 ` 167` ``` proof (intro exI allI impI) ``` huffman@22608 ` 168` ``` fix n assume n: "max M N \ n" ``` huffman@22608 ` 169` ``` have "norm (X n + Y n) \ norm (X n) + norm (Y n)" ``` huffman@22608 ` 170` ``` by (rule norm_triangle_ineq) ``` huffman@22608 ` 171` ``` also have "\ < r/2 + r/2" ``` huffman@22608 ` 172` ``` proof (rule add_strict_mono) ``` huffman@22608 ` 173` ``` from M n show "norm (X n) < r/2" by simp ``` huffman@22608 ` 174` ``` from N n show "norm (Y n) < r/2" by simp ``` huffman@22608 ` 175` ``` qed ``` huffman@22608 ` 176` ``` finally show "norm (X n + Y n) < r" by simp ``` huffman@22608 ` 177` ``` qed ``` huffman@22608 ` 178` ```qed ``` huffman@22608 ` 179` huffman@22608 ` 180` ```lemma Zseq_minus: "Zseq X \ Zseq (\n. - X n)" ``` huffman@22608 ` 181` ```unfolding Zseq_def by simp ``` huffman@22608 ` 182` huffman@22608 ` 183` ```lemma Zseq_diff: "\Zseq X; Zseq Y\ \ Zseq (\n. X n - Y n)" ``` huffman@22608 ` 184` ```by (simp only: diff_minus Zseq_add Zseq_minus) ``` huffman@22608 ` 185` huffman@22608 ` 186` ```lemma (in bounded_linear) Zseq: ``` huffman@22608 ` 187` ``` assumes X: "Zseq X" ``` huffman@22608 ` 188` ``` shows "Zseq (\n. f (X n))" ``` huffman@22608 ` 189` ```proof - ``` huffman@22608 ` 190` ``` obtain K where "\x. norm (f x) \ norm x * K" ``` huffman@22608 ` 191` ``` using bounded by fast ``` huffman@22608 ` 192` ``` with X show ?thesis ``` huffman@22608 ` 193` ``` by (rule Zseq_imp_Zseq) ``` huffman@22608 ` 194` ```qed ``` huffman@22608 ` 195` huffman@23127 ` 196` ```lemma (in bounded_bilinear) Zseq: ``` huffman@22608 ` 197` ``` assumes X: "Zseq X" ``` huffman@22608 ` 198` ``` assumes Y: "Zseq Y" ``` huffman@22608 ` 199` ``` shows "Zseq (\n. X n ** Y n)" ``` huffman@22608 ` 200` ```proof (rule ZseqI) ``` huffman@22608 ` 201` ``` fix r::real assume r: "0 < r" ``` huffman@22608 ` 202` ``` obtain K where K: "0 < K" ``` huffman@22608 ` 203` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@22608 ` 204` ``` using pos_bounded by fast ``` huffman@22608 ` 205` ``` from K have K': "0 < inverse K" ``` huffman@22608 ` 206` ``` by (rule positive_imp_inverse_positive) ``` huffman@22608 ` 207` ``` obtain M where M: "\n\M. norm (X n) < r" ``` huffman@22608 ` 208` ``` using ZseqD [OF X r] by fast ``` huffman@22608 ` 209` ``` obtain N where N: "\n\N. norm (Y n) < inverse K" ``` huffman@22608 ` 210` ``` using ZseqD [OF Y K'] by fast ``` huffman@22608 ` 211` ``` show "\N. \n\N. norm (X n ** Y n) < r" ``` huffman@22608 ` 212` ``` proof (intro exI allI impI) ``` huffman@22608 ` 213` ``` fix n assume n: "max M N \ n" ``` huffman@22608 ` 214` ``` have "norm (X n ** Y n) \ norm (X n) * norm (Y n) * K" ``` huffman@22608 ` 215` ``` by (rule norm_le) ``` huffman@22608 ` 216` ``` also have "norm (X n) * norm (Y n) * K < r * inverse K * K" ``` huffman@22608 ` 217` ``` proof (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero K) ``` huffman@22608 ` 218` ``` from M n show Xn: "norm (X n) < r" by simp ``` huffman@22608 ` 219` ``` from N n show Yn: "norm (Y n) < inverse K" by simp ``` huffman@22608 ` 220` ``` qed ``` huffman@22608 ` 221` ``` also from K have "r * inverse K * K = r" by simp ``` huffman@22608 ` 222` ``` finally show "norm (X n ** Y n) < r" . ``` huffman@22608 ` 223` ``` qed ``` huffman@22608 ` 224` ```qed ``` huffman@22608 ` 225` huffman@22608 ` 226` ```lemma (in bounded_bilinear) Zseq_prod_Bseq: ``` huffman@22608 ` 227` ``` assumes X: "Zseq X" ``` huffman@22608 ` 228` ``` assumes Y: "Bseq Y" ``` huffman@22608 ` 229` ``` shows "Zseq (\n. X n ** Y n)" ``` huffman@22608 ` 230` ```proof - ``` huffman@22608 ` 231` ``` obtain K where K: "0 \ K" ``` huffman@22608 ` 232` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@22608 ` 233` ``` using nonneg_bounded by fast ``` huffman@22608 ` 234` ``` obtain B where B: "0 < B" ``` huffman@22608 ` 235` ``` and norm_Y: "\n. norm (Y n) \ B" ``` huffman@22608 ` 236` ``` using Y [unfolded Bseq_def] by fast ``` huffman@22608 ` 237` ``` from X show ?thesis ``` huffman@22608 ` 238` ``` proof (rule Zseq_imp_Zseq) ``` huffman@22608 ` 239` ``` fix n::nat ``` huffman@22608 ` 240` ``` have "norm (X n ** Y n) \ norm (X n) * norm (Y n) * K" ``` huffman@22608 ` 241` ``` by (rule norm_le) ``` huffman@22608 ` 242` ``` also have "\ \ norm (X n) * B * K" ``` huffman@22608 ` 243` ``` by (intro mult_mono' order_refl norm_Y norm_ge_zero ``` huffman@22608 ` 244` ``` mult_nonneg_nonneg K) ``` huffman@22608 ` 245` ``` also have "\ = norm (X n) * (B * K)" ``` huffman@22608 ` 246` ``` by (rule mult_assoc) ``` huffman@22608 ` 247` ``` finally show "norm (X n ** Y n) \ norm (X n) * (B * K)" . ``` huffman@22608 ` 248` ``` qed ``` huffman@22608 ` 249` ```qed ``` huffman@22608 ` 250` huffman@22608 ` 251` ```lemma (in bounded_bilinear) Bseq_prod_Zseq: ``` huffman@22608 ` 252` ``` assumes X: "Bseq X" ``` huffman@22608 ` 253` ``` assumes Y: "Zseq Y" ``` huffman@22608 ` 254` ``` shows "Zseq (\n. X n ** Y n)" ``` huffman@22608 ` 255` ```proof - ``` huffman@22608 ` 256` ``` obtain K where K: "0 \ K" ``` huffman@22608 ` 257` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@22608 ` 258` ``` using nonneg_bounded by fast ``` huffman@22608 ` 259` ``` obtain B where B: "0 < B" ``` huffman@22608 ` 260` ``` and norm_X: "\n. norm (X n) \ B" ``` huffman@22608 ` 261` ``` using X [unfolded Bseq_def] by fast ``` huffman@22608 ` 262` ``` from Y show ?thesis ``` huffman@22608 ` 263` ``` proof (rule Zseq_imp_Zseq) ``` huffman@22608 ` 264` ``` fix n::nat ``` huffman@22608 ` 265` ``` have "norm (X n ** Y n) \ norm (X n) * norm (Y n) * K" ``` huffman@22608 ` 266` ``` by (rule norm_le) ``` huffman@22608 ` 267` ``` also have "\ \ B * norm (Y n) * K" ``` huffman@22608 ` 268` ``` by (intro mult_mono' order_refl norm_X norm_ge_zero ``` huffman@22608 ` 269` ``` mult_nonneg_nonneg K) ``` huffman@22608 ` 270` ``` also have "\ = norm (Y n) * (B * K)" ``` huffman@22608 ` 271` ``` by (simp only: mult_ac) ``` huffman@22608 ` 272` ``` finally show "norm (X n ** Y n) \ norm (Y n) * (B * K)" . ``` huffman@22608 ` 273` ``` qed ``` huffman@22608 ` 274` ```qed ``` huffman@22608 ` 275` huffman@23127 ` 276` ```lemma (in bounded_bilinear) Zseq_left: ``` huffman@22608 ` 277` ``` "Zseq X \ Zseq (\n. X n ** a)" ``` huffman@22608 ` 278` ```by (rule bounded_linear_left [THEN bounded_linear.Zseq]) ``` huffman@22608 ` 279` huffman@23127 ` 280` ```lemma (in bounded_bilinear) Zseq_right: ``` huffman@22608 ` 281` ``` "Zseq X \ Zseq (\n. a ** X n)" ``` huffman@22608 ` 282` ```by (rule bounded_linear_right [THEN bounded_linear.Zseq]) ``` huffman@22608 ` 283` huffman@23127 ` 284` ```lemmas Zseq_mult = mult.Zseq ``` huffman@23127 ` 285` ```lemmas Zseq_mult_right = mult.Zseq_right ``` huffman@23127 ` 286` ```lemmas Zseq_mult_left = mult.Zseq_left ``` huffman@22608 ` 287` huffman@22608 ` 288` huffman@20696 ` 289` ```subsection {* Limits of Sequences *} ``` huffman@20696 ` 290` paulson@15082 ` 291` ```lemma LIMSEQ_iff: ``` huffman@20563 ` 292` ``` "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" ``` huffman@22608 ` 293` ```by (rule LIMSEQ_def) ``` huffman@22608 ` 294` huffman@22608 ` 295` ```lemma LIMSEQ_Zseq_iff: "((\n. X n) ----> L) = Zseq (\n. X n - L)" ``` huffman@22608 ` 296` ```by (simp only: LIMSEQ_def Zseq_def) ``` paulson@15082 ` 297` huffman@20751 ` 298` ```lemma LIMSEQ_I: ``` huffman@20751 ` 299` ``` "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" ``` huffman@20751 ` 300` ```by (simp add: LIMSEQ_def) ``` huffman@20751 ` 301` huffman@20751 ` 302` ```lemma LIMSEQ_D: ``` huffman@20751 ` 303` ``` "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" ``` huffman@20751 ` 304` ```by (simp add: LIMSEQ_def) ``` huffman@20751 ` 305` huffman@22608 ` 306` ```lemma LIMSEQ_const: "(\n. k) ----> k" ``` huffman@20696 ` 307` ```by (simp add: LIMSEQ_def) ``` huffman@20696 ` 308` huffman@22608 ` 309` ```lemma LIMSEQ_const_iff: "(\n. k) ----> l = (k = l)" ``` huffman@22608 ` 310` ```by (simp add: LIMSEQ_Zseq_iff Zseq_const_iff) ``` huffman@22608 ` 311` huffman@20696 ` 312` ```lemma LIMSEQ_norm: "X ----> a \ (\n. norm (X n)) ----> norm a" ``` huffman@20696 ` 313` ```apply (simp add: LIMSEQ_def, safe) ``` huffman@20696 ` 314` ```apply (drule_tac x="r" in spec, safe) ``` huffman@20696 ` 315` ```apply (rule_tac x="no" in exI, safe) ``` huffman@20696 ` 316` ```apply (drule_tac x="n" in spec, safe) ``` huffman@20696 ` 317` ```apply (erule order_le_less_trans [OF norm_triangle_ineq3]) ``` huffman@20696 ` 318` ```done ``` huffman@20696 ` 319` huffman@22615 ` 320` ```lemma LIMSEQ_ignore_initial_segment: ``` huffman@22615 ` 321` ``` "f ----> a \ (\n. f (n + k)) ----> a" ``` huffman@22615 ` 322` ```apply (rule LIMSEQ_I) ``` huffman@22615 ` 323` ```apply (drule (1) LIMSEQ_D) ``` huffman@22615 ` 324` ```apply (erule exE, rename_tac N) ``` huffman@22615 ` 325` ```apply (rule_tac x=N in exI) ``` huffman@22615 ` 326` ```apply simp ``` huffman@22615 ` 327` ```done ``` huffman@20696 ` 328` huffman@22615 ` 329` ```lemma LIMSEQ_offset: ``` huffman@22615 ` 330` ``` "(\n. f (n + k)) ----> a \ f ----> a" ``` huffman@22615 ` 331` ```apply (rule LIMSEQ_I) ``` huffman@22615 ` 332` ```apply (drule (1) LIMSEQ_D) ``` huffman@22615 ` 333` ```apply (erule exE, rename_tac N) ``` huffman@22615 ` 334` ```apply (rule_tac x="N + k" in exI) ``` huffman@22615 ` 335` ```apply clarify ``` huffman@22615 ` 336` ```apply (drule_tac x="n - k" in spec) ``` huffman@22615 ` 337` ```apply (simp add: le_diff_conv2) ``` huffman@20696 ` 338` ```done ``` huffman@20696 ` 339` huffman@22615 ` 340` ```lemma LIMSEQ_Suc: "f ----> l \ (\n. f (Suc n)) ----> l" ``` huffman@30082 ` 341` ```by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp) ``` huffman@22615 ` 342` huffman@22615 ` 343` ```lemma LIMSEQ_imp_Suc: "(\n. f (Suc n)) ----> l \ f ----> l" ``` huffman@30082 ` 344` ```by (rule_tac k="Suc 0" in LIMSEQ_offset, simp) ``` huffman@22615 ` 345` huffman@22615 ` 346` ```lemma LIMSEQ_Suc_iff: "(\n. f (Suc n)) ----> l = f ----> l" ``` huffman@22615 ` 347` ```by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) ``` huffman@22615 ` 348` hoelzl@29803 ` 349` ```lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ n. X (n * l)) ----> x" ``` hoelzl@29803 ` 350` ``` unfolding LIMSEQ_def ``` hoelzl@29803 ` 351` ``` by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute) ``` hoelzl@29803 ` 352` hoelzl@29803 ` 353` huffman@22608 ` 354` ```lemma add_diff_add: ``` huffman@22608 ` 355` ``` fixes a b c d :: "'a::ab_group_add" ``` huffman@22608 ` 356` ``` shows "(a + c) - (b + d) = (a - b) + (c - d)" ``` huffman@22608 ` 357` ```by simp ``` huffman@22608 ` 358` huffman@22608 ` 359` ```lemma minus_diff_minus: ``` huffman@22608 ` 360` ``` fixes a b :: "'a::ab_group_add" ``` huffman@22608 ` 361` ``` shows "(- a) - (- b) = - (a - b)" ``` huffman@22608 ` 362` ```by simp ``` huffman@22608 ` 363` huffman@22608 ` 364` ```lemma LIMSEQ_add: "\X ----> a; Y ----> b\ \ (\n. X n + Y n) ----> a + b" ``` huffman@22608 ` 365` ```by (simp only: LIMSEQ_Zseq_iff add_diff_add Zseq_add) ``` huffman@22608 ` 366` huffman@22608 ` 367` ```lemma LIMSEQ_minus: "X ----> a \ (\n. - X n) ----> - a" ``` huffman@22608 ` 368` ```by (simp only: LIMSEQ_Zseq_iff minus_diff_minus Zseq_minus) ``` huffman@22608 ` 369` huffman@22608 ` 370` ```lemma LIMSEQ_minus_cancel: "(\n. - X n) ----> - a \ X ----> a" ``` huffman@22608 ` 371` ```by (drule LIMSEQ_minus, simp) ``` huffman@22608 ` 372` huffman@22608 ` 373` ```lemma LIMSEQ_diff: "\X ----> a; Y ----> b\ \ (\n. X n - Y n) ----> a - b" ``` huffman@22608 ` 374` ```by (simp add: diff_minus LIMSEQ_add LIMSEQ_minus) ``` huffman@22608 ` 375` huffman@22608 ` 376` ```lemma LIMSEQ_unique: "\X ----> a; X ----> b\ \ a = b" ``` huffman@22608 ` 377` ```by (drule (1) LIMSEQ_diff, simp add: LIMSEQ_const_iff) ``` huffman@22608 ` 378` huffman@22608 ` 379` ```lemma (in bounded_linear) LIMSEQ: ``` huffman@22608 ` 380` ``` "X ----> a \ (\n. f (X n)) ----> f a" ``` huffman@22608 ` 381` ```by (simp only: LIMSEQ_Zseq_iff diff [symmetric] Zseq) ``` huffman@22608 ` 382` huffman@22608 ` 383` ```lemma (in bounded_bilinear) LIMSEQ: ``` huffman@22608 ` 384` ``` "\X ----> a; Y ----> b\ \ (\n. X n ** Y n) ----> a ** b" ``` huffman@22608 ` 385` ```by (simp only: LIMSEQ_Zseq_iff prod_diff_prod ``` huffman@23127 ` 386` ``` Zseq_add Zseq Zseq_left Zseq_right) ``` huffman@22608 ` 387` huffman@22608 ` 388` ```lemma LIMSEQ_mult: ``` huffman@22608 ` 389` ``` fixes a b :: "'a::real_normed_algebra" ``` huffman@22608 ` 390` ``` shows "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" ``` huffman@23127 ` 391` ```by (rule mult.LIMSEQ) ``` huffman@22608 ` 392` huffman@22608 ` 393` ```lemma inverse_diff_inverse: ``` huffman@22608 ` 394` ``` "\(a::'a::division_ring) \ 0; b \ 0\ ``` huffman@22608 ` 395` ``` \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" ``` nipkow@29667 ` 396` ```by (simp add: algebra_simps) ``` huffman@22608 ` 397` huffman@22608 ` 398` ```lemma Bseq_inverse_lemma: ``` huffman@22608 ` 399` ``` fixes x :: "'a::real_normed_div_algebra" ``` huffman@22608 ` 400` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` huffman@22608 ` 401` ```apply (subst nonzero_norm_inverse, clarsimp) ``` huffman@22608 ` 402` ```apply (erule (1) le_imp_inverse_le) ``` huffman@22608 ` 403` ```done ``` huffman@22608 ` 404` huffman@22608 ` 405` ```lemma Bseq_inverse: ``` huffman@22608 ` 406` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@22608 ` 407` ``` assumes X: "X ----> a" ``` huffman@22608 ` 408` ``` assumes a: "a \ 0" ``` huffman@22608 ` 409` ``` shows "Bseq (\n. inverse (X n))" ``` huffman@22608 ` 410` ```proof - ``` huffman@22608 ` 411` ``` from a have "0 < norm a" by simp ``` huffman@22608 ` 412` ``` hence "\r>0. r < norm a" by (rule dense) ``` huffman@22608 ` 413` ``` then obtain r where r1: "0 < r" and r2: "r < norm a" by fast ``` huffman@22608 ` 414` ``` obtain N where N: "\n. N \ n \ norm (X n - a) < r" ``` huffman@22608 ` 415` ``` using LIMSEQ_D [OF X r1] by fast ``` huffman@22608 ` 416` ``` show ?thesis ``` wenzelm@26312 ` 417` ``` proof (rule BseqI2' [rule_format]) ``` huffman@22608 ` 418` ``` fix n assume n: "N \ n" ``` huffman@22608 ` 419` ``` hence 1: "norm (X n - a) < r" by (rule N) ``` huffman@22608 ` 420` ``` hence 2: "X n \ 0" using r2 by auto ``` huffman@22608 ` 421` ``` hence "norm (inverse (X n)) = inverse (norm (X n))" ``` huffman@22608 ` 422` ``` by (rule nonzero_norm_inverse) ``` huffman@22608 ` 423` ``` also have "\ \ inverse (norm a - r)" ``` huffman@22608 ` 424` ``` proof (rule le_imp_inverse_le) ``` huffman@22608 ` 425` ``` show "0 < norm a - r" using r2 by simp ``` huffman@22608 ` 426` ``` next ``` huffman@22608 ` 427` ``` have "norm a - norm (X n) \ norm (a - X n)" ``` huffman@22608 ` 428` ``` by (rule norm_triangle_ineq2) ``` huffman@22608 ` 429` ``` also have "\ = norm (X n - a)" ``` huffman@22608 ` 430` ``` by (rule norm_minus_commute) ``` huffman@22608 ` 431` ``` also have "\ < r" using 1 . ``` huffman@22608 ` 432` ``` finally show "norm a - r \ norm (X n)" by simp ``` huffman@22608 ` 433` ``` qed ``` huffman@22608 ` 434` ``` finally show "norm (inverse (X n)) \ inverse (norm a - r)" . ``` huffman@22608 ` 435` ``` qed ``` huffman@22608 ` 436` ```qed ``` huffman@22608 ` 437` huffman@22608 ` 438` ```lemma LIMSEQ_inverse_lemma: ``` huffman@22608 ` 439` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@22608 ` 440` ``` shows "\X ----> a; a \ 0; \n. X n \ 0\ ``` huffman@22608 ` 441` ``` \ (\n. inverse (X n)) ----> inverse a" ``` huffman@22608 ` 442` ```apply (subst LIMSEQ_Zseq_iff) ``` huffman@22608 ` 443` ```apply (simp add: inverse_diff_inverse nonzero_imp_inverse_nonzero) ``` huffman@22608 ` 444` ```apply (rule Zseq_minus) ``` huffman@22608 ` 445` ```apply (rule Zseq_mult_left) ``` huffman@23127 ` 446` ```apply (rule mult.Bseq_prod_Zseq) ``` huffman@22608 ` 447` ```apply (erule (1) Bseq_inverse) ``` huffman@22608 ` 448` ```apply (simp add: LIMSEQ_Zseq_iff) ``` huffman@22608 ` 449` ```done ``` huffman@22608 ` 450` huffman@22608 ` 451` ```lemma LIMSEQ_inverse: ``` huffman@22608 ` 452` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@22608 ` 453` ``` assumes X: "X ----> a" ``` huffman@22608 ` 454` ``` assumes a: "a \ 0" ``` huffman@22608 ` 455` ``` shows "(\n. inverse (X n)) ----> inverse a" ``` huffman@22608 ` 456` ```proof - ``` huffman@22608 ` 457` ``` from a have "0 < norm a" by simp ``` huffman@22608 ` 458` ``` then obtain k where "\n\k. norm (X n - a) < norm a" ``` huffman@22608 ` 459` ``` using LIMSEQ_D [OF X] by fast ``` huffman@22608 ` 460` ``` hence "\n\k. X n \ 0" by auto ``` huffman@22608 ` 461` ``` hence k: "\n. X (n + k) \ 0" by simp ``` huffman@22608 ` 462` huffman@22608 ` 463` ``` from X have "(\n. X (n + k)) ----> a" ``` huffman@22608 ` 464` ``` by (rule LIMSEQ_ignore_initial_segment) ``` huffman@22608 ` 465` ``` hence "(\n. inverse (X (n + k))) ----> inverse a" ``` huffman@22608 ` 466` ``` using a k by (rule LIMSEQ_inverse_lemma) ``` huffman@22608 ` 467` ``` thus "(\n. inverse (X n)) ----> inverse a" ``` huffman@22608 ` 468` ``` by (rule LIMSEQ_offset) ``` huffman@22608 ` 469` ```qed ``` huffman@22608 ` 470` huffman@22608 ` 471` ```lemma LIMSEQ_divide: ``` huffman@22608 ` 472` ``` fixes a b :: "'a::real_normed_field" ``` huffman@22608 ` 473` ``` shows "\X ----> a; Y ----> b; b \ 0\ \ (\n. X n / Y n) ----> a / b" ``` huffman@22608 ` 474` ```by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) ``` huffman@22608 ` 475` huffman@22608 ` 476` ```lemma LIMSEQ_pow: ``` huffman@22608 ` 477` ``` fixes a :: "'a::{real_normed_algebra,recpower}" ``` huffman@22608 ` 478` ``` shows "X ----> a \ (\n. (X n) ^ m) ----> a ^ m" ``` huffman@22608 ` 479` ```by (induct m) (simp_all add: power_Suc LIMSEQ_const LIMSEQ_mult) ``` huffman@22608 ` 480` huffman@22608 ` 481` ```lemma LIMSEQ_setsum: ``` huffman@22608 ` 482` ``` assumes n: "\n. n \ S \ X n ----> L n" ``` huffman@22608 ` 483` ``` shows "(\m. \n\S. X n m) ----> (\n\S. L n)" ``` huffman@22608 ` 484` ```proof (cases "finite S") ``` huffman@22608 ` 485` ``` case True ``` huffman@22608 ` 486` ``` thus ?thesis using n ``` huffman@22608 ` 487` ``` proof (induct) ``` huffman@22608 ` 488` ``` case empty ``` huffman@22608 ` 489` ``` show ?case ``` huffman@22608 ` 490` ``` by (simp add: LIMSEQ_const) ``` huffman@22608 ` 491` ``` next ``` huffman@22608 ` 492` ``` case insert ``` huffman@22608 ` 493` ``` thus ?case ``` huffman@22608 ` 494` ``` by (simp add: LIMSEQ_add) ``` huffman@22608 ` 495` ``` qed ``` huffman@22608 ` 496` ```next ``` huffman@22608 ` 497` ``` case False ``` huffman@22608 ` 498` ``` thus ?thesis ``` huffman@22608 ` 499` ``` by (simp add: LIMSEQ_const) ``` huffman@22608 ` 500` ```qed ``` huffman@22608 ` 501` huffman@22608 ` 502` ```lemma LIMSEQ_setprod: ``` huffman@22608 ` 503` ``` fixes L :: "'a \ 'b::{real_normed_algebra,comm_ring_1}" ``` huffman@22608 ` 504` ``` assumes n: "\n. n \ S \ X n ----> L n" ``` huffman@22608 ` 505` ``` shows "(\m. \n\S. X n m) ----> (\n\S. L n)" ``` huffman@22608 ` 506` ```proof (cases "finite S") ``` huffman@22608 ` 507` ``` case True ``` huffman@22608 ` 508` ``` thus ?thesis using n ``` huffman@22608 ` 509` ``` proof (induct) ``` huffman@22608 ` 510` ``` case empty ``` huffman@22608 ` 511` ``` show ?case ``` huffman@22608 ` 512` ``` by (simp add: LIMSEQ_const) ``` huffman@22608 ` 513` ``` next ``` huffman@22608 ` 514` ``` case insert ``` huffman@22608 ` 515` ``` thus ?case ``` huffman@22608 ` 516` ``` by (simp add: LIMSEQ_mult) ``` huffman@22608 ` 517` ``` qed ``` huffman@22608 ` 518` ```next ``` huffman@22608 ` 519` ``` case False ``` huffman@22608 ` 520` ``` thus ?thesis ``` huffman@22608 ` 521` ``` by (simp add: setprod_def LIMSEQ_const) ``` huffman@22608 ` 522` ```qed ``` huffman@22608 ` 523` huffman@22614 ` 524` ```lemma LIMSEQ_add_const: "f ----> a ==> (%n.(f n + b)) ----> a + b" ``` huffman@22614 ` 525` ```by (simp add: LIMSEQ_add LIMSEQ_const) ``` huffman@22614 ` 526` huffman@22614 ` 527` ```(* FIXME: delete *) ``` huffman@22614 ` 528` ```lemma LIMSEQ_add_minus: ``` huffman@22614 ` 529` ``` "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" ``` huffman@22614 ` 530` ```by (simp only: LIMSEQ_add LIMSEQ_minus) ``` huffman@22614 ` 531` huffman@22614 ` 532` ```lemma LIMSEQ_diff_const: "f ----> a ==> (%n.(f n - b)) ----> a - b" ``` huffman@22614 ` 533` ```by (simp add: LIMSEQ_diff LIMSEQ_const) ``` huffman@22614 ` 534` huffman@22614 ` 535` ```lemma LIMSEQ_diff_approach_zero: ``` huffman@22614 ` 536` ``` "g ----> L ==> (%x. f x - g x) ----> 0 ==> ``` huffman@22614 ` 537` ``` f ----> L" ``` huffman@22614 ` 538` ``` apply (drule LIMSEQ_add) ``` huffman@22614 ` 539` ``` apply assumption ``` huffman@22614 ` 540` ``` apply simp ``` huffman@22614 ` 541` ```done ``` huffman@22614 ` 542` huffman@22614 ` 543` ```lemma LIMSEQ_diff_approach_zero2: ``` huffman@22614 ` 544` ``` "f ----> L ==> (%x. f x - g x) ----> 0 ==> ``` huffman@22614 ` 545` ``` g ----> L"; ``` huffman@22614 ` 546` ``` apply (drule LIMSEQ_diff) ``` huffman@22614 ` 547` ``` apply assumption ``` huffman@22614 ` 548` ``` apply simp ``` huffman@22614 ` 549` ```done ``` huffman@22614 ` 550` huffman@22614 ` 551` ```text{*A sequence tends to zero iff its abs does*} ``` huffman@22614 ` 552` ```lemma LIMSEQ_norm_zero: "((\n. norm (X n)) ----> 0) = (X ----> 0)" ``` huffman@22614 ` 553` ```by (simp add: LIMSEQ_def) ``` huffman@22614 ` 554` huffman@22614 ` 555` ```lemma LIMSEQ_rabs_zero: "((%n. \f n\) ----> 0) = (f ----> (0::real))" ``` huffman@22614 ` 556` ```by (simp add: LIMSEQ_def) ``` huffman@22614 ` 557` huffman@22614 ` 558` ```lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \f n\) ----> \l\" ``` huffman@22614 ` 559` ```by (drule LIMSEQ_norm, simp) ``` huffman@22614 ` 560` huffman@22614 ` 561` ```text{*An unbounded sequence's inverse tends to 0*} ``` huffman@22614 ` 562` huffman@22614 ` 563` ```lemma LIMSEQ_inverse_zero: ``` huffman@22974 ` 564` ``` "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) ----> 0" ``` huffman@22974 ` 565` ```apply (rule LIMSEQ_I) ``` huffman@22974 ` 566` ```apply (drule_tac x="inverse r" in spec, safe) ``` huffman@22974 ` 567` ```apply (rule_tac x="N" in exI, safe) ``` huffman@22974 ` 568` ```apply (drule_tac x="n" in spec, safe) ``` huffman@22614 ` 569` ```apply (frule positive_imp_inverse_positive) ``` huffman@22974 ` 570` ```apply (frule (1) less_imp_inverse_less) ``` huffman@22974 ` 571` ```apply (subgoal_tac "0 < X n", simp) ``` huffman@22974 ` 572` ```apply (erule (1) order_less_trans) ``` huffman@22614 ` 573` ```done ``` huffman@22614 ` 574` huffman@22614 ` 575` ```text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} ``` huffman@22614 ` 576` huffman@22614 ` 577` ```lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" ``` huffman@22614 ` 578` ```apply (rule LIMSEQ_inverse_zero, safe) ``` huffman@22974 ` 579` ```apply (cut_tac x = r in reals_Archimedean2) ``` huffman@22614 ` 580` ```apply (safe, rule_tac x = n in exI) ``` huffman@22614 ` 581` ```apply (auto simp add: real_of_nat_Suc) ``` huffman@22614 ` 582` ```done ``` huffman@22614 ` 583` huffman@22614 ` 584` ```text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to ``` huffman@22614 ` 585` ```infinity is now easily proved*} ``` huffman@22614 ` 586` huffman@22614 ` 587` ```lemma LIMSEQ_inverse_real_of_nat_add: ``` huffman@22614 ` 588` ``` "(%n. r + inverse(real(Suc n))) ----> r" ``` huffman@22614 ` 589` ```by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) ``` huffman@22614 ` 590` huffman@22614 ` 591` ```lemma LIMSEQ_inverse_real_of_nat_add_minus: ``` huffman@22614 ` 592` ``` "(%n. r + -inverse(real(Suc n))) ----> r" ``` huffman@22614 ` 593` ```by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) ``` huffman@22614 ` 594` huffman@22614 ` 595` ```lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: ``` huffman@22614 ` 596` ``` "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" ``` huffman@22614 ` 597` ```by (cut_tac b=1 in ``` huffman@22614 ` 598` ``` LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) ``` huffman@22614 ` 599` huffman@22615 ` 600` ```lemma LIMSEQ_le_const: ``` huffman@22615 ` 601` ``` "\X ----> (x::real); \N. \n\N. a \ X n\ \ a \ x" ``` huffman@22615 ` 602` ```apply (rule ccontr, simp only: linorder_not_le) ``` huffman@22615 ` 603` ```apply (drule_tac r="a - x" in LIMSEQ_D, simp) ``` huffman@22615 ` 604` ```apply clarsimp ``` huffman@22615 ` 605` ```apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1) ``` huffman@22615 ` 606` ```apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2) ``` huffman@22615 ` 607` ```apply simp ``` huffman@22615 ` 608` ```done ``` huffman@22615 ` 609` huffman@22615 ` 610` ```lemma LIMSEQ_le_const2: ``` huffman@22615 ` 611` ``` "\X ----> (x::real); \N. \n\N. X n \ a\ \ x \ a" ``` huffman@22615 ` 612` ```apply (subgoal_tac "- a \ - x", simp) ``` huffman@22615 ` 613` ```apply (rule LIMSEQ_le_const) ``` huffman@22615 ` 614` ```apply (erule LIMSEQ_minus) ``` huffman@22615 ` 615` ```apply simp ``` huffman@22615 ` 616` ```done ``` huffman@22615 ` 617` huffman@22615 ` 618` ```lemma LIMSEQ_le: ``` huffman@22615 ` 619` ``` "\X ----> x; Y ----> y; \N. \n\N. X n \ Y n\ \ x \ (y::real)" ``` huffman@22615 ` 620` ```apply (subgoal_tac "0 \ y - x", simp) ``` huffman@22615 ` 621` ```apply (rule LIMSEQ_le_const) ``` huffman@22615 ` 622` ```apply (erule (1) LIMSEQ_diff) ``` huffman@22615 ` 623` ```apply (simp add: le_diff_eq) ``` huffman@22615 ` 624` ```done ``` huffman@22615 ` 625` paulson@15082 ` 626` huffman@20696 ` 627` ```subsection {* Convergence *} ``` paulson@15082 ` 628` paulson@15082 ` 629` ```lemma limI: "X ----> L ==> lim X = L" ``` paulson@15082 ` 630` ```apply (simp add: lim_def) ``` paulson@15082 ` 631` ```apply (blast intro: LIMSEQ_unique) ``` paulson@15082 ` 632` ```done ``` paulson@15082 ` 633` paulson@15082 ` 634` ```lemma convergentD: "convergent X ==> \L. (X ----> L)" ``` paulson@15082 ` 635` ```by (simp add: convergent_def) ``` paulson@15082 ` 636` paulson@15082 ` 637` ```lemma convergentI: "(X ----> L) ==> convergent X" ``` paulson@15082 ` 638` ```by (auto simp add: convergent_def) ``` paulson@15082 ` 639` paulson@15082 ` 640` ```lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)" ``` huffman@20682 ` 641` ```by (auto intro: theI LIMSEQ_unique simp add: convergent_def lim_def) ``` paulson@15082 ` 642` huffman@20696 ` 643` ```lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))" ``` huffman@20696 ` 644` ```apply (simp add: convergent_def) ``` huffman@20696 ` 645` ```apply (auto dest: LIMSEQ_minus) ``` huffman@20696 ` 646` ```apply (drule LIMSEQ_minus, auto) ``` huffman@20696 ` 647` ```done ``` huffman@20696 ` 648` chaieb@30196 ` 649` ```text{* Given a binary function @{text "f:: nat \ 'a \ 'a"}, its values are uniquely determined by a function g *} ``` huffman@20696 ` 650` chaieb@30196 ` 651` ```lemma nat_function_unique: "EX! g. g 0 = e \ (\n. g (Suc n) = f n (g n))" ``` chaieb@30196 ` 652` ``` unfolding Ex1_def ``` chaieb@30196 ` 653` ``` apply (rule_tac x="nat_rec e f" in exI) ``` chaieb@30196 ` 654` ``` apply (rule conjI)+ ``` chaieb@30196 ` 655` ```apply (rule def_nat_rec_0, simp) ``` chaieb@30196 ` 656` ```apply (rule allI, rule def_nat_rec_Suc, simp) ``` chaieb@30196 ` 657` ```apply (rule allI, rule impI, rule ext) ``` chaieb@30196 ` 658` ```apply (erule conjE) ``` chaieb@30196 ` 659` ```apply (induct_tac x) ``` chaieb@30196 ` 660` ```apply (simp add: nat_rec_0) ``` chaieb@30196 ` 661` ```apply (erule_tac x="n" in allE) ``` chaieb@30196 ` 662` ```apply (simp) ``` chaieb@30196 ` 663` ```done ``` huffman@20696 ` 664` paulson@15082 ` 665` ```text{*Subsequence (alternative definition, (e.g. Hoskins)*} ``` paulson@15082 ` 666` paulson@15082 ` 667` ```lemma subseq_Suc_iff: "subseq f = (\n. (f n) < (f (Suc n)))" ``` paulson@15082 ` 668` ```apply (simp add: subseq_def) ``` paulson@15082 ` 669` ```apply (auto dest!: less_imp_Suc_add) ``` paulson@15082 ` 670` ```apply (induct_tac k) ``` paulson@15082 ` 671` ```apply (auto intro: less_trans) ``` paulson@15082 ` 672` ```done ``` paulson@15082 ` 673` paulson@15082 ` 674` ```lemma monoseq_Suc: ``` paulson@15082 ` 675` ``` "monoseq X = ((\n. X n \ X (Suc n)) ``` paulson@15082 ` 676` ``` | (\n. X (Suc n) \ X n))" ``` paulson@15082 ` 677` ```apply (simp add: monoseq_def) ``` paulson@15082 ` 678` ```apply (auto dest!: le_imp_less_or_eq) ``` paulson@15082 ` 679` ```apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) ``` paulson@15082 ` 680` ```apply (induct_tac "ka") ``` paulson@15082 ` 681` ```apply (auto intro: order_trans) ``` wenzelm@18585 ` 682` ```apply (erule contrapos_np) ``` paulson@15082 ` 683` ```apply (induct_tac "k") ``` paulson@15082 ` 684` ```apply (auto intro: order_trans) ``` paulson@15082 ` 685` ```done ``` paulson@15082 ` 686` nipkow@15360 ` 687` ```lemma monoI1: "\m. \ n \ m. X m \ X n ==> monoseq X" ``` paulson@15082 ` 688` ```by (simp add: monoseq_def) ``` paulson@15082 ` 689` nipkow@15360 ` 690` ```lemma monoI2: "\m. \ n \ m. X n \ X m ==> monoseq X" ``` paulson@15082 ` 691` ```by (simp add: monoseq_def) ``` paulson@15082 ` 692` paulson@15082 ` 693` ```lemma mono_SucI1: "\n. X n \ X (Suc n) ==> monoseq X" ``` paulson@15082 ` 694` ```by (simp add: monoseq_Suc) ``` paulson@15082 ` 695` paulson@15082 ` 696` ```lemma mono_SucI2: "\n. X (Suc n) \ X n ==> monoseq X" ``` paulson@15082 ` 697` ```by (simp add: monoseq_Suc) ``` paulson@15082 ` 698` hoelzl@29803 ` 699` ```lemma monoseq_minus: assumes "monoseq a" ``` hoelzl@29803 ` 700` ``` shows "monoseq (\ n. - a n)" ``` hoelzl@29803 ` 701` ```proof (cases "\ m. \ n \ m. a m \ a n") ``` hoelzl@29803 ` 702` ``` case True ``` hoelzl@29803 ` 703` ``` hence "\ m. \ n \ m. - a n \ - a m" by auto ``` hoelzl@29803 ` 704` ``` thus ?thesis by (rule monoI2) ``` hoelzl@29803 ` 705` ```next ``` hoelzl@29803 ` 706` ``` case False ``` hoelzl@29803 ` 707` ``` hence "\ m. \ n \ m. - a m \ - a n" using `monoseq a`[unfolded monoseq_def] by auto ``` hoelzl@29803 ` 708` ``` thus ?thesis by (rule monoI1) ``` hoelzl@29803 ` 709` ```qed ``` hoelzl@29803 ` 710` hoelzl@29803 ` 711` ```lemma monoseq_le: assumes "monoseq a" and "a ----> x" ``` hoelzl@29803 ` 712` ``` shows "((\ n. a n \ x) \ (\m. \n\m. a m \ a n)) \ ``` hoelzl@29803 ` 713` ``` ((\ n. x \ a n) \ (\m. \n\m. a n \ a m))" ``` hoelzl@29803 ` 714` ```proof - ``` hoelzl@29803 ` 715` ``` { fix x n fix a :: "nat \ real" ``` hoelzl@29803 ` 716` ``` assume "a ----> x" and "\ m. \ n \ m. a m \ a n" ``` hoelzl@29803 ` 717` ``` hence monotone: "\ m n. m \ n \ a m \ a n" by auto ``` hoelzl@29803 ` 718` ``` have "a n \ x" ``` hoelzl@29803 ` 719` ``` proof (rule ccontr) ``` hoelzl@29803 ` 720` ``` assume "\ a n \ x" hence "x < a n" by auto ``` hoelzl@29803 ` 721` ``` hence "0 < a n - x" by auto ``` hoelzl@29803 ` 722` ``` from `a ----> x`[THEN LIMSEQ_D, OF this] ``` hoelzl@29803 ` 723` ``` obtain no where "\n'. no \ n' \ norm (a n' - x) < a n - x" by blast ``` hoelzl@29803 ` 724` ``` hence "norm (a (max no n) - x) < a n - x" by auto ``` hoelzl@29803 ` 725` ``` moreover ``` hoelzl@29803 ` 726` ``` { fix n' have "n \ n' \ x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto } ``` hoelzl@29803 ` 727` ``` hence "x < a (max no n)" by auto ``` hoelzl@29803 ` 728` ``` ultimately ``` hoelzl@29803 ` 729` ``` have "a (max no n) < a n" by auto ``` hoelzl@29803 ` 730` ``` with monotone[where m=n and n="max no n"] ``` hoelzl@29803 ` 731` ``` show False by auto ``` hoelzl@29803 ` 732` ``` qed ``` hoelzl@29803 ` 733` ``` } note top_down = this ``` hoelzl@29803 ` 734` ``` { fix x n m fix a :: "nat \ real" ``` hoelzl@29803 ` 735` ``` assume "a ----> x" and "monoseq a" and "a m < x" ``` hoelzl@29803 ` 736` ``` have "a n \ x \ (\ m. \ n \ m. a m \ a n)" ``` hoelzl@29803 ` 737` ``` proof (cases "\ m. \ n \ m. a m \ a n") ``` hoelzl@29803 ` 738` ``` case True with top_down and `a ----> x` show ?thesis by auto ``` hoelzl@29803 ` 739` ``` next ``` hoelzl@29803 ` 740` ``` case False with `monoseq a`[unfolded monoseq_def] have "\ m. \ n \ m. - a m \ - a n" by auto ``` hoelzl@29803 ` 741` ``` hence "- a m \ - x" using top_down[OF LIMSEQ_minus[OF `a ----> x`]] by blast ``` hoelzl@29803 ` 742` ``` hence False using `a m < x` by auto ``` hoelzl@29803 ` 743` ``` thus ?thesis .. ``` hoelzl@29803 ` 744` ``` qed ``` hoelzl@29803 ` 745` ``` } note when_decided = this ``` hoelzl@29803 ` 746` hoelzl@29803 ` 747` ``` show ?thesis ``` hoelzl@29803 ` 748` ``` proof (cases "\ m. a m \ x") ``` hoelzl@29803 ` 749` ``` case True then obtain m where "a m \ x" by auto ``` hoelzl@29803 ` 750` ``` show ?thesis ``` hoelzl@29803 ` 751` ``` proof (cases "a m < x") ``` hoelzl@29803 ` 752` ``` case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m] ``` hoelzl@29803 ` 753` ``` show ?thesis by blast ``` hoelzl@29803 ` 754` ``` next ``` hoelzl@29803 ` 755` ``` case False hence "- a m < - x" using `a m \ x` by auto ``` hoelzl@29803 ` 756` ``` with when_decided[OF LIMSEQ_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m] ``` hoelzl@29803 ` 757` ``` show ?thesis by auto ``` hoelzl@29803 ` 758` ``` qed ``` hoelzl@29803 ` 759` ``` qed auto ``` hoelzl@29803 ` 760` ```qed ``` hoelzl@29803 ` 761` chaieb@30196 ` 762` ```text{* for any sequence, there is a mootonic subsequence *} ``` chaieb@30196 ` 763` ```lemma seq_monosub: "\f. subseq f \ monoseq (\ n. (s (f n)))" ``` chaieb@30196 ` 764` ```proof- ``` chaieb@30196 ` 765` ``` {assume H: "\n. \p >n. \ m\p. s m \ s p" ``` chaieb@30196 ` 766` ``` let ?P = "\ p n. p > n \ (\m \ p. s m \ s p)" ``` chaieb@30196 ` 767` ``` from nat_function_unique[of "SOME p. ?P p 0" "\p n. SOME p. ?P p n"] ``` chaieb@30196 ` 768` ``` obtain f where f: "f 0 = (SOME p. ?P p 0)" "\n. f (Suc n) = (SOME p. ?P p (f n))" by blast ``` chaieb@30196 ` 769` ``` have "?P (f 0) 0" unfolding f(1) some_eq_ex[of "\p. ?P p 0"] ``` chaieb@30196 ` 770` ``` using H apply - ``` chaieb@30196 ` 771` ``` apply (erule allE[where x=0], erule exE, rule_tac x="p" in exI) ``` chaieb@30196 ` 772` ``` unfolding order_le_less by blast ``` chaieb@30196 ` 773` ``` hence f0: "f 0 > 0" "\m \ f 0. s m \ s (f 0)" by blast+ ``` chaieb@30196 ` 774` ``` {fix n ``` chaieb@30196 ` 775` ``` have "?P (f (Suc n)) (f n)" ``` chaieb@30196 ` 776` ``` unfolding f(2)[rule_format, of n] some_eq_ex[of "\p. ?P p (f n)"] ``` chaieb@30196 ` 777` ``` using H apply - ``` chaieb@30196 ` 778` ``` apply (erule allE[where x="f n"], erule exE, rule_tac x="p" in exI) ``` chaieb@30196 ` 779` ``` unfolding order_le_less by blast ``` chaieb@30196 ` 780` ``` hence "f (Suc n) > f n" "\m \ f (Suc n). s m \ s (f (Suc n))" by blast+} ``` chaieb@30196 ` 781` ``` note fSuc = this ``` chaieb@30196 ` 782` ``` {fix p q assume pq: "p \ f q" ``` chaieb@30196 ` 783` ``` have "s p \ s(f(q))" using f0(2)[rule_format, of p] pq fSuc ``` chaieb@30196 ` 784` ``` by (cases q, simp_all) } ``` chaieb@30196 ` 785` ``` note pqth = this ``` chaieb@30196 ` 786` ``` {fix q ``` chaieb@30196 ` 787` ``` have "f (Suc q) > f q" apply (induct q) ``` chaieb@30196 ` 788` ``` using f0(1) fSuc(1)[of 0] apply simp by (rule fSuc(1))} ``` chaieb@30196 ` 789` ``` note fss = this ``` chaieb@30196 ` 790` ``` from fss have th1: "subseq f" unfolding subseq_Suc_iff .. ``` chaieb@30196 ` 791` ``` {fix a b ``` chaieb@30196 ` 792` ``` have "f a \ f (a + b)" ``` chaieb@30196 ` 793` ``` proof(induct b) ``` chaieb@30196 ` 794` ``` case 0 thus ?case by simp ``` chaieb@30196 ` 795` ``` next ``` chaieb@30196 ` 796` ``` case (Suc b) ``` chaieb@30196 ` 797` ``` from fSuc(1)[of "a + b"] Suc.hyps show ?case by simp ``` chaieb@30196 ` 798` ``` qed} ``` chaieb@30196 ` 799` ``` note fmon0 = this ``` chaieb@30196 ` 800` ``` have "monoseq (\n. s (f n))" ``` chaieb@30196 ` 801` ``` proof- ``` chaieb@30196 ` 802` ``` {fix n ``` chaieb@30196 ` 803` ``` have "s (f n) \ s (f (Suc n))" ``` chaieb@30196 ` 804` ``` proof(cases n) ``` chaieb@30196 ` 805` ``` case 0 ``` chaieb@30196 ` 806` ``` assume n0: "n = 0" ``` chaieb@30196 ` 807` ``` from fSuc(1)[of 0] have th0: "f 0 \ f (Suc 0)" by simp ``` chaieb@30196 ` 808` ``` from f0(2)[rule_format, OF th0] show ?thesis using n0 by simp ``` chaieb@30196 ` 809` ``` next ``` chaieb@30196 ` 810` ``` case (Suc m) ``` chaieb@30196 ` 811` ``` assume m: "n = Suc m" ``` chaieb@30196 ` 812` ``` from fSuc(1)[of n] m have th0: "f (Suc m) \ f (Suc (Suc m))" by simp ``` chaieb@30196 ` 813` ``` from m fSuc(2)[rule_format, OF th0] show ?thesis by simp ``` chaieb@30196 ` 814` ``` qed} ``` chaieb@30196 ` 815` ``` thus "monoseq (\n. s (f n))" unfolding monoseq_Suc by blast ``` chaieb@30196 ` 816` ``` qed ``` chaieb@30196 ` 817` ``` with th1 have ?thesis by blast} ``` chaieb@30196 ` 818` ``` moreover ``` chaieb@30196 ` 819` ``` {fix N assume N: "\p >N. \ m\p. s m > s p" ``` chaieb@30196 ` 820` ``` {fix p assume p: "p \ Suc N" ``` chaieb@30196 ` 821` ``` hence pN: "p > N" by arith with N obtain m where m: "m \ p" "s m > s p" by blast ``` chaieb@30196 ` 822` ``` have "m \ p" using m(2) by auto ``` chaieb@30196 ` 823` ``` with m have "\m>p. s p < s m" by - (rule exI[where x=m], auto)} ``` chaieb@30196 ` 824` ``` note th0 = this ``` chaieb@30196 ` 825` ``` let ?P = "\m x. m > x \ s x < s m" ``` chaieb@30196 ` 826` ``` from nat_function_unique[of "SOME x. ?P x (Suc N)" "\m x. SOME y. ?P y x"] ``` chaieb@30196 ` 827` ``` obtain f where f: "f 0 = (SOME x. ?P x (Suc N))" ``` chaieb@30196 ` 828` ``` "\n. f (Suc n) = (SOME m. ?P m (f n))" by blast ``` chaieb@30196 ` 829` ``` have "?P (f 0) (Suc N)" unfolding f(1) some_eq_ex[of "\p. ?P p (Suc N)"] ``` chaieb@30196 ` 830` ``` using N apply - ``` chaieb@30196 ` 831` ``` apply (erule allE[where x="Suc N"], clarsimp) ``` chaieb@30196 ` 832` ``` apply (rule_tac x="m" in exI) ``` chaieb@30196 ` 833` ``` apply auto ``` chaieb@30196 ` 834` ``` apply (subgoal_tac "Suc N \ m") ``` chaieb@30196 ` 835` ``` apply simp ``` chaieb@30196 ` 836` ``` apply (rule ccontr, simp) ``` chaieb@30196 ` 837` ``` done ``` chaieb@30196 ` 838` ``` hence f0: "f 0 > Suc N" "s (Suc N) < s (f 0)" by blast+ ``` chaieb@30196 ` 839` ``` {fix n ``` chaieb@30196 ` 840` ``` have "f n > N \ ?P (f (Suc n)) (f n)" ``` chaieb@30196 ` 841` ``` unfolding f(2)[rule_format, of n] some_eq_ex[of "\p. ?P p (f n)"] ``` chaieb@30196 ` 842` ``` proof (induct n) ``` chaieb@30196 ` 843` ``` case 0 thus ?case ``` chaieb@30196 ` 844` ``` using f0 N apply auto ``` chaieb@30196 ` 845` ``` apply (erule allE[where x="f 0"], clarsimp) ``` chaieb@30196 ` 846` ``` apply (rule_tac x="m" in exI, simp) ``` chaieb@30196 ` 847` ``` by (subgoal_tac "f 0 \ m", auto) ``` chaieb@30196 ` 848` ``` next ``` chaieb@30196 ` 849` ``` case (Suc n) ``` chaieb@30196 ` 850` ``` from Suc.hyps have Nfn: "N < f n" by blast ``` chaieb@30196 ` 851` ``` from Suc.hyps obtain m where m: "m > f n" "s (f n) < s m" by blast ``` chaieb@30196 ` 852` ``` with Nfn have mN: "m > N" by arith ``` chaieb@30196 ` 853` ``` note key = Suc.hyps[unfolded some_eq_ex[of "\p. ?P p (f n)", symmetric] f(2)[rule_format, of n, symmetric]] ``` chaieb@30196 ` 854` ``` ``` chaieb@30196 ` 855` ``` from key have th0: "f (Suc n) > N" by simp ``` chaieb@30196 ` 856` ``` from N[rule_format, OF th0] ``` chaieb@30196 ` 857` ``` obtain m' where m': "m' \ f (Suc n)" "s (f (Suc n)) < s m'" by blast ``` chaieb@30196 ` 858` ``` have "m' \ f (Suc (n))" apply (rule ccontr) using m'(2) by auto ``` chaieb@30196 ` 859` ``` hence "m' > f (Suc n)" using m'(1) by simp ``` chaieb@30196 ` 860` ``` with key m'(2) show ?case by auto ``` chaieb@30196 ` 861` ``` qed} ``` chaieb@30196 ` 862` ``` note fSuc = this ``` chaieb@30196 ` 863` ``` {fix n ``` chaieb@30196 ` 864` ``` have "f n \ Suc N \ f(Suc n) > f n \ s(f n) < s(f(Suc n))" using fSuc[of n] by auto ``` chaieb@30196 ` 865` ``` hence "f n \ Suc N" "f(Suc n) > f n" "s(f n) < s(f(Suc n))" by blast+} ``` chaieb@30196 ` 866` ``` note thf = this ``` chaieb@30196 ` 867` ``` have sqf: "subseq f" unfolding subseq_Suc_iff using thf by simp ``` chaieb@30196 ` 868` ``` have "monoseq (\n. s (f n))" unfolding monoseq_Suc using thf ``` chaieb@30196 ` 869` ``` apply - ``` chaieb@30196 ` 870` ``` apply (rule disjI1) ``` chaieb@30196 ` 871` ``` apply auto ``` chaieb@30196 ` 872` ``` apply (rule order_less_imp_le) ``` chaieb@30196 ` 873` ``` apply blast ``` chaieb@30196 ` 874` ``` done ``` chaieb@30196 ` 875` ``` then have ?thesis using sqf by blast} ``` chaieb@30196 ` 876` ``` ultimately show ?thesis unfolding linorder_not_less[symmetric] by blast ``` chaieb@30196 ` 877` ```qed ``` chaieb@30196 ` 878` chaieb@30196 ` 879` ```lemma seq_suble: assumes sf: "subseq f" shows "n \ f n" ``` chaieb@30196 ` 880` ```proof(induct n) ``` chaieb@30196 ` 881` ``` case 0 thus ?case by simp ``` chaieb@30196 ` 882` ```next ``` chaieb@30196 ` 883` ``` case (Suc n) ``` chaieb@30196 ` 884` ``` from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps ``` chaieb@30196 ` 885` ``` have "n < f (Suc n)" by arith ``` chaieb@30196 ` 886` ``` thus ?case by arith ``` chaieb@30196 ` 887` ```qed ``` chaieb@30196 ` 888` chaieb@30196 ` 889` ```subsection {* Bounded Monotonic Sequences *} ``` chaieb@30196 ` 890` chaieb@30196 ` 891` huffman@20696 ` 892` ```text{*Bounded Sequence*} ``` paulson@15082 ` 893` huffman@20552 ` 894` ```lemma BseqD: "Bseq X ==> \K. 0 < K & (\n. norm (X n) \ K)" ``` paulson@15082 ` 895` ```by (simp add: Bseq_def) ``` paulson@15082 ` 896` huffman@20552 ` 897` ```lemma BseqI: "[| 0 < K; \n. norm (X n) \ K |] ==> Bseq X" ``` paulson@15082 ` 898` ```by (auto simp add: Bseq_def) ``` paulson@15082 ` 899` paulson@15082 ` 900` ```lemma lemma_NBseq_def: ``` huffman@20552 ` 901` ``` "(\K > 0. \n. norm (X n) \ K) = ``` huffman@20552 ` 902` ``` (\N. \n. norm (X n) \ real(Suc N))" ``` paulson@15082 ` 903` ```apply auto ``` paulson@15082 ` 904` ``` prefer 2 apply force ``` paulson@15082 ` 905` ```apply (cut_tac x = K in reals_Archimedean2, clarify) ``` paulson@15082 ` 906` ```apply (rule_tac x = n in exI, clarify) ``` paulson@15082 ` 907` ```apply (drule_tac x = na in spec) ``` paulson@15082 ` 908` ```apply (auto simp add: real_of_nat_Suc) ``` paulson@15082 ` 909` ```done ``` paulson@15082 ` 910` paulson@15082 ` 911` ```text{* alternative definition for Bseq *} ``` huffman@20552 ` 912` ```lemma Bseq_iff: "Bseq X = (\N. \n. norm (X n) \ real(Suc N))" ``` paulson@15082 ` 913` ```apply (simp add: Bseq_def) ``` paulson@15082 ` 914` ```apply (simp (no_asm) add: lemma_NBseq_def) ``` paulson@15082 ` 915` ```done ``` paulson@15082 ` 916` paulson@15082 ` 917` ```lemma lemma_NBseq_def2: ``` huffman@20552 ` 918` ``` "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) < real(Suc N))" ``` paulson@15082 ` 919` ```apply (subst lemma_NBseq_def, auto) ``` paulson@15082 ` 920` ```apply (rule_tac x = "Suc N" in exI) ``` paulson@15082 ` 921` ```apply (rule_tac [2] x = N in exI) ``` paulson@15082 ` 922` ```apply (auto simp add: real_of_nat_Suc) ``` paulson@15082 ` 923` ``` prefer 2 apply (blast intro: order_less_imp_le) ``` paulson@15082 ` 924` ```apply (drule_tac x = n in spec, simp) ``` paulson@15082 ` 925` ```done ``` paulson@15082 ` 926` paulson@15082 ` 927` ```(* yet another definition for Bseq *) ``` huffman@20552 ` 928` ```lemma Bseq_iff1a: "Bseq X = (\N. \n. norm (X n) < real(Suc N))" ``` paulson@15082 ` 929` ```by (simp add: Bseq_def lemma_NBseq_def2) ``` paulson@15082 ` 930` huffman@20696 ` 931` ```subsubsection{*Upper Bounds and Lubs of Bounded Sequences*} ``` paulson@15082 ` 932` paulson@15082 ` 933` ```lemma Bseq_isUb: ``` paulson@15082 ` 934` ``` "!!(X::nat=>real). Bseq X ==> \U. isUb (UNIV::real set) {x. \n. X n = x} U" ``` huffman@22998 ` 935` ```by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) ``` paulson@15082 ` 936` paulson@15082 ` 937` paulson@15082 ` 938` ```text{* Use completeness of reals (supremum property) ``` paulson@15082 ` 939` ``` to show that any bounded sequence has a least upper bound*} ``` paulson@15082 ` 940` paulson@15082 ` 941` ```lemma Bseq_isLub: ``` paulson@15082 ` 942` ``` "!!(X::nat=>real). Bseq X ==> ``` paulson@15082 ` 943` ``` \U. isLub (UNIV::real set) {x. \n. X n = x} U" ``` paulson@15082 ` 944` ```by (blast intro: reals_complete Bseq_isUb) ``` paulson@15082 ` 945` huffman@20696 ` 946` ```subsubsection{*A Bounded and Monotonic Sequence Converges*} ``` paulson@15082 ` 947` paulson@15082 ` 948` ```lemma lemma_converg1: ``` nipkow@15360 ` 949` ``` "!!(X::nat=>real). [| \m. \ n \ m. X m \ X n; ``` paulson@15082 ` 950` ``` isLub (UNIV::real set) {x. \n. X n = x} (X ma) ``` nipkow@15360 ` 951` ``` |] ==> \n \ ma. X n = X ma" ``` paulson@15082 ` 952` ```apply safe ``` paulson@15082 ` 953` ```apply (drule_tac y = "X n" in isLubD2) ``` paulson@15082 ` 954` ```apply (blast dest: order_antisym)+ ``` paulson@15082 ` 955` ```done ``` paulson@15082 ` 956` paulson@15082 ` 957` ```text{* The best of both worlds: Easier to prove this result as a standard ``` paulson@15082 ` 958` ``` theorem and then use equivalence to "transfer" it into the ``` paulson@15082 ` 959` ``` equivalent nonstandard form if needed!*} ``` paulson@15082 ` 960` paulson@15082 ` 961` ```lemma Bmonoseq_LIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X ----> L)" ``` paulson@15082 ` 962` ```apply (simp add: LIMSEQ_def) ``` paulson@15082 ` 963` ```apply (rule_tac x = "X m" in exI, safe) ``` paulson@15082 ` 964` ```apply (rule_tac x = m in exI, safe) ``` paulson@15082 ` 965` ```apply (drule spec, erule impE, auto) ``` paulson@15082 ` 966` ```done ``` paulson@15082 ` 967` paulson@15082 ` 968` ```lemma lemma_converg2: ``` paulson@15082 ` 969` ``` "!!(X::nat=>real). ``` paulson@15082 ` 970` ``` [| \m. X m ~= U; isLub UNIV {x. \n. X n = x} U |] ==> \m. X m < U" ``` paulson@15082 ` 971` ```apply safe ``` paulson@15082 ` 972` ```apply (drule_tac y = "X m" in isLubD2) ``` paulson@15082 ` 973` ```apply (auto dest!: order_le_imp_less_or_eq) ``` paulson@15082 ` 974` ```done ``` paulson@15082 ` 975` paulson@15082 ` 976` ```lemma lemma_converg3: "!!(X ::nat=>real). \m. X m \ U ==> isUb UNIV {x. \n. X n = x} U" ``` paulson@15082 ` 977` ```by (rule setleI [THEN isUbI], auto) ``` paulson@15082 ` 978` paulson@15082 ` 979` ```text{* FIXME: @{term "U - T < U"} is redundant *} ``` paulson@15082 ` 980` ```lemma lemma_converg4: "!!(X::nat=> real). ``` paulson@15082 ` 981` ``` [| \m. X m ~= U; ``` paulson@15082 ` 982` ``` isLub UNIV {x. \n. X n = x} U; ``` paulson@15082 ` 983` ``` 0 < T; ``` paulson@15082 ` 984` ``` U + - T < U ``` paulson@15082 ` 985` ``` |] ==> \m. U + -T < X m & X m < U" ``` paulson@15082 ` 986` ```apply (drule lemma_converg2, assumption) ``` paulson@15082 ` 987` ```apply (rule ccontr, simp) ``` paulson@15082 ` 988` ```apply (simp add: linorder_not_less) ``` paulson@15082 ` 989` ```apply (drule lemma_converg3) ``` paulson@15082 ` 990` ```apply (drule isLub_le_isUb, assumption) ``` paulson@15082 ` 991` ```apply (auto dest: order_less_le_trans) ``` paulson@15082 ` 992` ```done ``` paulson@15082 ` 993` paulson@15082 ` 994` ```text{*A standard proof of the theorem for monotone increasing sequence*} ``` paulson@15082 ` 995` paulson@15082 ` 996` ```lemma Bseq_mono_convergent: ``` huffman@20552 ` 997` ``` "[| Bseq X; \m. \n \ m. X m \ X n |] ==> convergent (X::nat=>real)" ``` paulson@15082 ` 998` ```apply (simp add: convergent_def) ``` paulson@15082 ` 999` ```apply (frule Bseq_isLub, safe) ``` paulson@15082 ` 1000` ```apply (case_tac "\m. X m = U", auto) ``` paulson@15082 ` 1001` ```apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ) ``` paulson@15082 ` 1002` ```(* second case *) ``` paulson@15082 ` 1003` ```apply (rule_tac x = U in exI) ``` paulson@15082 ` 1004` ```apply (subst LIMSEQ_iff, safe) ``` paulson@15082 ` 1005` ```apply (frule lemma_converg2, assumption) ``` paulson@15082 ` 1006` ```apply (drule lemma_converg4, auto) ``` paulson@15082 ` 1007` ```apply (rule_tac x = m in exI, safe) ``` paulson@15082 ` 1008` ```apply (subgoal_tac "X m \ X n") ``` paulson@15082 ` 1009` ``` prefer 2 apply blast ``` paulson@15082 ` 1010` ```apply (drule_tac x=n and P="%m. X m < U" in spec, arith) ``` paulson@15082 ` 1011` ```done ``` paulson@15082 ` 1012` paulson@15082 ` 1013` ```lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X" ``` paulson@15082 ` 1014` ```by (simp add: Bseq_def) ``` paulson@15082 ` 1015` paulson@15082 ` 1016` ```text{*Main monotonicity theorem*} ``` paulson@15082 ` 1017` ```lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X" ``` paulson@15082 ` 1018` ```apply (simp add: monoseq_def, safe) ``` paulson@15082 ` 1019` ```apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) ``` paulson@15082 ` 1020` ```apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) ``` paulson@15082 ` 1021` ```apply (auto intro!: Bseq_mono_convergent) ``` paulson@15082 ` 1022` ```done ``` paulson@15082 ` 1023` huffman@20696 ` 1024` ```subsubsection{*A Few More Equivalence Theorems for Boundedness*} ``` paulson@15082 ` 1025` paulson@15082 ` 1026` ```text{*alternative formulation for boundedness*} ``` huffman@20552 ` 1027` ```lemma Bseq_iff2: "Bseq X = (\k > 0. \x. \n. norm (X(n) + -x) \ k)" ``` paulson@15082 ` 1028` ```apply (unfold Bseq_def, safe) ``` huffman@20552 ` 1029` ```apply (rule_tac [2] x = "k + norm x" in exI) ``` nipkow@15360 ` 1030` ```apply (rule_tac x = K in exI, simp) ``` paulson@15221 ` 1031` ```apply (rule exI [where x = 0], auto) ``` huffman@20552 ` 1032` ```apply (erule order_less_le_trans, simp) ``` huffman@20552 ` 1033` ```apply (drule_tac x=n in spec, fold diff_def) ``` huffman@20552 ` 1034` ```apply (drule order_trans [OF norm_triangle_ineq2]) ``` huffman@20552 ` 1035` ```apply simp ``` paulson@15082 ` 1036` ```done ``` paulson@15082 ` 1037` paulson@15082 ` 1038` ```text{*alternative formulation for boundedness*} ``` huffman@20552 ` 1039` ```lemma Bseq_iff3: "Bseq X = (\k > 0. \N. \n. norm(X(n) + -X(N)) \ k)" ``` paulson@15082 ` 1040` ```apply safe ``` paulson@15082 ` 1041` ```apply (simp add: Bseq_def, safe) ``` huffman@20552 ` 1042` ```apply (rule_tac x = "K + norm (X N)" in exI) ``` paulson@15082 ` 1043` ```apply auto ``` huffman@20552 ` 1044` ```apply (erule order_less_le_trans, simp) ``` paulson@15082 ` 1045` ```apply (rule_tac x = N in exI, safe) ``` huffman@20552 ` 1046` ```apply (drule_tac x = n in spec) ``` huffman@20552 ` 1047` ```apply (rule order_trans [OF norm_triangle_ineq], simp) ``` paulson@15082 ` 1048` ```apply (auto simp add: Bseq_iff2) ``` paulson@15082 ` 1049` ```done ``` paulson@15082 ` 1050` huffman@20552 ` 1051` ```lemma BseqI2: "(\n. k \ f n & f n \ (K::real)) ==> Bseq f" ``` paulson@15082 ` 1052` ```apply (simp add: Bseq_def) ``` paulson@15221 ` 1053` ```apply (rule_tac x = " (\k\ + \K\) + 1" in exI, auto) ``` webertj@20217 ` 1054` ```apply (drule_tac x = n in spec, arith) ``` paulson@15082 ` 1055` ```done ``` paulson@15082 ` 1056` paulson@15082 ` 1057` huffman@20696 ` 1058` ```subsection {* Cauchy Sequences *} ``` paulson@15082 ` 1059` huffman@20751 ` 1060` ```lemma CauchyI: ``` huffman@20751 ` 1061` ``` "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" ``` huffman@20751 ` 1062` ```by (simp add: Cauchy_def) ``` huffman@20751 ` 1063` huffman@20751 ` 1064` ```lemma CauchyD: ``` huffman@20751 ` 1065` ``` "\Cauchy X; 0 < e\ \ \M. \m\M. \n\M. norm (X m - X n) < e" ``` huffman@20751 ` 1066` ```by (simp add: Cauchy_def) ``` huffman@20751 ` 1067` huffman@20696 ` 1068` ```subsubsection {* Cauchy Sequences are Bounded *} ``` huffman@20696 ` 1069` paulson@15082 ` 1070` ```text{*A Cauchy sequence is bounded -- this is the standard ``` paulson@15082 ` 1071` ``` proof mechanization rather than the nonstandard proof*} ``` paulson@15082 ` 1072` huffman@20563 ` 1073` ```lemma lemmaCauchy: "\n \ M. norm (X M - X n) < (1::real) ``` huffman@20552 ` 1074` ``` ==> \n \ M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" ``` huffman@20552 ` 1075` ```apply (clarify, drule spec, drule (1) mp) ``` huffman@20563 ` 1076` ```apply (simp only: norm_minus_commute) ``` huffman@20552 ` 1077` ```apply (drule order_le_less_trans [OF norm_triangle_ineq2]) ``` huffman@20552 ` 1078` ```apply simp ``` huffman@20552 ` 1079` ```done ``` paulson@15082 ` 1080` paulson@15082 ` 1081` ```lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" ``` huffman@20552 ` 1082` ```apply (simp add: Cauchy_def) ``` huffman@20552 ` 1083` ```apply (drule spec, drule mp, rule zero_less_one, safe) ``` huffman@20552 ` 1084` ```apply (drule_tac x="M" in spec, simp) ``` paulson@15082 ` 1085` ```apply (drule lemmaCauchy) ``` huffman@22608 ` 1086` ```apply (rule_tac k="M" in Bseq_offset) ``` huffman@20552 ` 1087` ```apply (simp add: Bseq_def) ``` huffman@20552 ` 1088` ```apply (rule_tac x="1 + norm (X M)" in exI) ``` huffman@20552 ` 1089` ```apply (rule conjI, rule order_less_le_trans [OF zero_less_one], simp) ``` huffman@20552 ` 1090` ```apply (simp add: order_less_imp_le) ``` paulson@15082 ` 1091` ```done ``` paulson@15082 ` 1092` huffman@20696 ` 1093` ```subsubsection {* Cauchy Sequences are Convergent *} ``` paulson@15082 ` 1094` huffman@20830 ` 1095` ```axclass banach \ real_normed_vector ``` huffman@20830 ` 1096` ``` Cauchy_convergent: "Cauchy X \ convergent X" ``` huffman@20830 ` 1097` huffman@22629 ` 1098` ```theorem LIMSEQ_imp_Cauchy: ``` huffman@22629 ` 1099` ``` assumes X: "X ----> a" shows "Cauchy X" ``` huffman@22629 ` 1100` ```proof (rule CauchyI) ``` huffman@22629 ` 1101` ``` fix e::real assume "0 < e" ``` huffman@22629 ` 1102` ``` hence "0 < e/2" by simp ``` huffman@22629 ` 1103` ``` with X have "\N. \n\N. norm (X n - a) < e/2" by (rule LIMSEQ_D) ``` huffman@22629 ` 1104` ``` then obtain N where N: "\n\N. norm (X n - a) < e/2" .. ``` huffman@22629 ` 1105` ``` show "\N. \m\N. \n\N. norm (X m - X n) < e" ``` huffman@22629 ` 1106` ``` proof (intro exI allI impI) ``` huffman@22629 ` 1107` ``` fix m assume "N \ m" ``` huffman@22629 ` 1108` ``` hence m: "norm (X m - a) < e/2" using N by fast ``` huffman@22629 ` 1109` ``` fix n assume "N \ n" ``` huffman@22629 ` 1110` ``` hence n: "norm (X n - a) < e/2" using N by fast ``` huffman@22629 ` 1111` ``` have "norm (X m - X n) = norm ((X m - a) - (X n - a))" by simp ``` huffman@22629 ` 1112` ``` also have "\ \ norm (X m - a) + norm (X n - a)" ``` huffman@22629 ` 1113` ``` by (rule norm_triangle_ineq4) ``` nipkow@23482 ` 1114` ``` also from m n have "\ < e" by(simp add:field_simps) ``` huffman@22629 ` 1115` ``` finally show "norm (X m - X n) < e" . ``` huffman@22629 ` 1116` ``` qed ``` huffman@22629 ` 1117` ```qed ``` huffman@22629 ` 1118` huffman@20691 ` 1119` ```lemma convergent_Cauchy: "convergent X \ Cauchy X" ``` huffman@22629 ` 1120` ```unfolding convergent_def ``` huffman@22629 ` 1121` ```by (erule exE, erule LIMSEQ_imp_Cauchy) ``` huffman@20691 ` 1122` huffman@22629 ` 1123` ```text {* ``` huffman@22629 ` 1124` ```Proof that Cauchy sequences converge based on the one from ``` huffman@22629 ` 1125` ```http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html ``` huffman@22629 ` 1126` ```*} ``` huffman@22629 ` 1127` huffman@22629 ` 1128` ```text {* ``` huffman@22629 ` 1129` ``` If sequence @{term "X"} is Cauchy, then its limit is the lub of ``` huffman@22629 ` 1130` ``` @{term "{r::real. \N. \n\N. r < X n}"} ``` huffman@22629 ` 1131` ```*} ``` huffman@22629 ` 1132` huffman@22629 ` 1133` ```lemma isUb_UNIV_I: "(\y. y \ S \ y \ u) \ isUb UNIV S u" ``` huffman@22629 ` 1134` ```by (simp add: isUbI setleI) ``` huffman@22629 ` 1135` huffman@22629 ` 1136` ```lemma real_abs_diff_less_iff: ``` huffman@22629 ` 1137` ``` "(\x - a\ < (r::real)) = (a - r < x \ x < a + r)" ``` huffman@22629 ` 1138` ```by auto ``` huffman@22629 ` 1139` haftmann@27681 ` 1140` ```locale real_Cauchy = ``` huffman@22629 ` 1141` ``` fixes X :: "nat \ real" ``` huffman@22629 ` 1142` ``` assumes X: "Cauchy X" ``` huffman@22629 ` 1143` ``` fixes S :: "real set" ``` huffman@22629 ` 1144` ``` defines S_def: "S \ {x::real. \N. \n\N. x < X n}" ``` huffman@22629 ` 1145` haftmann@27681 ` 1146` ```lemma real_CauchyI: ``` haftmann@27681 ` 1147` ``` assumes "Cauchy X" ``` haftmann@27681 ` 1148` ``` shows "real_Cauchy X" ``` haftmann@28823 ` 1149` ``` proof qed (fact assms) ``` haftmann@27681 ` 1150` huffman@22629 ` 1151` ```lemma (in real_Cauchy) mem_S: "\n\N. x < X n \ x \ S" ``` huffman@22629 ` 1152` ```by (unfold S_def, auto) ``` huffman@22629 ` 1153` huffman@22629 ` 1154` ```lemma (in real_Cauchy) bound_isUb: ``` huffman@22629 ` 1155` ``` assumes N: "\n\N. X n < x" ``` huffman@22629 ` 1156` ``` shows "isUb UNIV S x" ``` huffman@22629 ` 1157` ```proof (rule isUb_UNIV_I) ``` huffman@22629 ` 1158` ``` fix y::real assume "y \ S" ``` huffman@22629 ` 1159` ``` hence "\M. \n\M. y < X n" ``` huffman@22629 ` 1160` ``` by (simp add: S_def) ``` huffman@22629 ` 1161` ``` then obtain M where "\n\M. y < X n" .. ``` huffman@22629 ` 1162` ``` hence "y < X (max M N)" by simp ``` huffman@22629 ` 1163` ``` also have "\ < x" using N by simp ``` huffman@22629 ` 1164` ``` finally show "y \ x" ``` huffman@22629 ` 1165` ``` by (rule order_less_imp_le) ``` huffman@22629 ` 1166` ```qed ``` huffman@22629 ` 1167` huffman@22629 ` 1168` ```lemma (in real_Cauchy) isLub_ex: "\u. isLub UNIV S u" ``` huffman@22629 ` 1169` ```proof (rule reals_complete) ``` huffman@22629 ` 1170` ``` obtain N where "\m\N. \n\N. norm (X m - X n) < 1" ``` huffman@22629 ` 1171` ``` using CauchyD [OF X zero_less_one] by fast ``` huffman@22629 ` 1172` ``` hence N: "\n\N. norm (X n - X N) < 1" by simp ``` huffman@22629 ` 1173` ``` show "\x. x \ S" ``` huffman@22629 ` 1174` ``` proof ``` huffman@22629 ` 1175` ``` from N have "\n\N. X N - 1 < X n" ``` huffman@22629 ` 1176` ``` by (simp add: real_abs_diff_less_iff) ``` huffman@22629 ` 1177` ``` thus "X N - 1 \ S" by (rule mem_S) ``` huffman@22629 ` 1178` ``` qed ``` huffman@22629 ` 1179` ``` show "\u. isUb UNIV S u" ``` huffman@22629 ` 1180` ``` proof ``` huffman@22629 ` 1181` ``` from N have "\n\N. X n < X N + 1" ``` huffman@22629 ` 1182` ``` by (simp add: real_abs_diff_less_iff) ``` huffman@22629 ` 1183` ``` thus "isUb UNIV S (X N + 1)" ``` huffman@22629 ` 1184` ``` by (rule bound_isUb) ``` huffman@22629 ` 1185` ``` qed ``` huffman@22629 ` 1186` ```qed ``` huffman@22629 ` 1187` huffman@22629 ` 1188` ```lemma (in real_Cauchy) isLub_imp_LIMSEQ: ``` huffman@22629 ` 1189` ``` assumes x: "isLub UNIV S x" ``` huffman@22629 ` 1190` ``` shows "X ----> x" ``` huffman@22629 ` 1191` ```proof (rule LIMSEQ_I) ``` huffman@22629 ` 1192` ``` fix r::real assume "0 < r" ``` huffman@22629 ` 1193` ``` hence r: "0 < r/2" by simp ``` huffman@22629 ` 1194` ``` obtain N where "\n\N. \m\N. norm (X n - X m) < r/2" ``` huffman@22629 ` 1195` ``` using CauchyD [OF X r] by fast ``` huffman@22629 ` 1196` ``` hence "\n\N. norm (X n - X N) < r/2" by simp ``` huffman@22629 ` 1197` ``` hence N: "\n\N. X N - r/2 < X n \ X n < X N + r/2" ``` huffman@22629 ` 1198` ``` by (simp only: real_norm_def real_abs_diff_less_iff) ``` huffman@22629 ` 1199` huffman@22629 ` 1200` ``` from N have "\n\N. X N - r/2 < X n" by fast ``` huffman@22629 ` 1201` ``` hence "X N - r/2 \ S" by (rule mem_S) ``` nipkow@23482 ` 1202` ``` hence 1: "X N - r/2 \ x" using x isLub_isUb isUbD by fast ``` huffman@22629 ` 1203` huffman@22629 ` 1204` ``` from N have "\n\N. X n < X N + r/2" by fast ``` huffman@22629 ` 1205` ``` hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) ``` nipkow@23482 ` 1206` ``` hence 2: "x \ X N + r/2" using x isLub_le_isUb by fast ``` huffman@22629 ` 1207` huffman@22629 ` 1208` ``` show "\N. \n\N. norm (X n - x) < r" ``` huffman@22629 ` 1209` ``` proof (intro exI allI impI) ``` huffman@22629 ` 1210` ``` fix n assume n: "N \ n" ``` nipkow@23482 ` 1211` ``` from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ ``` nipkow@23482 ` 1212` ``` thus "norm (X n - x) < r" using 1 2 ``` huffman@22629 ` 1213` ``` by (simp add: real_abs_diff_less_iff) ``` huffman@22629 ` 1214` ``` qed ``` huffman@22629 ` 1215` ```qed ``` huffman@22629 ` 1216` huffman@22629 ` 1217` ```lemma (in real_Cauchy) LIMSEQ_ex: "\x. X ----> x" ``` huffman@22629 ` 1218` ```proof - ``` huffman@22629 ` 1219` ``` obtain x where "isLub UNIV S x" ``` huffman@22629 ` 1220` ``` using isLub_ex by fast ``` huffman@22629 ` 1221` ``` hence "X ----> x" ``` huffman@22629 ` 1222` ``` by (rule isLub_imp_LIMSEQ) ``` huffman@22629 ` 1223` ``` thus ?thesis .. ``` huffman@22629 ` 1224` ```qed ``` huffman@22629 ` 1225` huffman@20830 ` 1226` ```lemma real_Cauchy_convergent: ``` huffman@20830 ` 1227` ``` fixes X :: "nat \ real" ``` huffman@20830 ` 1228` ``` shows "Cauchy X \ convergent X" ``` haftmann@27681 ` 1229` ```unfolding convergent_def ``` haftmann@27681 ` 1230` ```by (rule real_Cauchy.LIMSEQ_ex) ``` haftmann@27681 ` 1231` ``` (rule real_CauchyI) ``` huffman@20830 ` 1232` huffman@20830 ` 1233` ```instance real :: banach ``` huffman@20830 ` 1234` ```by intro_classes (rule real_Cauchy_convergent) ``` huffman@20830 ` 1235` huffman@20830 ` 1236` ```lemma Cauchy_convergent_iff: ``` huffman@20830 ` 1237` ``` fixes X :: "nat \ 'a::banach" ``` huffman@20830 ` 1238` ``` shows "Cauchy X = convergent X" ``` huffman@20830 ` 1239` ```by (fast intro: Cauchy_convergent convergent_Cauchy) ``` paulson@15082 ` 1240` paulson@15082 ` 1241` huffman@20696 ` 1242` ```subsection {* Power Sequences *} ``` paulson@15082 ` 1243` paulson@15082 ` 1244` ```text{*The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term ``` paulson@15082 ` 1245` ```"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and ``` paulson@15082 ` 1246` ``` also fact that bounded and monotonic sequence converges.*} ``` paulson@15082 ` 1247` huffman@20552 ` 1248` ```lemma Bseq_realpow: "[| 0 \ (x::real); x \ 1 |] ==> Bseq (%n. x ^ n)" ``` paulson@15082 ` 1249` ```apply (simp add: Bseq_def) ``` paulson@15082 ` 1250` ```apply (rule_tac x = 1 in exI) ``` paulson@15082 ` 1251` ```apply (simp add: power_abs) ``` huffman@22974 ` 1252` ```apply (auto dest: power_mono) ``` paulson@15082 ` 1253` ```done ``` paulson@15082 ` 1254` paulson@15082 ` 1255` ```lemma monoseq_realpow: "[| 0 \ x; x \ 1 |] ==> monoseq (%n. x ^ n)" ``` paulson@15082 ` 1256` ```apply (clarify intro!: mono_SucI2) ``` paulson@15082 ` 1257` ```apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) ``` paulson@15082 ` 1258` ```done ``` paulson@15082 ` 1259` huffman@20552 ` 1260` ```lemma convergent_realpow: ``` huffman@20552 ` 1261` ``` "[| 0 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" ``` paulson@15082 ` 1262` ```by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) ``` paulson@15082 ` 1263` huffman@22628 ` 1264` ```lemma LIMSEQ_inverse_realpow_zero_lemma: ``` huffman@22628 ` 1265` ``` fixes x :: real ``` huffman@22628 ` 1266` ``` assumes x: "0 \ x" ``` huffman@22628 ` 1267` ``` shows "real n * x + 1 \ (x + 1) ^ n" ``` huffman@22628 ` 1268` ```apply (induct n) ``` huffman@22628 ` 1269` ```apply simp ``` huffman@22628 ` 1270` ```apply simp ``` huffman@22628 ` 1271` ```apply (rule order_trans) ``` huffman@22628 ` 1272` ```prefer 2 ``` huffman@22628 ` 1273` ```apply (erule mult_left_mono) ``` huffman@22628 ` 1274` ```apply (rule add_increasing [OF x], simp) ``` huffman@22628 ` 1275` ```apply (simp add: real_of_nat_Suc) ``` nipkow@23477 ` 1276` ```apply (simp add: ring_distribs) ``` huffman@22628 ` 1277` ```apply (simp add: mult_nonneg_nonneg x) ``` huffman@22628 ` 1278` ```done ``` huffman@22628 ` 1279` huffman@22628 ` 1280` ```lemma LIMSEQ_inverse_realpow_zero: ``` huffman@22628 ` 1281` ``` "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" ``` huffman@22628 ` 1282` ```proof (rule LIMSEQ_inverse_zero [rule_format]) ``` huffman@22628 ` 1283` ``` fix y :: real ``` huffman@22628 ` 1284` ``` assume x: "1 < x" ``` huffman@22628 ` 1285` ``` hence "0 < x - 1" by simp ``` huffman@22628 ` 1286` ``` hence "\y. \N::nat. y < real N * (x - 1)" ``` huffman@22628 ` 1287` ``` by (rule reals_Archimedean3) ``` huffman@22628 ` 1288` ``` hence "\N::nat. y < real N * (x - 1)" .. ``` huffman@22628 ` 1289` ``` then obtain N::nat where "y < real N * (x - 1)" .. ``` huffman@22628 ` 1290` ``` also have "\ \ real N * (x - 1) + 1" by simp ``` huffman@22628 ` 1291` ``` also have "\ \ (x - 1 + 1) ^ N" ``` huffman@22628 ` 1292` ``` by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp) ``` huffman@22628 ` 1293` ``` also have "\ = x ^ N" by simp ``` huffman@22628 ` 1294` ``` finally have "y < x ^ N" . ``` huffman@22628 ` 1295` ``` hence "\n\N. y < x ^ n" ``` huffman@22628 ` 1296` ``` apply clarify ``` huffman@22628 ` 1297` ``` apply (erule order_less_le_trans) ``` huffman@22628 ` 1298` ``` apply (erule power_increasing) ``` huffman@22628 ` 1299` ``` apply (rule order_less_imp_le [OF x]) ``` huffman@22628 ` 1300` ``` done ``` huffman@22628 ` 1301` ``` thus "\N. \n\N. y < x ^ n" .. ``` huffman@22628 ` 1302` ```qed ``` huffman@22628 ` 1303` huffman@20552 ` 1304` ```lemma LIMSEQ_realpow_zero: ``` huffman@22628 ` 1305` ``` "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" ``` huffman@22628 ` 1306` ```proof (cases) ``` huffman@22628 ` 1307` ``` assume "x = 0" ``` huffman@22628 ` 1308` ``` hence "(\n. x ^ Suc n) ----> 0" by (simp add: LIMSEQ_const) ``` huffman@22628 ` 1309` ``` thus ?thesis by (rule LIMSEQ_imp_Suc) ``` huffman@22628 ` 1310` ```next ``` huffman@22628 ` 1311` ``` assume "0 \ x" and "x \ 0" ``` huffman@22628 ` 1312` ``` hence x0: "0 < x" by simp ``` huffman@22628 ` 1313` ``` assume x1: "x < 1" ``` huffman@22628 ` 1314` ``` from x0 x1 have "1 < inverse x" ``` huffman@22628 ` 1315` ``` by (rule real_inverse_gt_one) ``` huffman@22628 ` 1316` ``` hence "(\n. inverse (inverse x ^ n)) ----> 0" ``` huffman@22628 ` 1317` ``` by (rule LIMSEQ_inverse_realpow_zero) ``` huffman@22628 ` 1318` ``` thus ?thesis by (simp add: power_inverse) ``` huffman@22628 ` 1319` ```qed ``` paulson@15082 ` 1320` huffman@20685 ` 1321` ```lemma LIMSEQ_power_zero: ``` huffman@22974 ` 1322` ``` fixes x :: "'a::{real_normed_algebra_1,recpower}" ``` huffman@20685 ` 1323` ``` shows "norm x < 1 \ (\n. x ^ n) ----> 0" ``` huffman@20685 ` 1324` ```apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) ``` huffman@22974 ` 1325` ```apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le) ``` huffman@22974 ` 1326` ```apply (simp add: power_abs norm_power_ineq) ``` huffman@20685 ` 1327` ```done ``` huffman@20685 ` 1328` huffman@20552 ` 1329` ```lemma LIMSEQ_divide_realpow_zero: ``` huffman@20552 ` 1330` ``` "1 < (x::real) ==> (%n. a / (x ^ n)) ----> 0" ``` paulson@15082 ` 1331` ```apply (cut_tac a = a and x1 = "inverse x" in ``` paulson@15082 ` 1332` ``` LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero]) ``` paulson@15082 ` 1333` ```apply (auto simp add: divide_inverse power_inverse) ``` paulson@15082 ` 1334` ```apply (simp add: inverse_eq_divide pos_divide_less_eq) ``` paulson@15082 ` 1335` ```done ``` paulson@15082 ` 1336` paulson@15102 ` 1337` ```text{*Limit of @{term "c^n"} for @{term"\c\ < 1"}*} ``` paulson@15082 ` 1338` huffman@20552 ` 1339` ```lemma LIMSEQ_rabs_realpow_zero: "\c\ < (1::real) ==> (%n. \c\ ^ n) ----> 0" ``` huffman@20685 ` 1340` ```by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) ``` paulson@15082 ` 1341` huffman@20552 ` 1342` ```lemma LIMSEQ_rabs_realpow_zero2: "\c\ < (1::real) ==> (%n. c ^ n) ----> 0" ``` paulson@15082 ` 1343` ```apply (rule LIMSEQ_rabs_zero [THEN iffD1]) ``` paulson@15082 ` 1344` ```apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) ``` paulson@15082 ` 1345` ```done ``` paulson@15082 ` 1346` paulson@10751 ` 1347` ```end ```