1423 text {* |
1423 text {* |
1424 If sequence @{term "X"} is Cauchy, then its limit is the lub of |
1424 If sequence @{term "X"} is Cauchy, then its limit is the lub of |
1425 @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} |
1425 @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} |
1426 *} |
1426 *} |
1427 |
1427 |
1428 lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" |
|
1429 by (simp add: isUbI setleI) |
|
1430 |
|
1431 lemma increasing_LIMSEQ: |
1428 lemma increasing_LIMSEQ: |
1432 fixes f :: "nat \<Rightarrow> real" |
1429 fixes f :: "nat \<Rightarrow> real" |
1433 assumes inc: "\<And>n. f n \<le> f (Suc n)" |
1430 assumes inc: "\<And>n. f n \<le> f (Suc n)" |
1434 and bdd: "\<And>n. f n \<le> l" |
1431 and bdd: "\<And>n. f n \<le> l" |
1435 and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e" |
1432 and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e" |
1452 proof - |
1449 proof - |
1453 def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
1450 def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
1454 then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto |
1451 then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto |
1455 |
1452 |
1456 { fix N x assume N: "\<forall>n\<ge>N. X n < x" |
1453 { fix N x assume N: "\<forall>n\<ge>N. X n < x" |
1457 have "isUb UNIV S x" |
|
1458 proof (rule isUb_UNIV_I) |
|
1459 fix y::real assume "y \<in> S" |
1454 fix y::real assume "y \<in> S" |
1460 hence "\<exists>M. \<forall>n\<ge>M. y < X n" |
1455 hence "\<exists>M. \<forall>n\<ge>M. y < X n" |
1461 by (simp add: S_def) |
1456 by (simp add: S_def) |
1462 then obtain M where "\<forall>n\<ge>M. y < X n" .. |
1457 then obtain M where "\<forall>n\<ge>M. y < X n" .. |
1463 hence "y < X (max M N)" by simp |
1458 hence "y < X (max M N)" by simp |
1464 also have "\<dots> < x" using N by simp |
1459 also have "\<dots> < x" using N by simp |
1465 finally show "y \<le> x" |
1460 finally have "y \<le> x" |
1466 by (rule order_less_imp_le) |
1461 by (rule order_less_imp_le) } |
1467 qed } |
|
1468 note bound_isUb = this |
1462 note bound_isUb = this |
1469 |
1463 |
1470 have "\<exists>u. isLub UNIV S u" |
|
1471 proof (rule reals_complete) |
|
1472 obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1" |
1464 obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1" |
1473 using X[THEN metric_CauchyD, OF zero_less_one] by auto |
1465 using X[THEN metric_CauchyD, OF zero_less_one] by auto |
1474 hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp |
1466 hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp |
1475 show "\<exists>x. x \<in> S" |
1467 have [simp]: "S \<noteq> {}" |
1476 proof |
1468 proof (intro exI ex_in_conv[THEN iffD1]) |
1477 from N have "\<forall>n\<ge>N. X N - 1 < X n" |
1469 from N have "\<forall>n\<ge>N. X N - 1 < X n" |
1478 by (simp add: abs_diff_less_iff dist_real_def) |
1470 by (simp add: abs_diff_less_iff dist_real_def) |
1479 thus "X N - 1 \<in> S" by (rule mem_S) |
1471 thus "X N - 1 \<in> S" by (rule mem_S) |
1480 qed |
1472 qed |
1481 show "\<exists>u. isUb UNIV S u" |
1473 have [simp]: "bdd_above S" |
1482 proof |
1474 proof |
1483 from N have "\<forall>n\<ge>N. X n < X N + 1" |
1475 from N have "\<forall>n\<ge>N. X n < X N + 1" |
1484 by (simp add: abs_diff_less_iff dist_real_def) |
1476 by (simp add: abs_diff_less_iff dist_real_def) |
1485 thus "isUb UNIV S (X N + 1)" |
1477 thus "\<And>s. s \<in> S \<Longrightarrow> s \<le> X N + 1" |
1486 by (rule bound_isUb) |
1478 by (rule bound_isUb) |
1487 qed |
1479 qed |
1488 qed |
1480 have "X ----> Sup S" |
1489 then obtain x where x: "isLub UNIV S x" .. |
|
1490 have "X ----> x" |
|
1491 proof (rule metric_LIMSEQ_I) |
1481 proof (rule metric_LIMSEQ_I) |
1492 fix r::real assume "0 < r" |
1482 fix r::real assume "0 < r" |
1493 hence r: "0 < r/2" by simp |
1483 hence r: "0 < r/2" by simp |
1494 obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. dist (X n) (X m) < r/2" |
1484 obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. dist (X n) (X m) < r/2" |
1495 using metric_CauchyD [OF X r] by auto |
1485 using metric_CauchyD [OF X r] by auto |
1497 hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2" |
1487 hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2" |
1498 by (simp only: dist_real_def abs_diff_less_iff) |
1488 by (simp only: dist_real_def abs_diff_less_iff) |
1499 |
1489 |
1500 from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast |
1490 from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast |
1501 hence "X N - r/2 \<in> S" by (rule mem_S) |
1491 hence "X N - r/2 \<in> S" by (rule mem_S) |
1502 hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast |
1492 hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper) |
1503 |
1493 |
1504 from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast |
1494 from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast |
1505 hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) |
1495 from bound_isUb[OF this] |
1506 hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast |
1496 have 2: "Sup S \<le> X N + r/2" |
1507 |
1497 by (intro cSup_least) simp_all |
1508 show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r" |
1498 |
|
1499 show "\<exists>N. \<forall>n\<ge>N. dist (X n) (Sup S) < r" |
1509 proof (intro exI allI impI) |
1500 proof (intro exI allI impI) |
1510 fix n assume n: "N \<le> n" |
1501 fix n assume n: "N \<le> n" |
1511 from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ |
1502 from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ |
1512 thus "dist (X n) x < r" using 1 2 |
1503 thus "dist (X n) (Sup S) < r" using 1 2 |
1513 by (simp add: abs_diff_less_iff dist_real_def) |
1504 by (simp add: abs_diff_less_iff dist_real_def) |
1514 qed |
1505 qed |
1515 qed |
1506 qed |
1516 then show ?thesis unfolding convergent_def by auto |
1507 then show ?thesis unfolding convergent_def by auto |
1517 qed |
1508 qed |