46 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |
46 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |
47 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
47 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
48 |
48 |
49 lemma Lim_within_open: |
49 lemma Lim_within_open: |
50 fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" |
50 fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space" |
51 shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" |
51 shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l)(at a)" |
52 by (fact tendsto_within_open) |
52 by (fact tendsto_within_open) |
53 |
53 |
54 lemma continuous_on_union: |
54 lemma continuous_on_union: |
55 "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f" |
55 "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f" |
56 by (fact continuous_on_closed_Un) |
56 by (fact continuous_on_closed_Un) |
2291 |
2291 |
2292 |
2292 |
2293 subsection \<open>Limits\<close> |
2293 subsection \<open>Limits\<close> |
2294 |
2294 |
2295 lemma Lim: |
2295 lemma Lim: |
2296 "(f ---> l) net \<longleftrightarrow> |
2296 "(f \<longlongrightarrow> l) net \<longleftrightarrow> |
2297 trivial_limit net \<or> |
2297 trivial_limit net \<or> |
2298 (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
2298 (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)" |
2299 unfolding tendsto_iff trivial_limit_eq by auto |
2299 unfolding tendsto_iff trivial_limit_eq by auto |
2300 |
2300 |
2301 text\<open>Show that they yield usual definitions in the various cases.\<close> |
2301 text\<open>Show that they yield usual definitions in the various cases.\<close> |
2302 |
2302 |
2303 lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow> |
2303 lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow> |
2304 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)" |
2304 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)" |
2305 by (auto simp add: tendsto_iff eventually_at_le dist_nz) |
2305 by (auto simp add: tendsto_iff eventually_at_le dist_nz) |
2306 |
2306 |
2307 lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow> |
2307 lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> |
2308 (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2308 (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2309 by (auto simp add: tendsto_iff eventually_at dist_nz) |
2309 by (auto simp add: tendsto_iff eventually_at dist_nz) |
2310 |
2310 |
2311 lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow> |
2311 lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow> |
2312 (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2312 (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)" |
2313 by (auto simp add: tendsto_iff eventually_at2) |
2313 by (auto simp add: tendsto_iff eventually_at2) |
2314 |
2314 |
2315 lemma Lim_at_infinity: |
2315 lemma Lim_at_infinity: |
2316 "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)" |
2316 "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)" |
2317 by (auto simp add: tendsto_iff eventually_at_infinity) |
2317 by (auto simp add: tendsto_iff eventually_at_infinity) |
2318 |
2318 |
2319 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net" |
2319 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net" |
2320 by (rule topological_tendstoI, auto elim: eventually_mono) |
2320 by (rule topological_tendstoI, auto elim: eventually_mono) |
2321 |
2321 |
2322 text\<open>The expected monotonicity property.\<close> |
2322 text\<open>The expected monotonicity property.\<close> |
2323 |
2323 |
2324 lemma Lim_Un: |
2324 lemma Lim_Un: |
2325 assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)" |
2325 assumes "(f \<longlongrightarrow> l) (at x within S)" "(f \<longlongrightarrow> l) (at x within T)" |
2326 shows "(f ---> l) (at x within (S \<union> T))" |
2326 shows "(f \<longlongrightarrow> l) (at x within (S \<union> T))" |
2327 using assms unfolding at_within_union by (rule filterlim_sup) |
2327 using assms unfolding at_within_union by (rule filterlim_sup) |
2328 |
2328 |
2329 lemma Lim_Un_univ: |
2329 lemma Lim_Un_univ: |
2330 "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow> |
2330 "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T) \<Longrightarrow> |
2331 S \<union> T = UNIV \<Longrightarrow> (f ---> l) (at x)" |
2331 S \<union> T = UNIV \<Longrightarrow> (f \<longlongrightarrow> l) (at x)" |
2332 by (metis Lim_Un) |
2332 by (metis Lim_Un) |
2333 |
2333 |
2334 text\<open>Interrelations between restricted and unrestricted limits.\<close> |
2334 text\<open>Interrelations between restricted and unrestricted limits.\<close> |
2335 |
2335 |
2336 lemma Lim_at_imp_Lim_at_within: |
2336 lemma Lim_at_imp_Lim_at_within: |
2337 "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)" |
2337 "(f \<longlongrightarrow> l) (at x) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S)" |
2338 by (metis order_refl filterlim_mono subset_UNIV at_le) |
2338 by (metis order_refl filterlim_mono subset_UNIV at_le) |
2339 |
2339 |
2340 lemma eventually_within_interior: |
2340 lemma eventually_within_interior: |
2341 assumes "x \<in> interior S" |
2341 assumes "x \<in> interior S" |
2342 shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" |
2342 shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" |
2364 unfolding filter_eq_iff by (intro allI eventually_within_interior) |
2364 unfolding filter_eq_iff by (intro allI eventually_within_interior) |
2365 |
2365 |
2366 lemma Lim_within_LIMSEQ: |
2366 lemma Lim_within_LIMSEQ: |
2367 fixes a :: "'a::first_countable_topology" |
2367 fixes a :: "'a::first_countable_topology" |
2368 assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L" |
2368 assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L" |
2369 shows "(X ---> L) (at a within T)" |
2369 shows "(X \<longlongrightarrow> L) (at a within T)" |
2370 using assms unfolding tendsto_def [where l=L] |
2370 using assms unfolding tendsto_def [where l=L] |
2371 by (simp add: sequentially_imp_eventually_within) |
2371 by (simp add: sequentially_imp_eventually_within) |
2372 |
2372 |
2373 lemma Lim_right_bound: |
2373 lemma Lim_right_bound: |
2374 fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow> |
2374 fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow> |
2375 'b::{linorder_topology, conditionally_complete_linorder}" |
2375 'b::{linorder_topology, conditionally_complete_linorder}" |
2376 assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" |
2376 assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" |
2377 and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a" |
2377 and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a" |
2378 shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))" |
2378 shows "(f \<longlongrightarrow> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))" |
2379 proof (cases "{x<..} \<inter> I = {}") |
2379 proof (cases "{x<..} \<inter> I = {}") |
2380 case True |
2380 case True |
2381 then show ?thesis by simp |
2381 then show ?thesis by simp |
2382 next |
2382 next |
2383 case False |
2383 case False |
2454 qed |
2454 qed |
2455 qed |
2455 qed |
2456 |
2456 |
2457 lemma Lim_null: |
2457 lemma Lim_null: |
2458 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2458 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2459 shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" |
2459 shows "(f \<longlongrightarrow> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) \<longlongrightarrow> 0) net" |
2460 by (simp add: Lim dist_norm) |
2460 by (simp add: Lim dist_norm) |
2461 |
2461 |
2462 lemma Lim_null_comparison: |
2462 lemma Lim_null_comparison: |
2463 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2463 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2464 assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g ---> 0) net" |
2464 assumes "eventually (\<lambda>x. norm (f x) \<le> g x) net" "(g \<longlongrightarrow> 0) net" |
2465 shows "(f ---> 0) net" |
2465 shows "(f \<longlongrightarrow> 0) net" |
2466 using assms(2) |
2466 using assms(2) |
2467 proof (rule metric_tendsto_imp_tendsto) |
2467 proof (rule metric_tendsto_imp_tendsto) |
2468 show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net" |
2468 show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net" |
2469 using assms(1) by (rule eventually_mono) (simp add: dist_norm) |
2469 using assms(1) by (rule eventually_mono) (simp add: dist_norm) |
2470 qed |
2470 qed |
2471 |
2471 |
2472 lemma Lim_transform_bound: |
2472 lemma Lim_transform_bound: |
2473 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2473 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2474 and g :: "'a \<Rightarrow> 'c::real_normed_vector" |
2474 and g :: "'a \<Rightarrow> 'c::real_normed_vector" |
2475 assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) net" |
2475 assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) net" |
2476 and "(g ---> 0) net" |
2476 and "(g \<longlongrightarrow> 0) net" |
2477 shows "(f ---> 0) net" |
2477 shows "(f \<longlongrightarrow> 0) net" |
2478 using assms(1) tendsto_norm_zero [OF assms(2)] |
2478 using assms(1) tendsto_norm_zero [OF assms(2)] |
2479 by (rule Lim_null_comparison) |
2479 by (rule Lim_null_comparison) |
2480 |
2480 |
2481 text\<open>Deducing things about the limit from the elements.\<close> |
2481 text\<open>Deducing things about the limit from the elements.\<close> |
2482 |
2482 |
2483 lemma Lim_in_closed_set: |
2483 lemma Lim_in_closed_set: |
2484 assumes "closed S" |
2484 assumes "closed S" |
2485 and "eventually (\<lambda>x. f(x) \<in> S) net" |
2485 and "eventually (\<lambda>x. f(x) \<in> S) net" |
2486 and "\<not> trivial_limit net" "(f ---> l) net" |
2486 and "\<not> trivial_limit net" "(f \<longlongrightarrow> l) net" |
2487 shows "l \<in> S" |
2487 shows "l \<in> S" |
2488 proof (rule ccontr) |
2488 proof (rule ccontr) |
2489 assume "l \<notin> S" |
2489 assume "l \<notin> S" |
2490 with \<open>closed S\<close> have "open (- S)" "l \<in> - S" |
2490 with \<open>closed S\<close> have "open (- S)" "l \<in> - S" |
2491 by (simp_all add: open_Compl) |
2491 by (simp_all add: open_Compl) |
2499 |
2499 |
2500 text\<open>Need to prove closed(cball(x,e)) before deducing this as a corollary.\<close> |
2500 text\<open>Need to prove closed(cball(x,e)) before deducing this as a corollary.\<close> |
2501 |
2501 |
2502 lemma Lim_dist_ubound: |
2502 lemma Lim_dist_ubound: |
2503 assumes "\<not>(trivial_limit net)" |
2503 assumes "\<not>(trivial_limit net)" |
2504 and "(f ---> l) net" |
2504 and "(f \<longlongrightarrow> l) net" |
2505 and "eventually (\<lambda>x. dist a (f x) \<le> e) net" |
2505 and "eventually (\<lambda>x. dist a (f x) \<le> e) net" |
2506 shows "dist a l \<le> e" |
2506 shows "dist a l \<le> e" |
2507 using assms by (fast intro: tendsto_le tendsto_intros) |
2507 using assms by (fast intro: tendsto_le tendsto_intros) |
2508 |
2508 |
2509 lemma Lim_norm_ubound: |
2509 lemma Lim_norm_ubound: |
2510 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2510 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2511 assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net" |
2511 assumes "\<not>(trivial_limit net)" "(f \<longlongrightarrow> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net" |
2512 shows "norm(l) \<le> e" |
2512 shows "norm(l) \<le> e" |
2513 using assms by (fast intro: tendsto_le tendsto_intros) |
2513 using assms by (fast intro: tendsto_le tendsto_intros) |
2514 |
2514 |
2515 lemma Lim_norm_lbound: |
2515 lemma Lim_norm_lbound: |
2516 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2516 fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" |
2517 assumes "\<not> trivial_limit net" |
2517 assumes "\<not> trivial_limit net" |
2518 and "(f ---> l) net" |
2518 and "(f \<longlongrightarrow> l) net" |
2519 and "eventually (\<lambda>x. e \<le> norm (f x)) net" |
2519 and "eventually (\<lambda>x. e \<le> norm (f x)) net" |
2520 shows "e \<le> norm l" |
2520 shows "e \<le> norm l" |
2521 using assms by (fast intro: tendsto_le tendsto_intros) |
2521 using assms by (fast intro: tendsto_le tendsto_intros) |
2522 |
2522 |
2523 text\<open>Limit under bilinear function\<close> |
2523 text\<open>Limit under bilinear function\<close> |
2524 |
2524 |
2525 lemma Lim_bilinear: |
2525 lemma Lim_bilinear: |
2526 assumes "(f ---> l) net" |
2526 assumes "(f \<longlongrightarrow> l) net" |
2527 and "(g ---> m) net" |
2527 and "(g \<longlongrightarrow> m) net" |
2528 and "bounded_bilinear h" |
2528 and "bounded_bilinear h" |
2529 shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net" |
2529 shows "((\<lambda>x. h (f x) (g x)) \<longlongrightarrow> (h l m)) net" |
2530 using \<open>bounded_bilinear h\<close> \<open>(f ---> l) net\<close> \<open>(g ---> m) net\<close> |
2530 using \<open>bounded_bilinear h\<close> \<open>(f \<longlongrightarrow> l) net\<close> \<open>(g \<longlongrightarrow> m) net\<close> |
2531 by (rule bounded_bilinear.tendsto) |
2531 by (rule bounded_bilinear.tendsto) |
2532 |
2532 |
2533 text\<open>These are special for limits out of the same vector space.\<close> |
2533 text\<open>These are special for limits out of the same vector space.\<close> |
2534 |
2534 |
2535 lemma Lim_within_id: "(id ---> a) (at a within s)" |
2535 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)" |
2536 unfolding id_def by (rule tendsto_ident_at) |
2536 unfolding id_def by (rule tendsto_ident_at) |
2537 |
2537 |
2538 lemma Lim_at_id: "(id ---> a) (at a)" |
2538 lemma Lim_at_id: "(id \<longlongrightarrow> a) (at a)" |
2539 unfolding id_def by (rule tendsto_ident_at) |
2539 unfolding id_def by (rule tendsto_ident_at) |
2540 |
2540 |
2541 lemma Lim_at_zero: |
2541 lemma Lim_at_zero: |
2542 fixes a :: "'a::real_normed_vector" |
2542 fixes a :: "'a::real_normed_vector" |
2543 and l :: "'b::topological_space" |
2543 and l :: "'b::topological_space" |
2544 shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" |
2544 shows "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) \<longlongrightarrow> l) (at 0)" |
2545 using LIM_offset_zero LIM_offset_zero_cancel .. |
2545 using LIM_offset_zero LIM_offset_zero_cancel .. |
2546 |
2546 |
2547 text\<open>It's also sometimes useful to extract the limit point from the filter.\<close> |
2547 text\<open>It's also sometimes useful to extract the limit point from the filter.\<close> |
2548 |
2548 |
2549 abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a" |
2549 abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a" |
2556 fixes a :: "'a::{perfect_space,t2_space}" |
2556 fixes a :: "'a::{perfect_space,t2_space}" |
2557 shows "netlimit (at a) = a" |
2557 shows "netlimit (at a) = a" |
2558 using netlimit_within [of a UNIV] by simp |
2558 using netlimit_within [of a UNIV] by simp |
2559 |
2559 |
2560 lemma lim_within_interior: |
2560 lemma lim_within_interior: |
2561 "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)" |
2561 "x \<in> interior S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at x)" |
2562 by (metis at_within_interior) |
2562 by (metis at_within_interior) |
2563 |
2563 |
2564 lemma netlimit_within_interior: |
2564 lemma netlimit_within_interior: |
2565 fixes x :: "'a::{t2_space,perfect_space}" |
2565 fixes x :: "'a::{t2_space,perfect_space}" |
2566 assumes "x \<in> interior S" |
2566 assumes "x \<in> interior S" |
2608 then show "?lhs" unfolding closure_def islimpt_sequential by auto |
2608 then show "?lhs" unfolding closure_def islimpt_sequential by auto |
2609 qed |
2609 qed |
2610 |
2610 |
2611 lemma closed_sequential_limits: |
2611 lemma closed_sequential_limits: |
2612 fixes S :: "'a::first_countable_topology set" |
2612 fixes S :: "'a::first_countable_topology set" |
2613 shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)" |
2613 shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> l) sequentially \<longrightarrow> l \<in> S)" |
2614 by (metis closure_sequential closure_subset_eq subset_iff) |
2614 by (metis closure_sequential closure_subset_eq subset_iff) |
2615 |
2615 |
2616 lemma closure_approachable: |
2616 lemma closure_approachable: |
2617 fixes S :: "'a::metric_space set" |
2617 fixes S :: "'a::metric_space set" |
2618 shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)" |
2618 shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)" |
2793 by (rule in_closure_iff_infdist_zero) fact |
2793 by (rule in_closure_iff_infdist_zero) fact |
2794 with assms show ?thesis by simp |
2794 with assms show ?thesis by simp |
2795 qed |
2795 qed |
2796 |
2796 |
2797 lemma tendsto_infdist [tendsto_intros]: |
2797 lemma tendsto_infdist [tendsto_intros]: |
2798 assumes f: "(f ---> l) F" |
2798 assumes f: "(f \<longlongrightarrow> l) F" |
2799 shows "((\<lambda>x. infdist (f x) A) ---> infdist l A) F" |
2799 shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F" |
2800 proof (rule tendstoI) |
2800 proof (rule tendstoI) |
2801 fix e ::real |
2801 fix e ::real |
2802 assume "e > 0" |
2802 assume "e > 0" |
2803 from tendstoD[OF f this] |
2803 from tendstoD[OF f this] |
2804 show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F" |
2804 show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F" |
2818 assumes "eventually (\<lambda>i. P i) sequentially" |
2818 assumes "eventually (\<lambda>i. P i) sequentially" |
2819 shows "eventually (\<lambda>i. P (i + k)) sequentially" |
2819 shows "eventually (\<lambda>i. P (i + k)) sequentially" |
2820 using assms by (rule eventually_sequentially_seg [THEN iffD2]) |
2820 using assms by (rule eventually_sequentially_seg [THEN iffD2]) |
2821 |
2821 |
2822 lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *) |
2822 lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *) |
2823 "(f ---> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) ---> l) sequentially" |
2823 "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) \<longlongrightarrow> l) sequentially" |
2824 apply (erule filterlim_compose) |
2824 apply (erule filterlim_compose) |
2825 apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially) |
2825 apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially) |
2826 apply arith |
2826 apply arith |
2827 done |
2827 done |
2828 |
2828 |
2829 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) ---> 0) sequentially" |
2829 lemma seq_harmonic: "((\<lambda>n. inverse (real n)) \<longlongrightarrow> 0) sequentially" |
2830 using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *) |
2830 using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) (* TODO: move to Limits.thy *) |
2831 |
2831 |
2832 subsection \<open>More properties of closed balls\<close> |
2832 subsection \<open>More properties of closed balls\<close> |
2833 |
2833 |
2834 lemma closed_cball [iff]: "closed (cball x e)" |
2834 lemma closed_cball [iff]: "closed (cball x e)" |
3222 from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" |
3222 from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" |
3223 unfolding bounded_def by auto |
3223 unfolding bounded_def by auto |
3224 { |
3224 { |
3225 fix y |
3225 fix y |
3226 assume "y \<in> closure S" |
3226 assume "y \<in> closure S" |
3227 then obtain f where f: "\<forall>n. f n \<in> S" "(f ---> y) sequentially" |
3227 then obtain f where f: "\<forall>n. f n \<in> S" "(f \<longlongrightarrow> y) sequentially" |
3228 unfolding closure_sequential by auto |
3228 unfolding closure_sequential by auto |
3229 have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp |
3229 have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp |
3230 then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially" |
3230 then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially" |
3231 by (simp add: f(1)) |
3231 by (simp add: f(1)) |
3232 have "dist x y \<le> a" |
3232 have "dist x y \<le> a" |
3662 using l unfolding islimpt_eq_acc_point |
3662 using l unfolding islimpt_eq_acc_point |
3663 by (rule acc_point_range_imp_convergent_subsequence) |
3663 by (rule acc_point_range_imp_convergent_subsequence) |
3664 |
3664 |
3665 lemma sequence_unique_limpt: |
3665 lemma sequence_unique_limpt: |
3666 fixes f :: "nat \<Rightarrow> 'a::t2_space" |
3666 fixes f :: "nat \<Rightarrow> 'a::t2_space" |
3667 assumes "(f ---> l) sequentially" |
3667 assumes "(f \<longlongrightarrow> l) sequentially" |
3668 and "l' islimpt (range f)" |
3668 and "l' islimpt (range f)" |
3669 shows "l' = l" |
3669 shows "l' = l" |
3670 proof (rule ccontr) |
3670 proof (rule ccontr) |
3671 assume "l' \<noteq> l" |
3671 assume "l' \<noteq> l" |
3672 obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}" |
3672 obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}" |
3972 |
3972 |
3973 subsubsection\<open>Sequential compactness\<close> |
3973 subsubsection\<open>Sequential compactness\<close> |
3974 |
3974 |
3975 definition seq_compact :: "'a::topological_space set \<Rightarrow> bool" |
3975 definition seq_compact :: "'a::topological_space set \<Rightarrow> bool" |
3976 where "seq_compact S \<longleftrightarrow> |
3976 where "seq_compact S \<longleftrightarrow> |
3977 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially))" |
3977 (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))" |
3978 |
3978 |
3979 lemma seq_compactI: |
3979 lemma seq_compactI: |
3980 assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
3980 assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
3981 shows "seq_compact S" |
3981 shows "seq_compact S" |
3982 unfolding seq_compact_def using assms by fast |
3982 unfolding seq_compact_def using assms by fast |
3983 |
3983 |
3984 lemma seq_compactE: |
3984 lemma seq_compactE: |
3985 assumes "seq_compact S" "\<forall>n. f n \<in> S" |
3985 assumes "seq_compact S" "\<forall>n. f n \<in> S" |
3986 obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially" |
3986 obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially" |
3987 using assms unfolding seq_compact_def by fast |
3987 using assms unfolding seq_compact_def by fast |
3988 |
3988 |
3989 lemma closed_sequentially: (* TODO: move upwards *) |
3989 lemma closed_sequentially: (* TODO: move upwards *) |
3990 assumes "closed s" and "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> l" |
3990 assumes "closed s" and "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> l" |
3991 shows "l \<in> s" |
3991 shows "l \<in> s" |
4182 shows "seq_compact s" |
4182 shows "seq_compact s" |
4183 proof - |
4183 proof - |
4184 { |
4184 { |
4185 fix f :: "nat \<Rightarrow> 'a" |
4185 fix f :: "nat \<Rightarrow> 'a" |
4186 assume f: "\<forall>n. f n \<in> s" |
4186 assume f: "\<forall>n. f n \<in> s" |
4187 have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
4187 have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4188 proof (cases "finite (range f)") |
4188 proof (cases "finite (range f)") |
4189 case True |
4189 case True |
4190 obtain l where "infinite {n. f n = f l}" |
4190 obtain l where "infinite {n. f n = f l}" |
4191 using pigeonhole_infinite[OF _ True] by auto |
4191 using pigeonhole_infinite[OF _ True] by auto |
4192 then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l" |
4192 then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l" |
4259 show "\<exists>r. ?Q x n r" |
4259 show "\<exists>r. ?Q x n r" |
4260 using z by auto |
4260 using z by auto |
4261 qed simp |
4261 qed simp |
4262 then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)" |
4262 then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)" |
4263 by blast |
4263 by blast |
4264 then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" |
4264 then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially" |
4265 using assms by (metis seq_compact_def) |
4265 using assms by (metis seq_compact_def) |
4266 from this(3) have "Cauchy (x \<circ> r)" |
4266 from this(3) have "Cauchy (x \<circ> r)" |
4267 using LIMSEQ_imp_Cauchy by auto |
4267 using LIMSEQ_imp_Cauchy by auto |
4268 then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" |
4268 then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" |
4269 unfolding cauchy_def using \<open>e > 0\<close> by blast |
4269 unfolding cauchy_def using \<open>e > 0\<close> by blast |
4368 proof (unfold seq_compact_def, clarify) |
4368 proof (unfold seq_compact_def, clarify) |
4369 fix f :: "nat \<Rightarrow> 'a" |
4369 fix f :: "nat \<Rightarrow> 'a" |
4370 assume f: "\<forall>n. f n \<in> s" |
4370 assume f: "\<forall>n. f n \<in> s" |
4371 with \<open>bounded s\<close> have "bounded (range f)" |
4371 with \<open>bounded s\<close> have "bounded (range f)" |
4372 by (auto intro: bounded_subset) |
4372 by (auto intro: bounded_subset) |
4373 obtain l r where r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially" |
4373 obtain l r where r: "subseq r" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4374 using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto |
4374 using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto |
4375 from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" |
4375 from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" |
4376 by simp |
4376 by simp |
4377 have "l \<in> s" using \<open>closed s\<close> fr l |
4377 have "l \<in> s" using \<open>closed s\<close> fr l |
4378 by (rule closed_sequentially) |
4378 by (rule closed_sequentially) |
4379 show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
4379 show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4380 using \<open>l \<in> s\<close> r l by blast |
4380 using \<open>l \<in> s\<close> r l by blast |
4381 qed |
4381 qed |
4382 |
4382 |
4383 lemma compact_eq_bounded_closed: |
4383 lemma compact_eq_bounded_closed: |
4384 fixes s :: "'a::heine_borel set" |
4384 fixes s :: "'a::heine_borel set" |
4449 using insert(3) using insert(4) by auto |
4449 using insert(3) using insert(4) by auto |
4450 have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f" |
4450 have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f" |
4451 by simp |
4451 by simp |
4452 have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))" |
4452 have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))" |
4453 by (metis (lifting) bounded_subset f' image_subsetI s') |
4453 by (metis (lifting) bounded_subset f' image_subsetI s') |
4454 then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially" |
4454 then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) \<longlongrightarrow> l2) sequentially" |
4455 using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"] |
4455 using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"] |
4456 by (auto simp: o_def) |
4456 by (auto simp: o_def) |
4457 def r \<equiv> "r1 \<circ> r2" |
4457 def r \<equiv> "r1 \<circ> r2" |
4458 have r:"subseq r" |
4458 have r:"subseq r" |
4459 using r1 and r2 unfolding r_def o_def subseq_def by auto |
4459 using r1 and r2 unfolding r_def o_def subseq_def by auto |
4533 by (simp add: image_comp) |
4533 by (simp add: image_comp) |
4534 obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1" |
4534 obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1" |
4535 using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast |
4535 using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast |
4536 from f have s2: "bounded (range (snd \<circ> f \<circ> r1))" |
4536 from f have s2: "bounded (range (snd \<circ> f \<circ> r1))" |
4537 by (auto simp add: image_comp intro: bounded_snd bounded_subset) |
4537 by (auto simp add: image_comp intro: bounded_snd bounded_subset) |
4538 obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) ---> l2) sequentially" |
4538 obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially" |
4539 using bounded_imp_convergent_subsequence [OF s2] |
4539 using bounded_imp_convergent_subsequence [OF s2] |
4540 unfolding o_def by fast |
4540 unfolding o_def by fast |
4541 have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially" |
4541 have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially" |
4542 using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . |
4542 using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . |
4543 have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially" |
4543 have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially" |
4544 using tendsto_Pair [OF l1' l2] unfolding o_def by simp |
4544 using tendsto_Pair [OF l1' l2] unfolding o_def by simp |
4545 have r: "subseq (r1 \<circ> r2)" |
4545 have r: "subseq (r1 \<circ> r2)" |
4546 using r1 r2 unfolding subseq_def by simp |
4546 using r1 r2 unfolding subseq_def by simp |
4547 show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" |
4547 show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" |
4548 using l r by fast |
4548 using l r by fast |
4549 qed |
4549 qed |
4550 |
4550 |
4551 subsubsection \<open>Completeness\<close> |
4551 subsubsection \<open>Completeness\<close> |
4552 |
4552 |
4775 unfolding compact_eq_bounded_closed by auto |
4775 unfolding compact_eq_bounded_closed by auto |
4776 then have "complete (closure (range f))" |
4776 then have "complete (closure (range f))" |
4777 by (rule compact_imp_complete) |
4777 by (rule compact_imp_complete) |
4778 moreover have "\<forall>n. f n \<in> closure (range f)" |
4778 moreover have "\<forall>n. f n \<in> closure (range f)" |
4779 using closure_subset [of "range f"] by auto |
4779 using closure_subset [of "range f"] by auto |
4780 ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially" |
4780 ultimately have "\<exists>l\<in>closure (range f). (f \<longlongrightarrow> l) sequentially" |
4781 using \<open>Cauchy f\<close> unfolding complete_def by auto |
4781 using \<open>Cauchy f\<close> unfolding complete_def by auto |
4782 then show "convergent f" |
4782 then show "convergent f" |
4783 unfolding convergent_def by auto |
4783 unfolding convergent_def by auto |
4784 qed |
4784 qed |
4785 |
4785 |
4838 by (rule complete_imp_closed) |
4838 by (rule complete_imp_closed) |
4839 qed |
4839 qed |
4840 |
4840 |
4841 lemma convergent_eq_cauchy: |
4841 lemma convergent_eq_cauchy: |
4842 fixes s :: "nat \<Rightarrow> 'a::complete_space" |
4842 fixes s :: "nat \<Rightarrow> 'a::complete_space" |
4843 shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" |
4843 shows "(\<exists>l. (s \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy s" |
4844 unfolding Cauchy_convergent_iff convergent_def .. |
4844 unfolding Cauchy_convergent_iff convergent_def .. |
4845 |
4845 |
4846 lemma convergent_imp_bounded: |
4846 lemma convergent_imp_bounded: |
4847 fixes s :: "nat \<Rightarrow> 'a::metric_space" |
4847 fixes s :: "nat \<Rightarrow> 'a::metric_space" |
4848 shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)" |
4848 shows "(s \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range s)" |
4849 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) |
4849 by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) |
4850 |
4850 |
4851 lemma compact_cball[simp]: |
4851 lemma compact_cball[simp]: |
4852 fixes x :: "'a::heine_borel" |
4852 fixes x :: "'a::heine_borel" |
4853 shows "compact (cball x e)" |
4853 shows "compact (cball x e)" |
5284 qed |
5284 qed |
5285 |
5285 |
5286 lemma continuous_at_sequentially: |
5286 lemma continuous_at_sequentially: |
5287 fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space" |
5287 fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space" |
5288 shows "continuous (at a) f \<longleftrightarrow> |
5288 shows "continuous (at a) f \<longleftrightarrow> |
5289 (\<forall>x. (x ---> a) sequentially --> ((f \<circ> x) ---> f a) sequentially)" |
5289 (\<forall>x. (x \<longlongrightarrow> a) sequentially --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)" |
5290 using continuous_within_sequentially[of a UNIV f] by simp |
5290 using continuous_within_sequentially[of a UNIV f] by simp |
5291 |
5291 |
5292 lemma continuous_on_sequentially: |
5292 lemma continuous_on_sequentially: |
5293 fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space" |
5293 fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space" |
5294 shows "continuous_on s f \<longleftrightarrow> |
5294 shows "continuous_on s f \<longleftrightarrow> |
5295 (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially |
5295 (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x \<longlongrightarrow> a) sequentially |
5296 --> ((f \<circ> x) ---> f a) sequentially)" |
5296 --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)" |
5297 (is "?lhs = ?rhs") |
5297 (is "?lhs = ?rhs") |
5298 proof |
5298 proof |
5299 assume ?rhs |
5299 assume ?rhs |
5300 then show ?lhs |
5300 then show ?lhs |
5301 using continuous_within_sequentially[of _ s f] |
5301 using continuous_within_sequentially[of _ s f] |
5309 by auto |
5309 by auto |
5310 qed |
5310 qed |
5311 |
5311 |
5312 lemma uniformly_continuous_on_sequentially: |
5312 lemma uniformly_continuous_on_sequentially: |
5313 "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and> |
5313 "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and> |
5314 ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially |
5314 ((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially |
5315 \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs") |
5315 \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially)" (is "?lhs = ?rhs") |
5316 proof |
5316 proof |
5317 assume ?lhs |
5317 assume ?lhs |
5318 { |
5318 { |
5319 fix x y |
5319 fix x y |
5320 assume x: "\<forall>n. x n \<in> s" |
5320 assume x: "\<forall>n. x n \<in> s" |
5321 and y: "\<forall>n. y n \<in> s" |
5321 and y: "\<forall>n. y n \<in> s" |
5322 and xy: "((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially" |
5322 and xy: "((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially" |
5323 { |
5323 { |
5324 fix e :: real |
5324 fix e :: real |
5325 assume "e > 0" |
5325 assume "e > 0" |
5326 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" |
5326 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" |
5327 using \<open>?lhs\<close>[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto |
5327 using \<open>?lhs\<close>[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto |
5388 unfolding uniformly_continuous_on_def by blast |
5388 unfolding uniformly_continuous_on_def by blast |
5389 qed |
5389 qed |
5390 |
5390 |
5391 lemma continuous_on_tendsto_compose: |
5391 lemma continuous_on_tendsto_compose: |
5392 assumes f_cont: "continuous_on s f" |
5392 assumes f_cont: "continuous_on s f" |
5393 assumes g: "(g ---> l) F" |
5393 assumes g: "(g \<longlongrightarrow> l) F" |
5394 assumes l: "l \<in> s" |
5394 assumes l: "l \<in> s" |
5395 assumes ev: "\<forall>\<^sub>F x in F. g x \<in> s" |
5395 assumes ev: "\<forall>\<^sub>F x in F. g x \<in> s" |
5396 shows "((\<lambda>x. f (g x)) ---> f l) F" |
5396 shows "((\<lambda>x. f (g x)) \<longlongrightarrow> f l) F" |
5397 proof - |
5397 proof - |
5398 from f_cont have f: "(f ---> f l) (at l within s)" |
5398 from f_cont have f: "(f \<longlongrightarrow> f l) (at l within s)" |
5399 by (auto simp: l continuous_on) |
5399 by (auto simp: l continuous_on) |
5400 have i: "((\<lambda>x. if g x = l then f l else f (g x)) ---> f l) F" |
5400 have i: "((\<lambda>x. if g x = l then f l else f (g x)) \<longlongrightarrow> f l) F" |
5401 by (rule filterlim_If) |
5401 by (rule filterlim_If) |
5402 (auto intro!: filterlim_compose[OF f] eventually_conj tendsto_mono[OF _ g] |
5402 (auto intro!: filterlim_compose[OF f] eventually_conj tendsto_mono[OF _ g] |
5403 simp: filterlim_at eventually_inf_principal eventually_mono[OF ev]) |
5403 simp: filterlim_at eventually_inf_principal eventually_mono[OF ev]) |
5404 show ?thesis |
5404 show ?thesis |
5405 by (rule filterlim_cong[THEN iffD1[OF _ i]]) auto |
5405 by (rule filterlim_cong[THEN iffD1[OF _ i]]) auto |
5420 show "0 < d" by fact |
5420 show "0 < d" by fact |
5421 show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'" |
5421 show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'" |
5422 using assms(3) by auto |
5422 using assms(3) by auto |
5423 have "f x = g x" |
5423 have "f x = g x" |
5424 using assms(1,2,3) by auto |
5424 using assms(1,2,3) by auto |
5425 then show "(f ---> g x) (at x within s)" |
5425 then show "(f \<longlongrightarrow> g x) (at x within s)" |
5426 using assms(4) unfolding continuous_within by simp |
5426 using assms(4) unfolding continuous_within by simp |
5427 qed |
5427 qed |
5428 |
5428 |
5429 lemma continuous_transform_at: |
5429 lemma continuous_transform_at: |
5430 fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space" |
5430 fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space" |
5820 and "f x \<noteq> a" |
5820 and "f x \<noteq> a" |
5821 shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a" |
5821 shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a" |
5822 proof - |
5822 proof - |
5823 obtain U where "open U" and "f x \<in> U" and "a \<notin> U" |
5823 obtain U where "open U" and "f x \<in> U" and "a \<notin> U" |
5824 using t1_space [OF \<open>f x \<noteq> a\<close>] by fast |
5824 using t1_space [OF \<open>f x \<noteq> a\<close>] by fast |
5825 have "(f ---> f x) (at x within s)" |
5825 have "(f \<longlongrightarrow> f x) (at x within s)" |
5826 using assms(1) by (simp add: continuous_within) |
5826 using assms(1) by (simp add: continuous_within) |
5827 then have "eventually (\<lambda>y. f y \<in> U) (at x within s)" |
5827 then have "eventually (\<lambda>y. f y \<in> U) (at x within s)" |
5828 using \<open>open U\<close> and \<open>f x \<in> U\<close> |
5828 using \<open>open U\<close> and \<open>f x \<in> U\<close> |
5829 unfolding tendsto_def by fast |
5829 unfolding tendsto_def by fast |
5830 then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)" |
5830 then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)" |
6568 shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}" |
6568 shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}" |
6569 proof - |
6569 proof - |
6570 let ?S = "{x + y |x y. x \<in> s \<and> y \<in> t}" |
6570 let ?S = "{x + y |x y. x \<in> s \<and> y \<in> t}" |
6571 { |
6571 { |
6572 fix x l |
6572 fix x l |
6573 assume as: "\<forall>n. x n \<in> ?S" "(x ---> l) sequentially" |
6573 assume as: "\<forall>n. x n \<in> ?S" "(x \<longlongrightarrow> l) sequentially" |
6574 from as(1) obtain f where f: "\<forall>n. x n = fst (f n) + snd (f n)" "\<forall>n. fst (f n) \<in> s" "\<forall>n. snd (f n) \<in> t" |
6574 from as(1) obtain f where f: "\<forall>n. x n = fst (f n) + snd (f n)" "\<forall>n. fst (f n) \<in> s" "\<forall>n. snd (f n) \<in> t" |
6575 using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> s \<and> snd y \<in> t"] by auto |
6575 using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> s \<and> snd y \<in> t"] by auto |
6576 obtain l' r where "l'\<in>s" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially" |
6576 obtain l' r where "l'\<in>s" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially" |
6577 using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto |
6577 using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto |
6578 have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially" |
6578 have "((\<lambda>n. snd (f (r n))) \<longlongrightarrow> l - l') sequentially" |
6579 using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) |
6579 using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) |
6580 unfolding o_def |
6580 unfolding o_def |
6581 by auto |
6581 by auto |
6582 then have "l - l' \<in> t" |
6582 then have "l - l' \<in> t" |
6583 using assms(2)[unfolded closed_sequential_limits, |
6583 using assms(2)[unfolded closed_sequential_limits, |
6904 |
6904 |
6905 text \<open>This gives a simple derivation of limit component bounds.\<close> |
6905 text \<open>This gives a simple derivation of limit component bounds.\<close> |
6906 |
6906 |
6907 lemma Lim_component_le: |
6907 lemma Lim_component_le: |
6908 fixes f :: "'a \<Rightarrow> 'b::euclidean_space" |
6908 fixes f :: "'a \<Rightarrow> 'b::euclidean_space" |
6909 assumes "(f ---> l) net" |
6909 assumes "(f \<longlongrightarrow> l) net" |
6910 and "\<not> (trivial_limit net)" |
6910 and "\<not> (trivial_limit net)" |
6911 and "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net" |
6911 and "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net" |
6912 shows "l\<bullet>i \<le> b" |
6912 shows "l\<bullet>i \<le> b" |
6913 by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)]) |
6913 by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)]) |
6914 |
6914 |
6915 lemma Lim_component_ge: |
6915 lemma Lim_component_ge: |
6916 fixes f :: "'a \<Rightarrow> 'b::euclidean_space" |
6916 fixes f :: "'a \<Rightarrow> 'b::euclidean_space" |
6917 assumes "(f ---> l) net" |
6917 assumes "(f \<longlongrightarrow> l) net" |
6918 and "\<not> (trivial_limit net)" |
6918 and "\<not> (trivial_limit net)" |
6919 and "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net" |
6919 and "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net" |
6920 shows "b \<le> l\<bullet>i" |
6920 shows "b \<le> l\<bullet>i" |
6921 by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)]) |
6921 by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)]) |
6922 |
6922 |
6923 lemma Lim_component_eq: |
6923 lemma Lim_component_eq: |
6924 fixes f :: "'a \<Rightarrow> 'b::euclidean_space" |
6924 fixes f :: "'a \<Rightarrow> 'b::euclidean_space" |
6925 assumes net: "(f ---> l) net" "\<not> trivial_limit net" |
6925 assumes net: "(f \<longlongrightarrow> l) net" "\<not> trivial_limit net" |
6926 and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net" |
6926 and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net" |
6927 shows "l\<bullet>i = b" |
6927 shows "l\<bullet>i = b" |
6928 using ev[unfolded order_eq_iff eventually_conj_iff] |
6928 using ev[unfolded order_eq_iff eventually_conj_iff] |
6929 using Lim_component_ge[OF net, of b i] |
6929 using Lim_component_ge[OF net, of b i] |
6930 using Lim_component_le[OF net, of i b] |
6930 using Lim_component_le[OF net, of i b] |
6937 eventually P (at x within s) \<and> eventually P (at x within t)" |
6937 eventually P (at x within s) \<and> eventually P (at x within t)" |
6938 unfolding eventually_at_filter |
6938 unfolding eventually_at_filter |
6939 by (auto elim!: eventually_rev_mp) |
6939 by (auto elim!: eventually_rev_mp) |
6940 |
6940 |
6941 lemma Lim_within_union: |
6941 lemma Lim_within_union: |
6942 "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow> |
6942 "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow> |
6943 (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)" |
6943 (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)" |
6944 unfolding tendsto_def |
6944 unfolding tendsto_def |
6945 by (auto simp add: eventually_within_Un) |
6945 by (auto simp add: eventually_within_Un) |
6946 |
6946 |
6947 lemma Lim_topological: |
6947 lemma Lim_topological: |
6948 "(f ---> l) net \<longleftrightarrow> |
6948 "(f \<longlongrightarrow> l) net \<longleftrightarrow> |
6949 trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)" |
6949 trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)" |
6950 unfolding tendsto_def trivial_limit_eq by auto |
6950 unfolding tendsto_def trivial_limit_eq by auto |
6951 |
6951 |
6952 text \<open>Continuity relative to a union.\<close> |
6952 text \<open>Continuity relative to a union.\<close> |
6953 |
6953 |
7279 by auto |
7279 by auto |
7280 have "inverse (real n + 1) < e" if "N \<le> n" for n |
7280 have "inverse (real n + 1) < e" if "N \<le> n" for n |
7281 by (auto intro!: that le_less_trans [OF _ N]) |
7281 by (auto intro!: that le_less_trans [OF _ N]) |
7282 then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto |
7282 then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto |
7283 } |
7283 } |
7284 then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially" |
7284 then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially" |
7285 unfolding lim_sequentially by(auto simp add: dist_norm) |
7285 unfolding lim_sequentially by(auto simp add: dist_norm) |
7286 then have "(f ---> x) sequentially" |
7286 then have "(f \<longlongrightarrow> x) sequentially" |
7287 unfolding f_def |
7287 unfolding f_def |
7288 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] |
7288 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] |
7289 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] |
7289 using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] |
7290 by auto |
7290 by auto |
7291 } |
7291 } |
7813 then have x:"\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" |
7813 then have x:"\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" |
7814 by auto |
7814 by auto |
7815 then have "f \<circ> x = g" |
7815 then have "f \<circ> x = g" |
7816 unfolding fun_eq_iff |
7816 unfolding fun_eq_iff |
7817 by auto |
7817 by auto |
7818 then obtain l where "l\<in>s" and l:"(x ---> l) sequentially" |
7818 then obtain l where "l\<in>s" and l:"(x \<longlongrightarrow> l) sequentially" |
7819 using cs[unfolded complete_def, THEN spec[where x="x"]] |
7819 using cs[unfolded complete_def, THEN spec[where x="x"]] |
7820 using cauchy_isometric[OF \<open>0 < e\<close> s f normf] and cfg and x(1) |
7820 using cauchy_isometric[OF \<open>0 < e\<close> s f normf] and cfg and x(1) |
7821 by auto |
7821 by auto |
7822 then have "\<exists>l\<in>f ` s. (g ---> l) sequentially" |
7822 then have "\<exists>l\<in>f ` s. (g \<longlongrightarrow> l) sequentially" |
7823 using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l] |
7823 using linear_continuous_at[OF f, unfolded continuous_at_sequentially, THEN spec[where x=x], of l] |
7824 unfolding \<open>f \<circ> x = g\<close> |
7824 unfolding \<open>f \<circ> x = g\<close> |
7825 by auto |
7825 by auto |
7826 } |
7826 } |
7827 then show ?thesis |
7827 then show ?thesis |