965 |
965 |
966 lemma Lim_at_infinity: |
966 lemma Lim_at_infinity: |
967 "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)" |
967 "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)" |
968 by (auto simp add: tendsto_iff eventually_at_infinity) |
968 by (auto simp add: tendsto_iff eventually_at_infinity) |
969 |
969 |
970 lemma Lim_sequentially: |
|
971 "(S ---> l) sequentially \<longleftrightarrow> |
|
972 (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (S n) l < e)" |
|
973 by (rule LIMSEQ_def) (* FIXME: redundant *) |
|
974 |
|
975 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net" |
970 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net" |
976 by (rule topological_tendstoI, auto elim: eventually_rev_mono) |
971 by (rule topological_tendstoI, auto elim: eventually_rev_mono) |
977 |
972 |
978 text{* The expected monotonicity property. *} |
973 text{* The expected monotonicity property. *} |
979 |
974 |
1102 by (simp add: norm_conv_dist [symmetric] less_imp_le f) |
1097 by (simp add: norm_conv_dist [symmetric] less_imp_le f) |
1103 qed |
1098 qed |
1104 ultimately show ?rhs by fast |
1099 ultimately show ?rhs by fast |
1105 next |
1100 next |
1106 assume ?rhs |
1101 assume ?rhs |
1107 then obtain f::"nat\<Rightarrow>'a" where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto |
1102 then obtain f::"nat\<Rightarrow>'a" where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding LIMSEQ_def by auto |
1108 { fix e::real assume "e>0" |
1103 { fix e::real assume "e>0" |
1109 then obtain N where "dist (f N) x < e" using f(2) by auto |
1104 then obtain N where "dist (f N) x < e" using f(2) by auto |
1110 moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto |
1105 moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto |
1111 ultimately have "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" by auto |
1106 ultimately have "\<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" by auto |
1112 } |
1107 } |
1985 apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) |
1980 apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) |
1986 apply(case_tac "m \<le> na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq) } |
1981 apply(case_tac "m \<le> na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq) } |
1987 hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto |
1982 hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto |
1988 then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar> (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] |
1983 then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar> (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] |
1989 unfolding monoseq_def by auto |
1984 unfolding monoseq_def by auto |
1990 thus ?thesis unfolding Lim_sequentially apply(rule_tac x="l" in exI) |
1985 thus ?thesis unfolding LIMSEQ_def apply(rule_tac x="l" in exI) |
1991 unfolding dist_norm by auto |
1986 unfolding dist_norm by auto |
1992 qed |
1987 qed |
1993 |
1988 |
1994 lemma compact_real_lemma: |
1989 lemma compact_real_lemma: |
1995 assumes "\<forall>n::nat. abs(s n) \<le> b" |
1990 assumes "\<forall>n::nat. abs(s n) \<le> b" |
2182 |
2177 |
2183 lemma convergent_imp_cauchy: |
2178 lemma convergent_imp_cauchy: |
2184 "(s ---> l) sequentially ==> Cauchy s" |
2179 "(s ---> l) sequentially ==> Cauchy s" |
2185 proof(simp only: cauchy_def, rule, rule) |
2180 proof(simp only: cauchy_def, rule, rule) |
2186 fix e::real assume "e>0" "(s ---> l) sequentially" |
2181 fix e::real assume "e>0" "(s ---> l) sequentially" |
2187 then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding Lim_sequentially by(erule_tac x="e/2" in allE) auto |
2182 then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding LIMSEQ_def by(erule_tac x="e/2" in allE) auto |
2188 thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e" using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto |
2183 thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e" using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto |
2189 qed |
2184 qed |
2190 |
2185 |
2191 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" |
2186 lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" |
2192 proof- |
2187 proof- |
2209 |
2204 |
2210 note lr' = subseq_bigger [OF lr(2)] |
2205 note lr' = subseq_bigger [OF lr(2)] |
2211 |
2206 |
2212 { fix e::real assume "e>0" |
2207 { fix e::real assume "e>0" |
2213 from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto |
2208 from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto |
2214 from lr(3)[unfolded Lim_sequentially, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto |
2209 from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto |
2215 { fix n::nat assume n:"n \<ge> max N M" |
2210 { fix n::nat assume n:"n \<ge> max N M" |
2216 have "dist ((f \<circ> r) n) l < e/2" using n M by auto |
2211 have "dist ((f \<circ> r) n) l < e/2" using n M by auto |
2217 moreover have "r n \<ge> N" using lr'[of n] n by auto |
2212 moreover have "r n \<ge> N" using lr'[of n] n by auto |
2218 hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto |
2213 hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto |
2219 ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) } |
2214 ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) } |
2220 hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast } |
2215 hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast } |
2221 hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding Lim_sequentially by auto } |
2216 hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto } |
2222 thus ?thesis unfolding complete_def by auto |
2217 thus ?thesis unfolding complete_def by auto |
2223 qed |
2218 qed |
2224 |
2219 |
2225 instance heine_borel < complete_space |
2220 instance heine_borel < complete_space |
2226 proof |
2221 proof |
2339 obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto |
2334 obtain b where "l\<in>b" "b\<in>t" using assms(2) and l by auto |
2340 then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b" |
2335 then obtain e where "e>0" and e:"\<forall>z. dist z l < e \<longrightarrow> z\<in>b" |
2341 using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto |
2336 using assms(3)[THEN bspec[where x=b]] unfolding open_dist by auto |
2342 |
2337 |
2343 then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2" |
2338 then obtain N1 where N1:"\<forall>n\<ge>N1. dist ((f \<circ> r) n) l < e / 2" |
2344 using lr[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto |
2339 using lr[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto |
2345 |
2340 |
2346 obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto |
2341 obtain N2::nat where N2:"N2>0" "inverse (real N2) < e /2" using real_arch_inv[of "e/2"] and `e>0` by auto |
2347 have N2':"inverse (real (r (N1 + N2) +1 )) < e/2" |
2342 have N2':"inverse (real (r (N1 + N2) +1 )) < e/2" |
2348 apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2 |
2343 apply(rule order_less_trans) apply(rule less_imp_inverse_less) using N2 |
2349 using subseq_bigger[OF r, of "N1 + N2"] by auto |
2344 using subseq_bigger[OF r, of "N1 + N2"] by auto |
2474 apply (simp_all add: r_simps) |
2469 apply (simp_all add: r_simps) |
2475 apply (rule t_less, rule zero_less_one) |
2470 apply (rule t_less, rule zero_less_one) |
2476 apply (rule t_less, rule f_r_neq) |
2471 apply (rule t_less, rule f_r_neq) |
2477 done |
2472 done |
2478 show "((f \<circ> r) ---> l) sequentially" |
2473 show "((f \<circ> r) ---> l) sequentially" |
2479 unfolding Lim_sequentially o_def |
2474 unfolding LIMSEQ_def o_def |
2480 apply (clarify, rule_tac x="t e" in exI, clarify) |
2475 apply (clarify, rename_tac e, rule_tac x="t e" in exI, clarify) |
2481 apply (drule le_trans, rule seq_suble [OF `subseq r`]) |
2476 apply (drule le_trans, rule seq_suble [OF `subseq r`]) |
2482 apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq) |
2477 apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq) |
2483 done |
2478 done |
2484 qed |
2479 qed |
2485 |
2480 |
2910 then obtain l r where lr:"l\<in>s 0" "subseq r" "((x \<circ> r) ---> l) sequentially" |
2905 then obtain l r where lr:"l\<in>s 0" "subseq r" "((x \<circ> r) ---> l) sequentially" |
2911 unfolding compact_def apply(erule_tac x=x in allE) using x using assms(3) by blast |
2906 unfolding compact_def apply(erule_tac x=x in allE) using x using assms(3) by blast |
2912 |
2907 |
2913 { fix n::nat |
2908 { fix n::nat |
2914 { fix e::real assume "e>0" |
2909 { fix e::real assume "e>0" |
2915 with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding Lim_sequentially by auto |
2910 with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto |
2916 hence "dist ((x \<circ> r) (max N n)) l < e" by auto |
2911 hence "dist ((x \<circ> r) (max N n)) l < e" by auto |
2917 moreover |
2912 moreover |
2918 have "r (max N n) \<ge> n" using lr(2) using subseq_bigger[of r "max N n"] by auto |
2913 have "r (max N n) \<ge> n" using lr(2) using subseq_bigger[of r "max N n"] by auto |
2919 hence "(x \<circ> r) (max N n) \<in> s n" |
2914 hence "(x \<circ> r) (max N n) \<in> s n" |
2920 using x apply(erule_tac x=n in allE) |
2915 using x apply(erule_tac x=n in allE) |
2949 } |
2944 } |
2950 hence "Cauchy t" unfolding cauchy_def by auto |
2945 hence "Cauchy t" unfolding cauchy_def by auto |
2951 then obtain l where l:"(t ---> l) sequentially" using complete_univ unfolding complete_def by auto |
2946 then obtain l where l:"(t ---> l) sequentially" using complete_univ unfolding complete_def by auto |
2952 { fix n::nat |
2947 { fix n::nat |
2953 { fix e::real assume "e>0" |
2948 { fix e::real assume "e>0" |
2954 then obtain N::nat where N:"\<forall>n\<ge>N. dist (t n) l < e" using l[unfolded Lim_sequentially] by auto |
2949 then obtain N::nat where N:"\<forall>n\<ge>N. dist (t n) l < e" using l[unfolded LIMSEQ_def] by auto |
2955 have "t (max n N) \<in> s n" using assms(3) unfolding subset_eq apply(erule_tac x=n in allE) apply (erule_tac x="max n N" in allE) using t by auto |
2950 have "t (max n N) \<in> s n" using assms(3) unfolding subset_eq apply(erule_tac x=n in allE) apply (erule_tac x="max n N" in allE) using t by auto |
2956 hence "\<exists>y\<in>s n. dist y l < e" apply(rule_tac x="t (max n N)" in bexI) using N by auto |
2951 hence "\<exists>y\<in>s n. dist y l < e" apply(rule_tac x="t (max n N)" in bexI) using N by auto |
2957 } |
2952 } |
2958 hence "l \<in> s n" using closed_approachable[of "s n" l] assms(1) by auto |
2953 hence "l \<in> s n" using closed_approachable[of "s n" l] assms(1) by auto |
2959 } |
2954 } |
3006 { fix e::real assume "e>0" |
3001 { fix e::real assume "e>0" |
3007 then obtain N where N:"\<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x \<longrightarrow> dist (s m x) (s n x) < e/2" |
3002 then obtain N where N:"\<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x \<longrightarrow> dist (s m x) (s n x) < e/2" |
3008 using `?rhs`[THEN spec[where x="e/2"]] by auto |
3003 using `?rhs`[THEN spec[where x="e/2"]] by auto |
3009 { fix x assume "P x" |
3004 { fix x assume "P x" |
3010 then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2" |
3005 then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2" |
3011 using l[THEN spec[where x=x], unfolded Lim_sequentially] using `e>0` by(auto elim!: allE[where x="e/2"]) |
3006 using l[THEN spec[where x=x], unfolded LIMSEQ_def] using `e>0` by(auto elim!: allE[where x="e/2"]) |
3012 fix n::nat assume "n\<ge>N" |
3007 fix n::nat assume "n\<ge>N" |
3013 hence "dist(s n x)(l x) < e" using `P x`and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]] |
3008 hence "dist(s n x)(l x) < e" using `P x`and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]] |
3014 using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"] by (auto simp add: dist_commute) } |
3009 using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"] by (auto simp add: dist_commute) } |
3015 hence "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e" by auto } |
3010 hence "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e" by auto } |
3016 thus ?lhs by auto |
3011 thus ?lhs by auto |
3025 obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e" |
3020 obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e" |
3026 using assms(1) unfolding uniformly_convergent_eq_cauchy[THEN sym] by auto |
3021 using assms(1) unfolding uniformly_convergent_eq_cauchy[THEN sym] by auto |
3027 moreover |
3022 moreover |
3028 { fix x assume "P x" |
3023 { fix x assume "P x" |
3029 hence "l x = l' x" using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"] |
3024 hence "l x = l' x" using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"] |
3030 using l and assms(2) unfolding Lim_sequentially by blast } |
3025 using l and assms(2) unfolding LIMSEQ_def by blast } |
3031 ultimately show ?thesis by auto |
3026 ultimately show ?thesis by auto |
3032 qed |
3027 qed |
3033 |
3028 |
3034 |
3029 |
3035 subsection {* Continuity *} |
3030 subsection {* Continuity *} |
3258 assume ?lhs |
3253 assume ?lhs |
3259 { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially" |
3254 { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially" |
3260 { fix e::real assume "e>0" |
3255 { fix e::real assume "e>0" |
3261 then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" |
3256 then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" |
3262 using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto |
3257 using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto |
3263 obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto |
3258 obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded LIMSEQ_def dist_norm] and `d>0` by auto |
3264 { fix n assume "n\<ge>N" |
3259 { fix n assume "n\<ge>N" |
3265 hence "dist (f (x n)) (f (y n)) < e" |
3260 hence "dist (f (x n)) (f (y n)) < e" |
3266 using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y |
3261 using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y |
3267 unfolding dist_commute by simp } |
3262 unfolding dist_commute by simp } |
3268 hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" by auto } |
3263 hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" by auto } |
3269 hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding Lim_sequentially and dist_real_def by auto } |
3264 hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding LIMSEQ_def and dist_real_def by auto } |
3270 thus ?rhs by auto |
3265 thus ?rhs by auto |
3271 next |
3266 next |
3272 assume ?rhs |
3267 assume ?rhs |
3273 { assume "\<not> ?lhs" |
3268 { assume "\<not> ?lhs" |
3274 then obtain e where "e>0" "\<forall>d>0. \<exists>x\<in>s. \<exists>x'\<in>s. dist x' x < d \<and> \<not> dist (f x') (f x) < e" unfolding uniformly_continuous_on_def by auto |
3269 then obtain e where "e>0" "\<forall>d>0. \<exists>x\<in>s. \<exists>x'\<in>s. dist x' x < d \<and> \<not> dist (f x') (f x) < e" unfolding uniformly_continuous_on_def by auto |
3285 hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto |
3280 hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto |
3286 also have "\<dots> < e" using N by auto |
3281 also have "\<dots> < e" using N by auto |
3287 finally have "inverse (real n + 1) < e" by auto |
3282 finally have "inverse (real n + 1) < e" by auto |
3288 hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto } |
3283 hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto } |
3289 hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto } |
3284 hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto } |
3290 hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially dist_real_def by auto |
3285 hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding LIMSEQ_def dist_real_def by auto |
3291 hence False using fxy and `e>0` by auto } |
3286 hence False using fxy and `e>0` by auto } |
3292 thus ?lhs unfolding uniformly_continuous_on_def by blast |
3287 thus ?lhs unfolding uniformly_continuous_on_def by blast |
3293 qed |
3288 qed |
3294 |
3289 |
3295 text{* The usual transformation theorems. *} |
3290 text{* The usual transformation theorems. *} |
3972 { fix x assume x:"\<forall>n::nat. x n \<in> f ` s" |
3967 { fix x assume x:"\<forall>n::nat. x n \<in> f ` s" |
3973 then obtain y where y:"\<forall>n. y n \<in> s \<and> x n = f (y n)" unfolding image_iff Bex_def using choice[of "\<lambda>n xa. xa \<in> s \<and> x n = f xa"] by auto |
3968 then obtain y where y:"\<forall>n. y n \<in> s \<and> x n = f (y n)" unfolding image_iff Bex_def using choice[of "\<lambda>n xa. xa \<in> s \<and> x n = f xa"] by auto |
3974 then obtain l r where "l\<in>s" and r:"subseq r" and lr:"((y \<circ> r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto |
3969 then obtain l r where "l\<in>s" and r:"subseq r" and lr:"((y \<circ> r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto |
3975 { fix e::real assume "e>0" |
3970 { fix e::real assume "e>0" |
3976 then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto |
3971 then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto |
3977 then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded Lim_sequentially, THEN spec[where x=d]] by auto |
3972 then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded LIMSEQ_def, THEN spec[where x=d]] by auto |
3978 { fix n::nat assume "n\<ge>N" hence "dist ((x \<circ> r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto } |
3973 { fix n::nat assume "n\<ge>N" hence "dist ((x \<circ> r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto } |
3979 hence "\<exists>N. \<forall>n\<ge>N. dist ((x \<circ> r) n) (f l) < e" by auto } |
3974 hence "\<exists>N. \<forall>n\<ge>N. dist ((x \<circ> r) n) (f l) < e" by auto } |
3980 hence "\<exists>l\<in>f ` s. \<exists>r. subseq r \<and> ((x \<circ> r) ---> l) sequentially" unfolding Lim_sequentially using r lr `l\<in>s` by auto } |
3975 hence "\<exists>l\<in>f ` s. \<exists>r. subseq r \<and> ((x \<circ> r) ---> l) sequentially" unfolding LIMSEQ_def using r lr `l\<in>s` by auto } |
3981 thus ?thesis unfolding compact_def by auto |
3976 thus ?thesis unfolding compact_def by auto |
3982 qed |
3977 qed |
3983 |
3978 |
3984 lemma connected_continuous_image: |
3979 lemma connected_continuous_image: |
3985 assumes "continuous_on s f" "connected s" |
3980 assumes "continuous_on s f" "connected s" |
4401 } |
4396 } |
4402 moreover |
4397 moreover |
4403 { fix e::real assume "e>0" |
4398 { fix e::real assume "e>0" |
4404 hence "0 < e *\<bar>c\<bar>" using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto |
4399 hence "0 < e *\<bar>c\<bar>" using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto |
4405 then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>" |
4400 then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>" |
4406 using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto |
4401 using as(2)[unfolded LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto |
4407 hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e" |
4402 hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e" |
4408 unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] |
4403 unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] |
4409 using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto } |
4404 using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto } |
4410 hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto |
4405 hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding LIMSEQ_def by auto |
4411 ultimately have "l \<in> scaleR c ` s" |
4406 ultimately have "l \<in> scaleR c ` s" |
4412 using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"], THEN spec[where x="scaleR (1/c) l"]] |
4407 using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"], THEN spec[where x="scaleR (1/c) l"]] |
4413 unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto } |
4408 unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto } |
4414 thus ?thesis unfolding closed_sequential_limits by fast |
4409 thus ?thesis unfolding closed_sequential_limits by fast |
4415 qed |
4410 qed |
4835 hence "\<exists>N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n - 1" in exI) by auto |
4830 hence "\<exists>N::nat. inverse (real (N + 1)) < e" using real_arch_inv[of e] apply (auto simp add: Suc_pred') apply(rule_tac x="n - 1" in exI) by auto |
4836 then obtain N::nat where "inverse (real (N + 1)) < e" by auto |
4831 then obtain N::nat where "inverse (real (N + 1)) < e" by auto |
4837 hence "\<forall>n\<ge>N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero) |
4832 hence "\<forall>n\<ge>N. inverse (real n + 1) < e" by (auto, metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans real_of_nat_Suc real_of_nat_Suc_gt_zero) |
4838 hence "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto } |
4833 hence "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto } |
4839 hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially" |
4834 hence "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially" |
4840 unfolding Lim_sequentially by(auto simp add: dist_norm) |
4835 unfolding LIMSEQ_def by(auto simp add: dist_norm) |
4841 hence "(f ---> x) sequentially" unfolding f_def |
4836 hence "(f ---> x) sequentially" unfolding f_def |
4842 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
4837 using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
4843 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } |
4838 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] by auto } |
4844 ultimately have "x \<in> closure {a<..<b}" |
4839 ultimately have "x \<in> closure {a<..<b}" |
4845 using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto } |
4840 using as and open_interval_midpoint[OF assms] unfolding closure_def unfolding islimpt_sequential by(cases "x=?c")auto } |
5732 def e \<equiv> "dist (f x) x" |
5727 def e \<equiv> "dist (f x) x" |
5733 have "e = 0" proof(rule ccontr) |
5728 have "e = 0" proof(rule ccontr) |
5734 assume "e \<noteq> 0" hence "e>0" unfolding e_def using zero_le_dist[of "f x" x] |
5729 assume "e \<noteq> 0" hence "e>0" unfolding e_def using zero_le_dist[of "f x" x] |
5735 by (metis dist_eq_0_iff dist_nz e_def) |
5730 by (metis dist_eq_0_iff dist_nz e_def) |
5736 then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2" |
5731 then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2" |
5737 using x[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto |
5732 using x[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto |
5738 hence N':"dist (z N) x < e / 2" by auto |
5733 hence N':"dist (z N) x < e / 2" by auto |
5739 |
5734 |
5740 have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2 |
5735 have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2 |
5741 using zero_le_dist[of "z N" x] and c |
5736 using zero_le_dist[of "z N" x] and c |
5742 by (metis dist_eq_0_iff dist_nz order_less_asym less_le) |
5737 by (metis dist_eq_0_iff dist_nz order_less_asym less_le) |
5829 using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this |
5824 using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this |
5830 |
5825 |
5831 { assume as:"dist a b > dist (f n x) (f n y)" |
5826 { assume as:"dist a b > dist (f n x) (f n y)" |
5832 then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2" |
5827 then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2" |
5833 and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2" |
5828 and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2" |
5834 using lima limb unfolding h_def Lim_sequentially by (fastforce simp del: less_divide_eq_number_of1) |
5829 using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_number_of1) |
5835 hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)" |
5830 hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)" |
5836 apply(erule_tac x="Na+Nb+n" in allE) |
5831 apply(erule_tac x="Na+Nb+n" in allE) |
5837 apply(erule_tac x="Na+Nb+n" in allE) apply simp |
5832 apply(erule_tac x="Na+Nb+n" in allE) apply simp |
5838 using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)" |
5833 using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)" |
5839 "-b" "- f (r (Na + Nb + n)) y"] |
5834 "-b" "- f (r (Na + Nb + n)) y"] |
5850 |
5845 |
5851 have [simp]:"a = b" proof(rule ccontr) |
5846 have [simp]:"a = b" proof(rule ccontr) |
5852 def e \<equiv> "dist a b - dist (g a) (g b)" |
5847 def e \<equiv> "dist a b - dist (g a) (g b)" |
5853 assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce |
5848 assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce |
5854 hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" |
5849 hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" |
5855 using lima limb unfolding Lim_sequentially |
5850 using lima limb unfolding LIMSEQ_def |
5856 apply (auto elim!: allE[where x="e/2"]) apply(rule_tac x="r (max N Na)" in exI) unfolding h_def by fastforce |
5851 apply (auto elim!: allE[where x="e/2"]) apply(rename_tac N N', rule_tac x="r (max N N')" in exI) unfolding h_def by fastforce |
5857 then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto |
5852 then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto |
5858 have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a" |
5853 have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a" |
5859 using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto |
5854 using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto |
5860 moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b" |
5855 moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b" |
5861 using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto |
5856 using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto |