651 lemma norm_power: |
658 lemma norm_power: |
652 fixes x :: "'a::{real_normed_div_algebra}" |
659 fixes x :: "'a::{real_normed_div_algebra}" |
653 shows "norm (x ^ n) = norm x ^ n" |
660 shows "norm (x ^ n) = norm x ^ n" |
654 by (induct n) (simp_all add: norm_mult) |
661 by (induct n) (simp_all add: norm_mult) |
655 |
662 |
|
663 |
|
664 subsection {* Metric spaces *} |
|
665 |
|
666 class metric_space = open_dist + |
|
667 assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y" |
|
668 assumes dist_triangle2: "dist x y \<le> dist x z + dist y z" |
|
669 begin |
|
670 |
|
671 lemma dist_self [simp]: "dist x x = 0" |
|
672 by simp |
|
673 |
|
674 lemma zero_le_dist [simp]: "0 \<le> dist x y" |
|
675 using dist_triangle2 [of x x y] by simp |
|
676 |
|
677 lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y" |
|
678 by (simp add: less_le) |
|
679 |
|
680 lemma dist_not_less_zero [simp]: "\<not> dist x y < 0" |
|
681 by (simp add: not_less) |
|
682 |
|
683 lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y" |
|
684 by (simp add: le_less) |
|
685 |
|
686 lemma dist_commute: "dist x y = dist y x" |
|
687 proof (rule order_antisym) |
|
688 show "dist x y \<le> dist y x" |
|
689 using dist_triangle2 [of x y x] by simp |
|
690 show "dist y x \<le> dist x y" |
|
691 using dist_triangle2 [of y x y] by simp |
|
692 qed |
|
693 |
|
694 lemma dist_triangle: "dist x z \<le> dist x y + dist y z" |
|
695 using dist_triangle2 [of x z y] by (simp add: dist_commute) |
|
696 |
|
697 lemma dist_triangle3: "dist x y \<le> dist a x + dist a y" |
|
698 using dist_triangle2 [of x y a] by (simp add: dist_commute) |
|
699 |
|
700 lemma dist_triangle_alt: |
|
701 shows "dist y z <= dist x y + dist x z" |
|
702 by (rule dist_triangle3) |
|
703 |
|
704 lemma dist_pos_lt: |
|
705 shows "x \<noteq> y ==> 0 < dist x y" |
|
706 by (simp add: zero_less_dist_iff) |
|
707 |
|
708 lemma dist_nz: |
|
709 shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y" |
|
710 by (simp add: zero_less_dist_iff) |
|
711 |
|
712 lemma dist_triangle_le: |
|
713 shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" |
|
714 by (rule order_trans [OF dist_triangle2]) |
|
715 |
|
716 lemma dist_triangle_lt: |
|
717 shows "dist x z + dist y z < e ==> dist x y < e" |
|
718 by (rule le_less_trans [OF dist_triangle2]) |
|
719 |
|
720 lemma dist_triangle_half_l: |
|
721 shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e" |
|
722 by (rule dist_triangle_lt [where z=y], simp) |
|
723 |
|
724 lemma dist_triangle_half_r: |
|
725 shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e" |
|
726 by (rule dist_triangle_half_l, simp_all add: dist_commute) |
|
727 |
|
728 subclass topological_space |
|
729 proof |
|
730 have "\<exists>e::real. 0 < e" |
|
731 by (fast intro: zero_less_one) |
|
732 then show "open UNIV" |
|
733 unfolding open_dist by simp |
|
734 next |
|
735 fix S T assume "open S" "open T" |
|
736 then show "open (S \<inter> T)" |
|
737 unfolding open_dist |
|
738 apply clarify |
|
739 apply (drule (1) bspec)+ |
|
740 apply (clarify, rename_tac r s) |
|
741 apply (rule_tac x="min r s" in exI, simp) |
|
742 done |
|
743 next |
|
744 fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
|
745 unfolding open_dist by fast |
|
746 qed |
|
747 |
|
748 lemma open_ball: "open {y. dist x y < d}" |
|
749 proof (unfold open_dist, intro ballI) |
|
750 fix y assume *: "y \<in> {y. dist x y < d}" |
|
751 then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}" |
|
752 by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt) |
|
753 qed |
|
754 |
|
755 subclass first_countable_topology |
|
756 proof |
|
757 fix x |
|
758 show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))" |
|
759 proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"]) |
|
760 fix S assume "open S" "x \<in> S" |
|
761 then obtain e where "0 < e" "{y. dist x y < e} \<subseteq> S" |
|
762 by (auto simp: open_dist subset_eq dist_commute) |
|
763 moreover |
|
764 then obtain i where "inverse (Suc i) < e" |
|
765 by (auto dest!: reals_Archimedean) |
|
766 then have "{y. dist x y < inverse (Suc i)} \<subseteq> {y. dist x y < e}" |
|
767 by auto |
|
768 ultimately show "\<exists>i. {y. dist x y < inverse (Suc i)} \<subseteq> S" |
|
769 by blast |
|
770 qed (auto intro: open_ball) |
|
771 qed |
|
772 |
|
773 end |
|
774 |
|
775 instance metric_space \<subseteq> t2_space |
|
776 proof |
|
777 fix x y :: "'a::metric_space" |
|
778 assume xy: "x \<noteq> y" |
|
779 let ?U = "{y'. dist x y' < dist x y / 2}" |
|
780 let ?V = "{x'. dist y x' < dist x y / 2}" |
|
781 have th0: "\<And>d x y z. (d x z :: real) \<le> d x y + d y z \<Longrightarrow> d y z = d z y |
|
782 \<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith |
|
783 have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}" |
|
784 using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute] |
|
785 using open_ball[of _ "dist x y / 2"] by auto |
|
786 then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}" |
|
787 by blast |
|
788 qed |
|
789 |
656 text {* Every normed vector space is a metric space. *} |
790 text {* Every normed vector space is a metric space. *} |
657 |
791 |
658 instance real_normed_vector < metric_space |
792 instance real_normed_vector < metric_space |
659 proof |
793 proof |
660 fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y" |
794 fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y" |
668 subsection {* Class instances for real numbers *} |
802 subsection {* Class instances for real numbers *} |
669 |
803 |
670 instantiation real :: real_normed_field |
804 instantiation real :: real_normed_field |
671 begin |
805 begin |
672 |
806 |
|
807 definition dist_real_def: |
|
808 "dist x y = \<bar>x - y\<bar>" |
|
809 |
|
810 definition open_real_def: |
|
811 "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
|
812 |
673 definition real_norm_def [simp]: |
813 definition real_norm_def [simp]: |
674 "norm r = \<bar>r\<bar>" |
814 "norm r = \<bar>r\<bar>" |
675 |
815 |
676 instance |
816 instance |
677 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
817 apply (intro_classes, unfold real_norm_def real_scaleR_def) |
678 apply (rule dist_real_def) |
818 apply (rule dist_real_def) |
|
819 apply (rule open_real_def) |
679 apply (simp add: sgn_real_def) |
820 apply (simp add: sgn_real_def) |
680 apply (rule abs_eq_0) |
821 apply (rule abs_eq_0) |
681 apply (rule abs_triangle_ineq) |
822 apply (rule abs_triangle_ineq) |
682 apply (rule abs_mult) |
823 apply (rule abs_mult) |
683 apply (rule abs_mult) |
824 apply (rule abs_mult) |
684 done |
825 done |
685 |
826 |
686 end |
827 end |
687 |
828 |
|
829 instance real :: linorder_topology |
|
830 proof |
|
831 show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)" |
|
832 proof (rule ext, safe) |
|
833 fix S :: "real set" assume "open S" |
|
834 then guess f unfolding open_real_def bchoice_iff .. |
|
835 then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})" |
|
836 by (fastforce simp: dist_real_def) |
|
837 show "generate_topology (range lessThan \<union> range greaterThan) S" |
|
838 apply (subst *) |
|
839 apply (intro generate_topology_Union generate_topology.Int) |
|
840 apply (auto intro: generate_topology.Basis) |
|
841 done |
|
842 next |
|
843 fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S" |
|
844 moreover have "\<And>a::real. open {..<a}" |
|
845 unfolding open_real_def dist_real_def |
|
846 proof clarify |
|
847 fix x a :: real assume "x < a" |
|
848 hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto |
|
849 thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" .. |
|
850 qed |
|
851 moreover have "\<And>a::real. open {a <..}" |
|
852 unfolding open_real_def dist_real_def |
|
853 proof clarify |
|
854 fix x a :: real assume "a < x" |
|
855 hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto |
|
856 thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" .. |
|
857 qed |
|
858 ultimately show "open S" |
|
859 by induct auto |
|
860 qed |
|
861 qed |
|
862 |
688 instance real :: linear_continuum_topology .. |
863 instance real :: linear_continuum_topology .. |
|
864 |
|
865 lemmas open_real_greaterThan = open_greaterThan[where 'a=real] |
|
866 lemmas open_real_lessThan = open_lessThan[where 'a=real] |
|
867 lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real] |
|
868 lemmas closed_real_atMost = closed_atMost[where 'a=real] |
|
869 lemmas closed_real_atLeast = closed_atLeast[where 'a=real] |
|
870 lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real] |
689 |
871 |
690 subsection {* Extra type constraints *} |
872 subsection {* Extra type constraints *} |
691 |
873 |
692 text {* Only allow @{term "open"} in class @{text topological_space}. *} |
874 text {* Only allow @{term "open"} in class @{text topological_space}. *} |
693 |
875 |
917 show "\<not> open {x}" |
1099 show "\<not> open {x}" |
918 unfolding open_dist dist_norm |
1100 unfolding open_dist dist_norm |
919 by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp) |
1101 by (clarsimp, rule_tac x="x + of_real (e/2)" in exI, simp) |
920 qed |
1102 qed |
921 |
1103 |
|
1104 subsection {* Filters and Limits on Metric Space *} |
|
1105 |
|
1106 lemma eventually_nhds_metric: |
|
1107 fixes a :: "'a :: metric_space" |
|
1108 shows "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)" |
|
1109 unfolding eventually_nhds open_dist |
|
1110 apply safe |
|
1111 apply fast |
|
1112 apply (rule_tac x="{x. dist x a < d}" in exI, simp) |
|
1113 apply clarsimp |
|
1114 apply (rule_tac x="d - dist x a" in exI, clarsimp) |
|
1115 apply (simp only: less_diff_eq) |
|
1116 apply (erule le_less_trans [OF dist_triangle]) |
|
1117 done |
|
1118 |
|
1119 lemma eventually_at: |
|
1120 fixes a :: "'a::metric_space" |
|
1121 shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)" |
|
1122 unfolding at_def eventually_within eventually_nhds_metric by auto |
|
1123 |
|
1124 lemma eventually_within_less: |
|
1125 fixes a :: "'a :: metric_space" |
|
1126 shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)" |
|
1127 unfolding eventually_within eventually_at dist_nz by auto |
|
1128 |
|
1129 lemma eventually_within_le: |
|
1130 fixes a :: "'a :: metric_space" |
|
1131 shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> P x)" |
|
1132 unfolding eventually_within_less by auto (metis dense order_le_less_trans) |
|
1133 |
|
1134 lemma tendstoI: |
|
1135 fixes l :: "'a :: metric_space" |
|
1136 assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F" |
|
1137 shows "(f ---> l) F" |
|
1138 apply (rule topological_tendstoI) |
|
1139 apply (simp add: open_dist) |
|
1140 apply (drule (1) bspec, clarify) |
|
1141 apply (drule assms) |
|
1142 apply (erule eventually_elim1, simp) |
|
1143 done |
|
1144 |
|
1145 lemma tendstoD: |
|
1146 fixes l :: "'a :: metric_space" |
|
1147 shows "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F" |
|
1148 apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) |
|
1149 apply (clarsimp simp add: open_dist) |
|
1150 apply (rule_tac x="e - dist x l" in exI, clarsimp) |
|
1151 apply (simp only: less_diff_eq) |
|
1152 apply (erule le_less_trans [OF dist_triangle]) |
|
1153 apply simp |
|
1154 apply simp |
|
1155 done |
|
1156 |
|
1157 lemma tendsto_iff: |
|
1158 fixes l :: "'a :: metric_space" |
|
1159 shows "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)" |
|
1160 using tendstoI tendstoD by fast |
|
1161 |
|
1162 lemma metric_tendsto_imp_tendsto: |
|
1163 fixes a :: "'a :: metric_space" and b :: "'b :: metric_space" |
|
1164 assumes f: "(f ---> a) F" |
|
1165 assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F" |
|
1166 shows "(g ---> b) F" |
|
1167 proof (rule tendstoI) |
|
1168 fix e :: real assume "0 < e" |
|
1169 with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD) |
|
1170 with le show "eventually (\<lambda>x. dist (g x) b < e) F" |
|
1171 using le_less_trans by (rule eventually_elim2) |
|
1172 qed |
|
1173 |
|
1174 lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top" |
|
1175 unfolding filterlim_at_top |
|
1176 apply (intro allI) |
|
1177 apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI) |
|
1178 apply (auto simp: natceiling_le_eq) |
|
1179 done |
|
1180 |
|
1181 subsubsection {* Limits of Sequences *} |
|
1182 |
|
1183 lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)" |
|
1184 unfolding tendsto_iff eventually_sequentially .. |
|
1185 |
|
1186 lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)" |
|
1187 unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc) |
|
1188 |
|
1189 lemma metric_LIMSEQ_I: |
|
1190 "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)" |
|
1191 by (simp add: LIMSEQ_def) |
|
1192 |
|
1193 lemma metric_LIMSEQ_D: |
|
1194 "\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r" |
|
1195 by (simp add: LIMSEQ_def) |
|
1196 |
|
1197 |
|
1198 subsubsection {* Limits of Functions *} |
|
1199 |
|
1200 lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) = |
|
1201 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s |
|
1202 --> dist (f x) L < r)" |
|
1203 unfolding tendsto_iff eventually_at .. |
|
1204 |
|
1205 lemma metric_LIM_I: |
|
1206 "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r) |
|
1207 \<Longrightarrow> f -- (a::'a::metric_space) --> (L::'b::metric_space)" |
|
1208 by (simp add: LIM_def) |
|
1209 |
|
1210 lemma metric_LIM_D: |
|
1211 "\<lbrakk>f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\<rbrakk> |
|
1212 \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r" |
|
1213 by (simp add: LIM_def) |
|
1214 |
|
1215 lemma metric_LIM_imp_LIM: |
|
1216 assumes f: "f -- a --> (l::'a::metric_space)" |
|
1217 assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l" |
|
1218 shows "g -- a --> (m::'b::metric_space)" |
|
1219 by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le) |
|
1220 |
|
1221 lemma metric_LIM_equal2: |
|
1222 assumes 1: "0 < R" |
|
1223 assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x" |
|
1224 shows "g -- a --> l \<Longrightarrow> f -- (a::'a::metric_space) --> l" |
|
1225 apply (rule topological_tendstoI) |
|
1226 apply (drule (2) topological_tendstoD) |
|
1227 apply (simp add: eventually_at, safe) |
|
1228 apply (rule_tac x="min d R" in exI, safe) |
|
1229 apply (simp add: 1) |
|
1230 apply (simp add: 2) |
|
1231 done |
|
1232 |
|
1233 lemma metric_LIM_compose2: |
|
1234 assumes f: "f -- (a::'a::metric_space) --> b" |
|
1235 assumes g: "g -- b --> c" |
|
1236 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b" |
|
1237 shows "(\<lambda>x. g (f x)) -- a --> c" |
|
1238 using g f inj [folded eventually_at] |
|
1239 by (rule tendsto_compose_eventually) |
|
1240 |
|
1241 lemma metric_isCont_LIM_compose2: |
|
1242 fixes f :: "'a :: metric_space \<Rightarrow> _" |
|
1243 assumes f [unfolded isCont_def]: "isCont f a" |
|
1244 assumes g: "g -- f a --> l" |
|
1245 assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a" |
|
1246 shows "(\<lambda>x. g (f x)) -- a --> l" |
|
1247 by (rule metric_LIM_compose2 [OF f g inj]) |
|
1248 |
|
1249 subsection {* Complete metric spaces *} |
|
1250 |
|
1251 subsection {* Cauchy sequences *} |
|
1252 |
|
1253 definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where |
|
1254 "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)" |
|
1255 |
|
1256 subsection {* Cauchy Sequences *} |
|
1257 |
|
1258 lemma metric_CauchyI: |
|
1259 "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X" |
|
1260 by (simp add: Cauchy_def) |
|
1261 |
|
1262 lemma metric_CauchyD: |
|
1263 "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e" |
|
1264 by (simp add: Cauchy_def) |
|
1265 |
|
1266 lemma metric_Cauchy_iff2: |
|
1267 "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))" |
|
1268 apply (simp add: Cauchy_def, auto) |
|
1269 apply (drule reals_Archimedean, safe) |
|
1270 apply (drule_tac x = n in spec, auto) |
|
1271 apply (rule_tac x = M in exI, auto) |
|
1272 apply (drule_tac x = m in spec, simp) |
|
1273 apply (drule_tac x = na in spec, auto) |
|
1274 done |
|
1275 |
|
1276 lemma Cauchy_iff2: |
|
1277 "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))" |
|
1278 unfolding metric_Cauchy_iff2 dist_real_def .. |
|
1279 |
|
1280 lemma Cauchy_subseq_Cauchy: |
|
1281 "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)" |
|
1282 apply (auto simp add: Cauchy_def) |
|
1283 apply (drule_tac x=e in spec, clarify) |
|
1284 apply (rule_tac x=M in exI, clarify) |
|
1285 apply (blast intro: le_trans [OF _ seq_suble] dest!: spec) |
|
1286 done |
|
1287 |
|
1288 theorem LIMSEQ_imp_Cauchy: |
|
1289 assumes X: "X ----> a" shows "Cauchy X" |
|
1290 proof (rule metric_CauchyI) |
|
1291 fix e::real assume "0 < e" |
|
1292 hence "0 < e/2" by simp |
|
1293 with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D) |
|
1294 then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" .. |
|
1295 show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e" |
|
1296 proof (intro exI allI impI) |
|
1297 fix m assume "N \<le> m" |
|
1298 hence m: "dist (X m) a < e/2" using N by fast |
|
1299 fix n assume "N \<le> n" |
|
1300 hence n: "dist (X n) a < e/2" using N by fast |
|
1301 have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a" |
|
1302 by (rule dist_triangle2) |
|
1303 also from m n have "\<dots> < e" by simp |
|
1304 finally show "dist (X m) (X n) < e" . |
|
1305 qed |
|
1306 qed |
|
1307 |
|
1308 lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X" |
|
1309 unfolding convergent_def |
|
1310 by (erule exE, erule LIMSEQ_imp_Cauchy) |
|
1311 |
|
1312 subsubsection {* Cauchy Sequences are Convergent *} |
|
1313 |
|
1314 class complete_space = metric_space + |
|
1315 assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X" |
|
1316 |
|
1317 lemma Cauchy_convergent_iff: |
|
1318 fixes X :: "nat \<Rightarrow> 'a::complete_space" |
|
1319 shows "Cauchy X = convergent X" |
|
1320 by (fast intro: Cauchy_convergent convergent_Cauchy) |
|
1321 |
|
1322 subsection {* The set of real numbers is a complete metric space *} |
|
1323 |
|
1324 text {* |
|
1325 Proof that Cauchy sequences converge based on the one from |
|
1326 http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html |
|
1327 *} |
|
1328 |
|
1329 text {* |
|
1330 If sequence @{term "X"} is Cauchy, then its limit is the lub of |
|
1331 @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"} |
|
1332 *} |
|
1333 |
|
1334 lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u" |
|
1335 by (simp add: isUbI setleI) |
|
1336 |
|
1337 lemma increasing_LIMSEQ: |
|
1338 fixes f :: "nat \<Rightarrow> real" |
|
1339 assumes inc: "\<And>n. f n \<le> f (Suc n)" |
|
1340 and bdd: "\<And>n. f n \<le> l" |
|
1341 and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e" |
|
1342 shows "f ----> l" |
|
1343 proof (rule increasing_tendsto) |
|
1344 fix x assume "x < l" |
|
1345 with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x" |
|
1346 by auto |
|
1347 from en[OF `0 < e`] obtain n where "l - e \<le> f n" |
|
1348 by (auto simp: field_simps) |
|
1349 with `e < l - x` `0 < e` have "x < f n" by simp |
|
1350 with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially" |
|
1351 by (auto simp: eventually_sequentially incseq_def intro: less_le_trans) |
|
1352 qed (insert bdd, auto) |
|
1353 |
|
1354 lemma real_Cauchy_convergent: |
|
1355 fixes X :: "nat \<Rightarrow> real" |
|
1356 assumes X: "Cauchy X" |
|
1357 shows "convergent X" |
|
1358 proof - |
|
1359 def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}" |
|
1360 then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto |
|
1361 |
|
1362 { fix N x assume N: "\<forall>n\<ge>N. X n < x" |
|
1363 have "isUb UNIV S x" |
|
1364 proof (rule isUb_UNIV_I) |
|
1365 fix y::real assume "y \<in> S" |
|
1366 hence "\<exists>M. \<forall>n\<ge>M. y < X n" |
|
1367 by (simp add: S_def) |
|
1368 then obtain M where "\<forall>n\<ge>M. y < X n" .. |
|
1369 hence "y < X (max M N)" by simp |
|
1370 also have "\<dots> < x" using N by simp |
|
1371 finally show "y \<le> x" |
|
1372 by (rule order_less_imp_le) |
|
1373 qed } |
|
1374 note bound_isUb = this |
|
1375 |
|
1376 have "\<exists>u. isLub UNIV S u" |
|
1377 proof (rule reals_complete) |
|
1378 obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1" |
|
1379 using X[THEN metric_CauchyD, OF zero_less_one] by auto |
|
1380 hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp |
|
1381 show "\<exists>x. x \<in> S" |
|
1382 proof |
|
1383 from N have "\<forall>n\<ge>N. X N - 1 < X n" |
|
1384 by (simp add: abs_diff_less_iff dist_real_def) |
|
1385 thus "X N - 1 \<in> S" by (rule mem_S) |
|
1386 qed |
|
1387 show "\<exists>u. isUb UNIV S u" |
|
1388 proof |
|
1389 from N have "\<forall>n\<ge>N. X n < X N + 1" |
|
1390 by (simp add: abs_diff_less_iff dist_real_def) |
|
1391 thus "isUb UNIV S (X N + 1)" |
|
1392 by (rule bound_isUb) |
|
1393 qed |
|
1394 qed |
|
1395 then obtain x where x: "isLub UNIV S x" .. |
|
1396 have "X ----> x" |
|
1397 proof (rule metric_LIMSEQ_I) |
|
1398 fix r::real assume "0 < r" |
|
1399 hence r: "0 < r/2" by simp |
|
1400 obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. dist (X n) (X m) < r/2" |
|
1401 using metric_CauchyD [OF X r] by auto |
|
1402 hence "\<forall>n\<ge>N. dist (X n) (X N) < r/2" by simp |
|
1403 hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2" |
|
1404 by (simp only: dist_real_def abs_diff_less_iff) |
|
1405 |
|
1406 from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast |
|
1407 hence "X N - r/2 \<in> S" by (rule mem_S) |
|
1408 hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast |
|
1409 |
|
1410 from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast |
|
1411 hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb) |
|
1412 hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast |
|
1413 |
|
1414 show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r" |
|
1415 proof (intro exI allI impI) |
|
1416 fix n assume n: "N \<le> n" |
|
1417 from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+ |
|
1418 thus "dist (X n) x < r" using 1 2 |
|
1419 by (simp add: abs_diff_less_iff dist_real_def) |
|
1420 qed |
|
1421 qed |
|
1422 then show ?thesis unfolding convergent_def by auto |
|
1423 qed |
|
1424 |
|
1425 instance real :: complete_space |
|
1426 by intro_classes (rule real_Cauchy_convergent) |
|
1427 |
|
1428 class banach = real_normed_vector + complete_space |
|
1429 |
|
1430 instance real :: banach by default |
|
1431 |
|
1432 lemma tendsto_at_topI_sequentially: |
|
1433 fixes f :: "real \<Rightarrow> real" |
|
1434 assumes mono: "mono f" |
|
1435 assumes limseq: "(\<lambda>n. f (real n)) ----> y" |
|
1436 shows "(f ---> y) at_top" |
|
1437 proof (rule tendstoI) |
|
1438 fix e :: real assume "0 < e" |
|
1439 with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e" |
|
1440 by (auto simp: LIMSEQ_def dist_real_def) |
|
1441 { fix x :: real |
|
1442 from ex_le_of_nat[of x] guess n .. |
|
1443 note monoD[OF mono this] |
|
1444 also have "f (real_of_nat n) \<le> y" |
|
1445 by (rule LIMSEQ_le_const[OF limseq]) |
|
1446 (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric]) |
|
1447 finally have "f x \<le> y" . } |
|
1448 note le = this |
|
1449 have "eventually (\<lambda>x. real N \<le> x) at_top" |
|
1450 by (rule eventually_ge_at_top) |
|
1451 then show "eventually (\<lambda>x. dist (f x) y < e) at_top" |
|
1452 proof eventually_elim |
|
1453 fix x assume N': "real N \<le> x" |
|
1454 with N[of N] le have "y - f (real N) < e" by auto |
|
1455 moreover note monoD[OF mono N'] |
|
1456 ultimately show "dist (f x) y < e" |
|
1457 using le[of x] by (auto simp: dist_real_def field_simps) |
|
1458 qed |
|
1459 qed |
|
1460 |
922 end |
1461 end |