equal
deleted
inserted
replaced
52 (\<forall>e>0. \<exists>d>0. \<forall>z. 0 < dist z x \<and> dist z x < d \<longrightarrow> (\<forall>x\<in>S. dist (f z x) (l x) \<le> e))" |
52 (\<forall>e>0. \<exists>d>0. \<forall>z. 0 < dist z x \<and> dist z x < d \<longrightarrow> (\<forall>x\<in>S. dist (f z x) (l x) \<le> e))" |
53 unfolding uniform_limit_iff eventually_at2 |
53 unfolding uniform_limit_iff eventually_at2 |
54 by (fastforce dest: spec[where x = "e / 2" for e]) |
54 by (fastforce dest: spec[where x = "e / 2" for e]) |
55 |
55 |
56 lemma swap_uniform_limit: |
56 lemma swap_uniform_limit: |
57 assumes f: "\<forall>\<^sub>F n in F. (f n ---> g n) (at x within S)" |
57 assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)" |
58 assumes g: "(g ---> l) F" |
58 assumes g: "(g \<longlongrightarrow> l) F" |
59 assumes uc: "uniform_limit S f h F" |
59 assumes uc: "uniform_limit S f h F" |
60 assumes "\<not>trivial_limit F" |
60 assumes "\<not>trivial_limit F" |
61 shows "(h ---> l) (at x within S)" |
61 shows "(h \<longlongrightarrow> l) (at x within S)" |
62 proof (rule tendstoI) |
62 proof (rule tendstoI) |
63 fix e :: real |
63 fix e :: real |
64 def e' \<equiv> "e/3" |
64 def e' \<equiv> "e/3" |
65 assume "0 < e" |
65 assume "0 < e" |
66 then have "0 < e'" by (simp add: e'_def) |
66 then have "0 < e'" by (simp add: e'_def) |
99 |
99 |
100 lemma |
100 lemma |
101 tendsto_uniform_limitI: |
101 tendsto_uniform_limitI: |
102 assumes "uniform_limit S f l F" |
102 assumes "uniform_limit S f l F" |
103 assumes "x \<in> S" |
103 assumes "x \<in> S" |
104 shows "((\<lambda>y. f y x) ---> l x) F" |
104 shows "((\<lambda>y. f y x) \<longlongrightarrow> l x) F" |
105 using assms |
105 using assms |
106 by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD) |
106 by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD) |
107 |
107 |
108 lemma uniform_limit_theorem: |
108 lemma uniform_limit_theorem: |
109 assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)" |
109 assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)" |
111 assumes "\<not> trivial_limit F" |
111 assumes "\<not> trivial_limit F" |
112 shows "continuous_on A l" |
112 shows "continuous_on A l" |
113 unfolding continuous_on_def |
113 unfolding continuous_on_def |
114 proof safe |
114 proof safe |
115 fix x assume "x \<in> A" |
115 fix x assume "x \<in> A" |
116 then have "\<forall>\<^sub>F n in F. (f n ---> f n x) (at x within A)" "((\<lambda>n. f n x) ---> l x) F" |
116 then have "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> f n x) (at x within A)" "((\<lambda>n. f n x) \<longlongrightarrow> l x) F" |
117 using c ul |
117 using c ul |
118 by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI) |
118 by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI) |
119 then show "(l ---> l x) (at x within A)" |
119 then show "(l \<longlongrightarrow> l x) (at x within A)" |
120 by (rule swap_uniform_limit) fact+ |
120 by (rule swap_uniform_limit) fact+ |
121 qed |
121 qed |
122 |
122 |
123 lemma uniformly_Cauchy_onI: |
123 lemma uniformly_Cauchy_onI: |
124 assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" |
124 assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" |