(* Title: HOL/Analysis/Uniform_Limit.thy
Author: Christoph Traut, TU München
Author: Fabian Immler, TU München
*)
section \Uniform Limit and Uniform Convergence\
theory Uniform_Limit
imports Topology_Euclidean_Space Summation_Tests
begin
definition uniformly_on :: "'a set \ ('a \ 'b::metric_space) \ ('a \ 'b) filter"
where "uniformly_on S l = (INF e:{0 <..}. principal {f. \x\S. dist (f x) (l x) < e})"
abbreviation
"uniform_limit S f l \ filterlim f (uniformly_on S l)"
definition uniformly_convergent_on where
"uniformly_convergent_on X f \ (\l. uniform_limit X f l sequentially)"
definition uniformly_Cauchy_on where
"uniformly_Cauchy_on X f \ (\e>0. \M. \x\X. \(m::nat)\M. \n\M. dist (f m x) (f n x) < e)"
lemma uniform_limit_iff:
"uniform_limit S f l F \ (\e>0. \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e)"
unfolding filterlim_iff uniformly_on_def
by (subst eventually_INF_base)
(fastforce
simp: eventually_principal uniformly_on_def
intro: bexI[where x="min a b" for a b]
elim: eventually_mono)+
lemma uniform_limitD:
"uniform_limit S f l F \ e > 0 \ \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e"
by (simp add: uniform_limit_iff)
lemma uniform_limitI:
"(\e. e > 0 \ \\<^sub>F n in F. \x\S. dist (f n x) (l x) < e) \ uniform_limit S f l F"
by (simp add: uniform_limit_iff)
lemma uniform_limit_sequentially_iff:
"uniform_limit S f l sequentially \ (\e>0. \N. \n\N. \x \ S. dist (f n x) (l x) < e)"
unfolding uniform_limit_iff eventually_sequentially ..
lemma uniform_limit_at_iff:
"uniform_limit S f l (at x) \
(\e>0. \d>0. \z. 0 < dist z x \ dist z x < d \ (\x\S. dist (f z x) (l x) < e))"
unfolding uniform_limit_iff eventually_at by simp
lemma uniform_limit_at_le_iff:
"uniform_limit S f l (at x) \
(\e>0. \d>0. \z. 0 < dist z x \ dist z x < d \ (\x\S. dist (f z x) (l x) \ e))"
unfolding uniform_limit_iff eventually_at
by (fastforce dest: spec[where x = "e / 2" for e])
lemma metric_uniform_limit_imp_uniform_limit:
assumes f: "uniform_limit S f a F"
assumes le: "eventually (\x. \y\S. dist (g x y) (b y) \ dist (f x y) (a y)) F"
shows "uniform_limit S g b F"
proof (rule uniform_limitI)
fix e :: real assume "0 < e"
from uniform_limitD[OF f this] le
show "\\<^sub>F x in F. \y\S. dist (g x y) (b y) < e"
by eventually_elim force
qed
lemma swap_uniform_limit:
assumes f: "\\<^sub>F n in F. (f n \ g n) (at x within S)"
assumes g: "(g \ l) F"
assumes uc: "uniform_limit S f h F"
assumes "\trivial_limit F"
shows "(h \ l) (at x within S)"
proof (rule tendstoI)
fix e :: real
define e' where "e' = e/3"
assume "0 < e"
then have "0 < e'" by (simp add: e'_def)
from uniform_limitD[OF uc \0 < e'\]
have "\\<^sub>F n in F. \x\S. dist (h x) (f n x) < e'"
by (simp add: dist_commute)
moreover
from f
have "\\<^sub>F n in F. \\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
by eventually_elim (auto dest!: tendstoD[OF _ \0 < e'\] simp: dist_commute)
moreover
from tendstoD[OF g \0 < e'\] have "\\<^sub>F x in F. dist l (g x) < e'"
by (simp add: dist_commute)
ultimately
have "\\<^sub>F _ in F. \\<^sub>F x in at x within S. dist (h x) l < e"
proof eventually_elim
case (elim n)
note fh = elim(1)
note gl = elim(3)
have "\\<^sub>F x in at x within S. x \ S"
by (auto simp: eventually_at_filter)
with elim(2)
show ?case
proof eventually_elim
case (elim x)
from fh[rule_format, OF \x \ S\] elim(1)
have "dist (h x) (g n) < e' + e'"
by (rule dist_triangle_lt[OF add_strict_mono])
from dist_triangle_lt[OF add_strict_mono, OF this gl]
show ?case by (simp add: e'_def)
qed
qed
thus "\\<^sub>F x in at x within S. dist (h x) l < e"
using eventually_happens by (metis \\trivial_limit F\)
qed
lemma
tendsto_uniform_limitI:
assumes "uniform_limit S f l F"
assumes "x \ S"
shows "((\y. f y x) \ l x) F"
using assms
by (auto intro!: tendstoI simp: eventually_mono dest!: uniform_limitD)
lemma uniform_limit_theorem:
assumes c: "\\<^sub>F n in F. continuous_on A (f n)"
assumes ul: "uniform_limit A f l F"
assumes "\ trivial_limit F"
shows "continuous_on A l"
unfolding continuous_on_def
proof safe
fix x assume "x \ A"
then have "\\<^sub>F n in F. (f n \ f n x) (at x within A)" "((\n. f n x) \ l x) F"
using c ul
by (auto simp: continuous_on_def eventually_mono tendsto_uniform_limitI)
then show "(l \ l x) (at x within A)"
by (rule swap_uniform_limit) fact+
qed
lemma uniformly_Cauchy_onI:
assumes "\e. e > 0 \ \M. \x\X. \m\M. \n\M. dist (f m x) (f n x) < e"
shows "uniformly_Cauchy_on X f"
using assms unfolding uniformly_Cauchy_on_def by blast
lemma uniformly_Cauchy_onI':
assumes "\e. e > 0 \ \M. \x\X. \m\M. \n>m. dist (f m x) (f n x) < e"
shows "uniformly_Cauchy_on X f"
proof (rule uniformly_Cauchy_onI)
fix e :: real assume e: "e > 0"
from assms[OF this] obtain M
where M: "\x m n. x \ X \ m \ M \ n > m \ dist (f m x) (f n x) < e" by fast
{
fix x m n assume x: "x \ X" and m: "m \ M" and n: "n \ M"
with M[OF this(1,2), of n] M[OF this(1,3), of m] e have "dist (f m x) (f n x) < e"
by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
}
thus "\M. \x\X. \m\M. \n\M. dist (f m x) (f n x) < e" by fast
qed
lemma uniformly_Cauchy_imp_Cauchy:
"uniformly_Cauchy_on X f \ x \ X \ Cauchy (\n. f n x)"
unfolding Cauchy_def uniformly_Cauchy_on_def by fast
lemma uniform_limit_cong:
fixes f g :: "'a \ 'b \ ('c :: metric_space)" and h i :: "'b \ 'c"
assumes "eventually (\y. \x\X. f y x = g y x) F"
assumes "\x. x \ X \ h x = i x"
shows "uniform_limit X f h F \ uniform_limit X g i F"
proof -
{
fix f g :: "'a \ 'b \ 'c" and h i :: "'b \ 'c"
assume C: "uniform_limit X f h F" and A: "eventually (\y. \x\X. f y x = g y x) F"
and B: "\x. x \ X \ h x = i x"
{
fix e ::real assume "e > 0"
with C have "eventually (\y. \x\X. dist (f y x) (h x) < e) F"
unfolding uniform_limit_iff by blast
with A have "eventually (\y. \x\X. dist (g y x) (i x) < e) F"
by eventually_elim (insert B, simp_all)
}
hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
} note A = this
show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
qed
lemma uniform_limit_cong':
fixes f g :: "'a \ 'b \ ('c :: metric_space)" and h i :: "'b \ 'c"
assumes "\y x. x \ X \ f y x = g y x"
assumes "\x. x \ X \ h x = i x"
shows "uniform_limit X f h F \ uniform_limit X g i F"
using assms by (intro uniform_limit_cong always_eventually) blast+
lemma uniformly_convergent_uniform_limit_iff:
"uniformly_convergent_on X f \ uniform_limit X f (\x. lim (\n. f n x)) sequentially"
proof
assume "uniformly_convergent_on X f"
then obtain l where l: "uniform_limit X f l sequentially"
unfolding uniformly_convergent_on_def by blast
from l have "uniform_limit X f (\x. lim (\n. f n x)) sequentially \
uniform_limit X f l sequentially"
by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
also note l
finally show "uniform_limit X f (\x. lim (\n. f n x)) sequentially" .
qed (auto simp: uniformly_convergent_on_def)
lemma uniformly_convergentI: "uniform_limit X f l sequentially \ uniformly_convergent_on X f"
unfolding uniformly_convergent_on_def by blast
lemma uniformly_convergent_on_empty [iff]: "uniformly_convergent_on {} f"
by (simp add: uniformly_convergent_on_def uniform_limit_sequentially_iff)
text\Cauchy-type criteria for uniform convergence.\
lemma Cauchy_uniformly_convergent:
fixes f :: "nat \ 'a \ 'b :: complete_space"
assumes "uniformly_Cauchy_on X f"
shows "uniformly_convergent_on X f"
unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
proof safe
let ?f = "\x. lim (\n. f n x)"
fix e :: real assume e: "e > 0"
hence "e/2 > 0" by simp
with assms obtain N where N: "\x m n. x \ X \ m \ N \ n \ N \ dist (f m x) (f n x) < e/2"
unfolding uniformly_Cauchy_on_def by fast
show "eventually (\n. \x\X. dist (f n x) (?f x) < e) sequentially"
using eventually_ge_at_top[of N]
proof eventually_elim
fix n assume n: "n \ N"
show "\x\X. dist (f n x) (?f x) < e"
proof
fix x assume x: "x \ X"
with assms have "(\n. f n x) \ ?f x"
by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
with \e/2 > 0\ have "eventually (\m. m \ N \ dist (f m x) (?f x) < e/2) sequentially"
by (intro tendstoD eventually_conj eventually_ge_at_top)
then obtain m where m: "m \ N" "dist (f m x) (?f x) < e/2"
unfolding eventually_at_top_linorder by blast
have "dist (f n x) (?f x) \ dist (f n x) (f m x) + dist (f m x) (?f x)"
by (rule dist_triangle)
also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
finally show "dist (f n x) (?f x) < e" by simp
qed
qed
qed
lemma uniformly_convergent_Cauchy:
assumes "uniformly_convergent_on X f"
shows "uniformly_Cauchy_on X f"
proof (rule uniformly_Cauchy_onI)
fix e::real assume "e > 0"
then have "0 < e / 2" by simp
with assms[unfolded uniformly_convergent_on_def uniform_limit_sequentially_iff]
obtain l N where l:"x \ X \ n \ N \ dist (f n x) (l x) < e / 2" for n x
by metis
from l l have "x \ X \ n \ N \ m \ N \ dist (f n x) (f m x) < e" for n m x
by (rule dist_triangle_half_l)
then show "\M. \x\X. \m\M. \n\M. dist (f m x) (f n x) < e" by blast
qed
lemma uniformly_convergent_eq_Cauchy:
"uniformly_convergent_on X f = uniformly_Cauchy_on X f" for f::"nat \ 'b \ 'a::complete_space"
using Cauchy_uniformly_convergent uniformly_convergent_Cauchy by blast
lemma uniformly_convergent_eq_cauchy:
fixes s::"nat \ 'b \ 'a::complete_space"
shows
"(\l. \e>0. \N. \n x. N \ n \ P x \ dist(s n x)(l x) < e) \
(\e>0. \N. \m n x. N \ m \ N \ n \ P x \ dist (s m x) (s n x) < e)"
proof -
have *: "(\n\N. \