equal
deleted
inserted
replaced
98 assumes "eventually (\<lambda>i. P i) F" |
98 assumes "eventually (\<lambda>i. P i) F" |
99 assumes "eventually (\<lambda>i. Q i) F" |
99 assumes "eventually (\<lambda>i. Q i) F" |
100 assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" |
100 assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i" |
101 shows "eventually (\<lambda>i. R i) F" |
101 shows "eventually (\<lambda>i. R i) F" |
102 using assms by (auto elim!: eventually_rev_mp) |
102 using assms by (auto elim!: eventually_rev_mp) |
|
103 |
|
104 lemma eventually_subst: |
|
105 assumes "eventually (\<lambda>n. P n = Q n) F" |
|
106 shows "eventually P F = eventually Q F" (is "?L = ?R") |
|
107 proof - |
|
108 from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" |
|
109 and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F" |
|
110 by (auto elim: eventually_elim1) |
|
111 then show ?thesis by (auto elim: eventually_elim2) |
|
112 qed |
|
113 |
|
114 |
103 |
115 |
104 subsection {* Finer-than relation *} |
116 subsection {* Finer-than relation *} |
105 |
117 |
106 text {* @{term "F \<le> F'"} means that filter @{term F} is finer than |
118 text {* @{term "F \<le> F'"} means that filter @{term F} is finer than |
107 filter @{term F'}. *} |
119 filter @{term F'}. *} |
277 |
289 |
278 lemma le_sequentially: |
290 lemma le_sequentially: |
279 "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)" |
291 "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)" |
280 unfolding le_filter_def eventually_sequentially |
292 unfolding le_filter_def eventually_sequentially |
281 by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) |
293 by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) |
|
294 |
|
295 lemma eventually_sequentiallyI: |
|
296 assumes "\<And>x. c \<le> x \<Longrightarrow> P x" |
|
297 shows "eventually P sequentially" |
|
298 using assms by (auto simp: eventually_sequentially) |
282 |
299 |
283 |
300 |
284 subsection {* Standard filters *} |
301 subsection {* Standard filters *} |
285 |
302 |
286 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) |
303 definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70) |
535 |
552 |
536 definition (in topological_space) |
553 definition (in topological_space) |
537 tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where |
554 tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where |
538 "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)" |
555 "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)" |
539 |
556 |
|
557 definition real_tendsto_inf :: "('a \<Rightarrow> real) \<Rightarrow> 'a filter \<Rightarrow> bool" where |
|
558 "real_tendsto_inf f F \<equiv> \<forall>x. eventually (\<lambda>y. x < f y) F" |
|
559 |
540 ML {* |
560 ML {* |
541 structure Tendsto_Intros = Named_Thms |
561 structure Tendsto_Intros = Named_Thms |
542 ( |
562 ( |
543 val name = @{binding tendsto_intros} |
563 val name = @{binding tendsto_intros} |
544 val description = "introduction rules for tendsto" |
564 val description = "introduction rules for tendsto" |
671 with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD) |
691 with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD) |
672 with le show "eventually (\<lambda>x. dist (g x) b < e) F" |
692 with le show "eventually (\<lambda>x. dist (g x) b < e) F" |
673 using le_less_trans by (rule eventually_elim2) |
693 using le_less_trans by (rule eventually_elim2) |
674 qed |
694 qed |
675 |
695 |
|
696 lemma real_tendsto_inf_real: "real_tendsto_inf real sequentially" |
|
697 proof (unfold real_tendsto_inf_def, rule allI) |
|
698 fix x show "eventually (\<lambda>y. x < real y) sequentially" |
|
699 by (rule eventually_sequentiallyI[of "natceiling (x + 1)"]) |
|
700 (simp add: natceiling_le_eq) |
|
701 qed |
|
702 |
|
703 |
|
704 |
676 subsubsection {* Distance and norms *} |
705 subsubsection {* Distance and norms *} |
677 |
706 |
678 lemma tendsto_dist [tendsto_intros]: |
707 lemma tendsto_dist [tendsto_intros]: |
679 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
708 assumes f: "(f ---> l) F" and g: "(g ---> m) F" |
680 shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F" |
709 shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F" |
765 assume "finite S" thus ?thesis using assms |
794 assume "finite S" thus ?thesis using assms |
766 by (induct, simp add: tendsto_const, simp add: tendsto_add) |
795 by (induct, simp add: tendsto_const, simp add: tendsto_add) |
767 next |
796 next |
768 assume "\<not> finite S" thus ?thesis |
797 assume "\<not> finite S" thus ?thesis |
769 by (simp add: tendsto_const) |
798 by (simp add: tendsto_const) |
|
799 qed |
|
800 |
|
801 lemma real_tendsto_sandwich: |
|
802 fixes f g h :: "'a \<Rightarrow> real" |
|
803 assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net" |
|
804 assumes lim: "(f ---> c) net" "(h ---> c) net" |
|
805 shows "(g ---> c) net" |
|
806 proof - |
|
807 have "((\<lambda>n. g n - f n) ---> 0) net" |
|
808 proof (rule metric_tendsto_imp_tendsto) |
|
809 show "eventually (\<lambda>n. dist (g n - f n) 0 \<le> dist (h n - f n) 0) net" |
|
810 using ev by (rule eventually_elim2) (simp add: dist_real_def) |
|
811 show "((\<lambda>n. h n - f n) ---> 0) net" |
|
812 using tendsto_diff[OF lim(2,1)] by simp |
|
813 qed |
|
814 from tendsto_add[OF this lim(1)] show ?thesis by simp |
770 qed |
815 qed |
771 |
816 |
772 subsubsection {* Linear operators and multiplication *} |
817 subsubsection {* Linear operators and multiplication *} |
773 |
818 |
774 lemma (in bounded_linear) tendsto: |
819 lemma (in bounded_linear) tendsto: |