60812
|
1 |
(* Title: HOL/Multivariate_Analysis/Uniform_Limit.thy
|
|
2 |
Author: Christoph Traut, TU München
|
|
3 |
Author: Fabian Immler, TU München
|
|
4 |
*)
|
|
5 |
|
|
6 |
section \<open>Uniform Limit and Uniform Convergence\<close>
|
|
7 |
|
|
8 |
theory Uniform_Limit
|
|
9 |
imports Topology_Euclidean_Space
|
|
10 |
begin
|
|
11 |
|
|
12 |
definition uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
|
|
13 |
where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
|
|
14 |
|
|
15 |
abbreviation
|
|
16 |
"uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
|
|
17 |
|
|
18 |
lemma uniform_limit_iff:
|
|
19 |
"uniform_limit S f l F \<longleftrightarrow> (\<forall>e>0. \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e)"
|
|
20 |
unfolding filterlim_iff uniformly_on_def
|
|
21 |
by (subst eventually_INF_base)
|
|
22 |
(fastforce
|
|
23 |
simp: eventually_principal uniformly_on_def
|
|
24 |
intro: bexI[where x="min a b" for a b]
|
|
25 |
elim: eventually_elim1)+
|
|
26 |
|
|
27 |
lemma uniform_limitD:
|
|
28 |
"uniform_limit S f l F \<Longrightarrow> e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e"
|
|
29 |
by (simp add: uniform_limit_iff)
|
|
30 |
|
|
31 |
lemma uniform_limitI:
|
|
32 |
"(\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e) \<Longrightarrow> uniform_limit S f l F"
|
|
33 |
by (simp add: uniform_limit_iff)
|
|
34 |
|
|
35 |
lemma uniform_limit_sequentially_iff:
|
|
36 |
"uniform_limit S f l sequentially \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. dist (f n x) (l x) < e)"
|
|
37 |
unfolding uniform_limit_iff eventually_sequentially ..
|
|
38 |
|
|
39 |
lemma uniform_limit_at_iff:
|
|
40 |
"uniform_limit S f l (at x) \<longleftrightarrow>
|
|
41 |
(\<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) < e))"
|
|
42 |
unfolding uniform_limit_iff eventually_at2 ..
|
|
43 |
|
|
44 |
lemma uniform_limit_at_le_iff:
|
|
45 |
"uniform_limit S f l (at x) \<longleftrightarrow>
|
|
46 |
(\<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))"
|
|
47 |
unfolding uniform_limit_iff eventually_at2
|
|
48 |
by (fastforce dest: spec[where x = "e / 2" for e])
|
|
49 |
|
|
50 |
lemma swap_uniform_limit:
|
|
51 |
assumes f: "\<forall>\<^sub>F n in F. (f n ---> g n) (at x within S)"
|
|
52 |
assumes g: "(g ---> l) F"
|
|
53 |
assumes uc: "uniform_limit S f h F"
|
|
54 |
assumes "\<not>trivial_limit F"
|
|
55 |
shows "(h ---> l) (at x within S)"
|
|
56 |
proof (rule tendstoI)
|
|
57 |
fix e :: real
|
|
58 |
def e' \<equiv> "e/3"
|
|
59 |
assume "0 < e"
|
|
60 |
then have "0 < e'" by (simp add: e'_def)
|
61222
|
61 |
from uniform_limitD[OF uc \<open>0 < e'\<close>]
|
60812
|
62 |
have "\<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (h x) (f n x) < e'"
|
|
63 |
by (simp add: dist_commute)
|
|
64 |
moreover
|
|
65 |
from f
|
|
66 |
have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
|
61222
|
67 |
by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
|
60812
|
68 |
moreover
|
61222
|
69 |
from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
|
60812
|
70 |
by (simp add: dist_commute)
|
|
71 |
ultimately
|
|
72 |
have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
|
|
73 |
proof eventually_elim
|
|
74 |
case (elim n)
|
|
75 |
note fh = elim(1)
|
|
76 |
note gl = elim(3)
|
|
77 |
have "\<forall>\<^sub>F x in at x within S. x \<in> S"
|
|
78 |
by (auto simp: eventually_at_filter)
|
|
79 |
with elim(2)
|
|
80 |
show ?case
|
|
81 |
proof eventually_elim
|
|
82 |
case (elim x)
|
61222
|
83 |
from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
|
60812
|
84 |
have "dist (h x) (g n) < e' + e'"
|
|
85 |
by (rule dist_triangle_lt[OF add_strict_mono])
|
|
86 |
from dist_triangle_lt[OF add_strict_mono, OF this gl]
|
|
87 |
show ?case by (simp add: e'_def)
|
|
88 |
qed
|
|
89 |
qed
|
|
90 |
thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
|
61222
|
91 |
using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
|
60812
|
92 |
qed
|
|
93 |
|
|
94 |
lemma
|
|
95 |
tendsto_uniform_limitI:
|
|
96 |
assumes "uniform_limit S f l F"
|
|
97 |
assumes "x \<in> S"
|
|
98 |
shows "((\<lambda>y. f y x) ---> l x) F"
|
|
99 |
using assms
|
|
100 |
by (auto intro!: tendstoI simp: eventually_elim1 dest!: uniform_limitD)
|
|
101 |
|
|
102 |
lemma uniform_limit_theorem:
|
|
103 |
assumes c: "\<forall>\<^sub>F n in F. continuous_on A (f n)"
|
|
104 |
assumes ul: "uniform_limit A f l F"
|
|
105 |
assumes "\<not> trivial_limit F"
|
|
106 |
shows "continuous_on A l"
|
|
107 |
unfolding continuous_on_def
|
|
108 |
proof safe
|
|
109 |
fix x assume "x \<in> A"
|
|
110 |
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"
|
|
111 |
using c ul
|
|
112 |
by (auto simp: continuous_on_def eventually_elim1 tendsto_uniform_limitI)
|
|
113 |
then show "(l ---> l x) (at x within A)"
|
|
114 |
by (rule swap_uniform_limit) fact+
|
|
115 |
qed
|
|
116 |
|
|
117 |
lemma weierstrass_m_test:
|
|
118 |
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
|
|
119 |
assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
|
|
120 |
assumes "summable M"
|
|
121 |
shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
|
|
122 |
proof (rule uniform_limitI)
|
|
123 |
fix e :: real
|
|
124 |
assume "0 < e"
|
61222
|
125 |
from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
|
60812
|
126 |
have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
|
|
127 |
by (auto simp: eventually_sequentially)
|
|
128 |
thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
|
|
129 |
proof eventually_elim
|
|
130 |
case (elim k)
|
|
131 |
show ?case
|
|
132 |
proof safe
|
|
133 |
fix x assume "x \<in> A"
|
|
134 |
have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
|
61222
|
135 |
using assms(1)[OF \<open>x \<in> A\<close>] by simp
|
60812
|
136 |
hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
|
61222
|
137 |
by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
|
60812
|
138 |
have summable_f: "summable (\<lambda>n. f n x)"
|
|
139 |
using summable_norm_cancel[OF summable_norm_f] .
|
|
140 |
have summable_norm_f_plus_k: "summable (\<lambda>i. norm (f (i + k) x))"
|
|
141 |
using summable_ignore_initial_segment[OF summable_norm_f]
|
|
142 |
by auto
|
|
143 |
have summable_M_plus_k: "summable (\<lambda>i. M (i + k))"
|
61222
|
144 |
using summable_ignore_initial_segment[OF \<open>summable M\<close>]
|
60812
|
145 |
by auto
|
|
146 |
|
|
147 |
have "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) = norm ((\<Sum>i. f i x) - (\<Sum>i<k. f i x))"
|
|
148 |
using dist_norm dist_commute by (subst dist_commute)
|
|
149 |
also have "... = norm (\<Sum>i. f (i + k) x)"
|
|
150 |
using suminf_minus_initial_segment[OF summable_f, where k=k] by simp
|
|
151 |
also have "... \<le> (\<Sum>i. norm (f (i + k) x))"
|
|
152 |
using summable_norm[OF summable_norm_f_plus_k] .
|
|
153 |
also have "... \<le> (\<Sum>i. M (i + k))"
|
|
154 |
by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
|
61222
|
155 |
(simp add: assms(1)[OF \<open>x \<in> A\<close>])
|
60812
|
156 |
finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
|
|
157 |
using elim by auto
|
|
158 |
qed
|
|
159 |
qed
|
|
160 |
qed
|
|
161 |
|
|
162 |
lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
|
|
163 |
by simp
|
|
164 |
|
|
165 |
named_theorems uniform_limit_intros "introduction rules for uniform_limit"
|
61222
|
166 |
setup \<open>
|
60812
|
167 |
Global_Theory.add_thms_dynamic (@{binding uniform_limit_eq_intros},
|
|
168 |
fn context =>
|
|
169 |
Named_Theorems.get (Context.proof_of context) @{named_theorems uniform_limit_intros}
|
|
170 |
|> map_filter (try (fn thm => @{thm uniform_limit_eq_rhs} OF [thm])))
|
61222
|
171 |
\<close>
|
60812
|
172 |
|
|
173 |
lemma (in bounded_linear) uniform_limit[uniform_limit_intros]:
|
|
174 |
assumes "uniform_limit X g l F"
|
|
175 |
shows "uniform_limit X (\<lambda>a b. f (g a b)) (\<lambda>a. f (l a)) F"
|
|
176 |
proof (rule uniform_limitI)
|
|
177 |
fix e::real
|
|
178 |
from pos_bounded obtain K
|
|
179 |
where K: "\<And>x y. dist (f x) (f y) \<le> K * dist x y" "K > 0"
|
|
180 |
by (auto simp: ac_simps dist_norm diff[symmetric])
|
61222
|
181 |
assume "0 < e" with \<open>K > 0\<close> have "e / K > 0" by simp
|
60812
|
182 |
from uniform_limitD[OF assms this]
|
|
183 |
show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f (g n x)) (f (l x)) < e"
|
|
184 |
by eventually_elim (metis le_less_trans mult.commute pos_less_divide_eq K)
|
|
185 |
qed
|
|
186 |
|
|
187 |
lemmas bounded_linear_uniform_limit_intros[uniform_limit_intros] =
|
|
188 |
bounded_linear.uniform_limit[OF bounded_linear_Im]
|
|
189 |
bounded_linear.uniform_limit[OF bounded_linear_Re]
|
|
190 |
bounded_linear.uniform_limit[OF bounded_linear_cnj]
|
|
191 |
bounded_linear.uniform_limit[OF bounded_linear_fst]
|
|
192 |
bounded_linear.uniform_limit[OF bounded_linear_snd]
|
|
193 |
bounded_linear.uniform_limit[OF bounded_linear_zero]
|
|
194 |
bounded_linear.uniform_limit[OF bounded_linear_of_real]
|
|
195 |
bounded_linear.uniform_limit[OF bounded_linear_inner_left]
|
|
196 |
bounded_linear.uniform_limit[OF bounded_linear_inner_right]
|
|
197 |
bounded_linear.uniform_limit[OF bounded_linear_divide]
|
|
198 |
bounded_linear.uniform_limit[OF bounded_linear_scaleR_right]
|
|
199 |
bounded_linear.uniform_limit[OF bounded_linear_mult_left]
|
|
200 |
bounded_linear.uniform_limit[OF bounded_linear_mult_right]
|
|
201 |
bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
|
|
202 |
|
|
203 |
lemmas uniform_limit_uminus[uniform_limit_intros] =
|
|
204 |
bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
|
|
205 |
|
|
206 |
lemma uniform_limit_add[uniform_limit_intros]:
|
|
207 |
fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
|
|
208 |
assumes "uniform_limit X f l F"
|
|
209 |
assumes "uniform_limit X g m F"
|
|
210 |
shows "uniform_limit X (\<lambda>a b. f a b + g a b) (\<lambda>a. l a + m a) F"
|
|
211 |
proof (rule uniform_limitI)
|
|
212 |
fix e::real
|
|
213 |
assume "0 < e"
|
|
214 |
hence "0 < e / 2" by simp
|
|
215 |
from
|
|
216 |
uniform_limitD[OF assms(1) this]
|
|
217 |
uniform_limitD[OF assms(2) this]
|
|
218 |
show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (f n x + g n x) (l x + m x) < e"
|
|
219 |
by eventually_elim (simp add: dist_triangle_add_half)
|
|
220 |
qed
|
|
221 |
|
|
222 |
lemma uniform_limit_minus[uniform_limit_intros]:
|
|
223 |
fixes f g::"'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
|
|
224 |
assumes "uniform_limit X f l F"
|
|
225 |
assumes "uniform_limit X g m F"
|
|
226 |
shows "uniform_limit X (\<lambda>a b. f a b - g a b) (\<lambda>a. l a - m a) F"
|
|
227 |
unfolding diff_conv_add_uminus
|
|
228 |
by (rule uniform_limit_intros assms)+
|
|
229 |
|
|
230 |
lemma (in bounded_bilinear) bounded_uniform_limit[uniform_limit_intros]:
|
|
231 |
assumes "uniform_limit X f l F"
|
|
232 |
assumes "uniform_limit X g m F"
|
|
233 |
assumes "bounded (m ` X)"
|
|
234 |
assumes "bounded (l ` X)"
|
|
235 |
shows "uniform_limit X (\<lambda>a b. prod (f a b) (g a b)) (\<lambda>a. prod (l a) (m a)) F"
|
|
236 |
proof (rule uniform_limitI)
|
|
237 |
fix e::real
|
|
238 |
from pos_bounded obtain K where K:
|
|
239 |
"0 < K" "\<And>a b. norm (prod a b) \<le> norm a * norm b * K"
|
|
240 |
by auto
|
|
241 |
hence "sqrt (K*4) > 0" by simp
|
|
242 |
|
|
243 |
from assms obtain Km Kl
|
|
244 |
where Km: "Km > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (m x) \<le> Km"
|
|
245 |
and Kl: "Kl > 0" "\<And>x. x \<in> X \<Longrightarrow> norm (l x) \<le> Kl"
|
|
246 |
by (auto simp: bounded_pos)
|
|
247 |
hence "K * Km * 4 > 0" "K * Kl * 4 > 0"
|
61222
|
248 |
using \<open>K > 0\<close>
|
60812
|
249 |
by simp_all
|
|
250 |
assume "0 < e"
|
|
251 |
|
|
252 |
hence "sqrt e > 0" by simp
|
61222
|
253 |
from uniform_limitD[OF assms(1) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
|
|
254 |
uniform_limitD[OF assms(2) divide_pos_pos[OF this \<open>sqrt (K*4) > 0\<close>]]
|
|
255 |
uniform_limitD[OF assms(1) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Km * 4 > 0\<close>]]
|
|
256 |
uniform_limitD[OF assms(2) divide_pos_pos[OF \<open>e > 0\<close> \<open>K * Kl * 4 > 0\<close>]]
|
60812
|
257 |
show "\<forall>\<^sub>F n in F. \<forall>x\<in>X. dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
|
|
258 |
proof eventually_elim
|
|
259 |
case (elim n)
|
|
260 |
show ?case
|
|
261 |
proof safe
|
|
262 |
fix x assume "x \<in> X"
|
|
263 |
have "dist (prod (f n x) (g n x)) (prod (l x) (m x)) \<le>
|
|
264 |
norm (prod (f n x - l x) (g n x - m x)) +
|
|
265 |
norm (prod (f n x - l x) (m x)) +
|
|
266 |
norm (prod (l x) (g n x - m x))"
|
|
267 |
by (auto simp: dist_norm prod_diff_prod intro: order_trans norm_triangle_ineq add_mono)
|
|
268 |
also note K(2)[of "f n x - l x" "g n x - m x"]
|
61222
|
269 |
also from elim(1)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
|
60812
|
270 |
have "norm (f n x - l x) \<le> sqrt e / sqrt (K * 4)"
|
|
271 |
by simp
|
61222
|
272 |
also from elim(2)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
|
60812
|
273 |
have "norm (g n x - m x) \<le> sqrt e / sqrt (K * 4)"
|
|
274 |
by simp
|
|
275 |
also have "sqrt e / sqrt (K * 4) * (sqrt e / sqrt (K * 4)) * K = e / 4"
|
61222
|
276 |
using \<open>K > 0\<close> \<open>e > 0\<close> by auto
|
60812
|
277 |
also note K(2)[of "f n x - l x" "m x"]
|
|
278 |
also note K(2)[of "l x" "g n x - m x"]
|
61222
|
279 |
also from elim(3)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
|
60812
|
280 |
have "norm (f n x - l x) \<le> e / (K * Km * 4)"
|
|
281 |
by simp
|
61222
|
282 |
also from elim(4)[THEN bspec, OF \<open>_ \<in> X\<close>, unfolded dist_norm]
|
60812
|
283 |
have "norm (g n x - m x) \<le> e / (K * Kl * 4)"
|
|
284 |
by simp
|
61222
|
285 |
also note Kl(2)[OF \<open>_ \<in> X\<close>]
|
|
286 |
also note Km(2)[OF \<open>_ \<in> X\<close>]
|
60812
|
287 |
also have "e / (K * Km * 4) * Km * K = e / 4"
|
61222
|
288 |
using \<open>K > 0\<close> \<open>Km > 0\<close> by simp
|
60812
|
289 |
also have " Kl * (e / (K * Kl * 4)) * K = e / 4"
|
61222
|
290 |
using \<open>K > 0\<close> \<open>Kl > 0\<close> by simp
|
|
291 |
also have "e / 4 + e / 4 + e / 4 < e" using \<open>e > 0\<close> by simp
|
60812
|
292 |
finally show "dist (prod (f n x) (g n x)) (prod (l x) (m x)) < e"
|
61222
|
293 |
using \<open>K > 0\<close> \<open>Kl > 0\<close> \<open>Km > 0\<close> \<open>e > 0\<close>
|
60812
|
294 |
by (simp add: algebra_simps mult_right_mono divide_right_mono)
|
|
295 |
qed
|
|
296 |
qed
|
|
297 |
qed
|
|
298 |
|
|
299 |
lemmas bounded_bilinear_bounded_uniform_limit_intros[uniform_limit_intros] =
|
|
300 |
bounded_bilinear.bounded_uniform_limit[OF Inner_Product.bounded_bilinear_inner]
|
|
301 |
bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_mult]
|
|
302 |
bounded_bilinear.bounded_uniform_limit[OF Real_Vector_Spaces.bounded_bilinear_scaleR]
|
|
303 |
|
|
304 |
lemma metric_uniform_limit_imp_uniform_limit:
|
|
305 |
assumes f: "uniform_limit S f a F"
|
|
306 |
assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
|
|
307 |
shows "uniform_limit S g b F"
|
|
308 |
proof (rule uniform_limitI)
|
|
309 |
fix e :: real assume "0 < e"
|
|
310 |
from uniform_limitD[OF f this] le
|
|
311 |
show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (g x y) (b y) < e"
|
|
312 |
by eventually_elim force
|
|
313 |
qed
|
|
314 |
|
|
315 |
lemma uniform_limit_null_comparison:
|
|
316 |
assumes "\<forall>\<^sub>F x in F. \<forall>a\<in>S. norm (f x a) \<le> g x a"
|
|
317 |
assumes "uniform_limit S g (\<lambda>_. 0) F"
|
|
318 |
shows "uniform_limit S f (\<lambda>_. 0) F"
|
|
319 |
using assms(2)
|
|
320 |
proof (rule metric_uniform_limit_imp_uniform_limit)
|
|
321 |
show "\<forall>\<^sub>F x in F. \<forall>y\<in>S. dist (f x y) 0 \<le> dist (g x y) 0"
|
|
322 |
using assms(1) by (rule eventually_elim1) (force simp add: dist_norm)
|
|
323 |
qed
|
|
324 |
|
|
325 |
lemma uniform_limit_on_union:
|
|
326 |
"uniform_limit I f g F \<Longrightarrow> uniform_limit J f g F \<Longrightarrow> uniform_limit (I \<union> J) f g F"
|
|
327 |
by (auto intro!: uniform_limitI dest!: uniform_limitD elim: eventually_elim2)
|
|
328 |
|
|
329 |
lemma uniform_limit_on_empty:
|
|
330 |
"uniform_limit {} f g F"
|
|
331 |
by (auto intro!: uniform_limitI)
|
|
332 |
|
|
333 |
lemma uniform_limit_on_UNION:
|
|
334 |
assumes "finite S"
|
|
335 |
assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
|
|
336 |
shows "uniform_limit (UNION S h) f g F"
|
|
337 |
using assms
|
|
338 |
by induct (auto intro: uniform_limit_on_empty uniform_limit_on_union)
|
|
339 |
|
|
340 |
lemma uniform_limit_on_Union:
|
|
341 |
assumes "finite I"
|
|
342 |
assumes "\<And>J. J \<in> I \<Longrightarrow> uniform_limit J f g F"
|
|
343 |
shows "uniform_limit (Union I) f g F"
|
|
344 |
by (metis SUP_identity_eq assms uniform_limit_on_UNION)
|
|
345 |
|
|
346 |
lemma uniform_limit_on_subset:
|
|
347 |
"uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
|
|
348 |
by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono)
|
|
349 |
|
|
350 |
end |