(* Author: L C Paulson, University of Cambridge
Author: Amine Chaieb, University of Cambridge
Author: Robert Himmelmann, TU Muenchen
Author: Brian Huffman, Portland State University
*)
section \<open>Elementary Metric Spaces\<close>
theory Elementary_Metric_Spaces
imports
Abstract_Topology_2
Metric_Arith
begin
subsection \<open>Open and closed balls\<close>
definition\<^marker>\<open>tag important\<close> ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "ball x e = {y. dist x y < e}"
definition\<^marker>\<open>tag important\<close> cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "cball x e = {y. dist x y \ e}"
definition\<^marker>\<open>tag important\<close> sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
where "sphere x e = {y. dist x y = e}"
lemma mem_ball [simp, metric_unfold]: "y \ ball x e \ dist x y < e"
by (simp add: ball_def)
lemma mem_cball [simp, metric_unfold]: "y \ cball x e \ dist x y \ e"
by (simp add: cball_def)
lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e"
by (simp add: sphere_def)
lemma ball_trivial [simp]: "ball x 0 = {}"
by (simp add: ball_def)
lemma cball_trivial [simp]: "cball x 0 = {x}"
by (simp add: cball_def)
lemma sphere_trivial [simp]: "sphere x 0 = {x}"
by (simp add: sphere_def)
lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}"
using dist_triangle_less_add not_le by fastforce
lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}"
by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)
lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}"
for a :: "'a::metric_space"
by auto
lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e"
by simp
lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e"
by simp
lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e"
by (simp add: subset_eq)
lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e"
by auto
lemma sphere_cball [simp,intro]: "sphere z r \ cball z r"
by force
lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"
by auto
lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e"
by auto
lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e"
by auto
lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f"
by auto
lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f"
by auto
lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)"
by metric
lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s"
by auto
lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s"
by auto
lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s"
by auto
lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s"
by auto
lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r"
by auto
lemma open_ball [intro, simp]: "open (ball x e)"
proof -
have "open (dist x -` {..
by (intro open_vimage open_lessThan continuous_intros)
also have "dist x -` {..
by auto
finally show ?thesis .
qed
lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)"
by (simp add: open_dist subset_eq Ball_def dist_commute)
lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S"
by (auto simp: open_contains_ball)
lemma openE[elim?]:
assumes "open S" "x\S"
obtains e where "e>0" "ball x e \ S"
using assms unfolding open_contains_ball by auto
lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)"
by (metis open_contains_ball subset_eq centre_in_ball)
lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0"
unfolding mem_ball set_eq_iff
by (simp add: not_less) metric
lemma ball_empty: "e \ 0 \ ball x e = {}"
by simp
lemma closed_cball [iff]: "closed (cball x e)"
proof -
have "closed (dist x -` {..e})"
by (intro closed_vimage closed_atMost continuous_intros)
also have "dist x -` {..e} = cball x e"
by auto
finally show ?thesis .
qed
lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)"
proof -
{
fix x and e::real
assume "x\S" "e>0" "ball x e \ S"
then have "\d>0. cball x d \ S"
unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
}
moreover
{
fix x and e::real
assume "x\S" "e>0" "cball x e \ S"
then have "\d>0. ball x d \ S"
using mem_ball_imp_mem_cball by blast
}
ultimately show ?thesis
unfolding open_contains_ball by auto
qed
lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))"
by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)"
by (rule eventually_nhds_in_open) simp_all
lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)"
unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)"
unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y"
by (subst at_within_open) auto
lemma atLeastAtMost_eq_cball:
fixes a b::real
shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps)
lemma cball_eq_atLeastAtMost:
fixes a b::real
shows "cball a b = {a - b .. a + b}"
by (auto simp: dist_real_def)
lemma greaterThanLessThan_eq_ball:
fixes a b::real
shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
by (auto simp: dist_real_def field_simps)
lemma ball_eq_greaterThanLessThan:
fixes a b::real
shows "ball a b = {a - b <..< a + b}"
by (auto simp: dist_real_def)
lemma interior_ball [simp]: "interior (ball x e) = ball x e"
by (simp add: interior_open)
lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0"
apply (simp add: set_eq_iff not_le)
apply (metis zero_le_dist dist_self order_less_le_trans)
done
lemma cball_empty [simp]: "e < 0 \ cball x e = {}"
by simp
lemma cball_sing:
fixes x :: "'a::metric_space"
shows "e = 0 \ cball x e = {x}"
by simp
lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e"
by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one)
lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e"
using ball_divide_subset one_le_numeral by blast
lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e"
apply (cases "e < 0", simp add: field_split_simps)
by (metis div_by_1 frac_le less_numeral_extra(1) not_le order_refl subset_cball)
lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e"
using cball_divide_subset one_le_numeral by blast
lemma cball_scale:
assumes "a \ 0"
shows "(\x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
have 1: "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a
proof safe
fix x
assume x: "x \ cball c r"
have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
by (auto simp: dist_norm)
also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
by (simp add: algebra_simps)
finally show "a *\<^sub>R x \ cball (a *\<^sub>R c) (\a\ * r)"
using that x by (auto simp: dist_norm)
qed
have "cball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\a\ * r)"
unfolding image_image using assms by simp
also have "\ \ (\x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
using assms by (intro image_mono 1) auto
also have "\ = (\x. a *\<^sub>R x) ` cball c r"
using assms by (simp add: algebra_simps)
finally have "cball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` cball c r" .
moreover from assms have "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)"
by (intro 1) auto
ultimately show ?thesis by blast
qed
lemma ball_scale:
assumes "a \ 0"
shows "(\x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
have 1: "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a
proof safe
fix x
assume x: "x \ ball c r"
have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
by (auto simp: dist_norm)
also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
by (simp add: algebra_simps)
finally show "a *\<^sub>R x \ ball (a *\<^sub>R c) (\a\ * r)"
using that x by (auto simp: dist_norm)
qed
have "ball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\a\ * r)"
unfolding image_image using assms by simp
also have "\ \ (\x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
using assms by (intro image_mono 1) auto
also have "\ = (\x. a *\<^sub>R x) ` ball c r"
using assms by (simp add: algebra_simps)
finally have "ball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` ball c r" .
moreover from assms have "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)"
by (intro 1) auto
ultimately show ?thesis by blast
qed
subsection \<open>Limit Points\<close>
lemma islimpt_approachable:
fixes x :: "'a::metric_space"
shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)"
unfolding islimpt_iff_eventually eventually_at by fast
lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)"
for x :: "'a::metric_space"
unfolding islimpt_approachable
using approachable_lt_le2 [where f="\y. dist y x" and P="\y. y \ S \ y = x" and Q="\x. True"]
by auto
lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S"
for x :: "'a::metric_space"
apply (clarsimp simp add: islimpt_approachable)
apply (drule_tac x="e/2" in spec)
apply (auto simp: simp del: less_divide_eq_numeral1)
apply (drule_tac x="dist x' x" in spec)
apply (auto simp del: less_divide_eq_numeral1)
apply metric
done
lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}"
using closed_limpt limpt_of_limpts by blast
lemma limpt_of_closure: "x islimpt closure S \ x islimpt S"
for x :: "'a::metric_space"
by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))"
apply (simp add: islimpt_eq_acc_point, safe)
apply (metis Int_commute open_ball centre_in_ball)
by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)
lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))"
apply (simp add: islimpt_eq_infinite_ball, safe)
apply (meson Int_mono ball_subset_cball finite_subset order_refl)
by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
subsection \<open>Perfect Metric Spaces\<close>
lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r"
for x :: "'a::{perfect_space,metric_space}"
using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
lemma cball_eq_sing:
fixes x :: "'a::{metric_space,perfect_space}"
shows "cball x e = {x} \ e = 0"
proof (rule linorder_cases)
assume e: "0 < e"
obtain a where "a \ x" "dist a x < e"
using perfect_choose_dist [OF e] by auto
then have "a \ x" "dist x a \ e"
by (auto simp: dist_commute)
with e show ?thesis by (auto simp: set_eq_iff)
qed auto
subsection \<open>?\<close>
lemma finite_ball_include:
fixes a :: "'a::metric_space"
assumes "finite S"
shows "\e>0. S \ ball a e"
using assms
proof induction
case (insert x S)
then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto
define e where "e = max e0 (2 * dist a x)"
have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
moreover have "insert x S \ ball a e"
using e0 \<open>e>0\<close> unfolding e_def by auto
ultimately show ?case by auto
qed (auto intro: zero_less_one)
lemma finite_set_avoid:
fixes a :: "'a::metric_space"
assumes "finite S"
shows "\d>0. \x\S. x \ a \ d \ dist a x"
using assms
proof induction
case (insert x S)
then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x"
by blast
show ?case
proof (cases "x = a")
case True
with \<open>d > 0 \<close>d show ?thesis by auto
next
case False
let ?d = "min d (dist a x)"
from False \<open>d > 0\<close> have dp: "?d > 0"
by auto
from d have d': "\x\S. x \ a \ ?d \ dist a x"
by auto
with dp False show ?thesis
by (metis insert_iff le_less min_less_iff_conj not_less)
qed
qed (auto intro: zero_less_one)
lemma discrete_imp_closed:
fixes S :: "'a::metric_space set"
assumes e: "0 < e"
and d: "\x \ S. \y \ S. dist y x < e \ y = x"
shows "closed S"
proof -
have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x
proof -
from e have e2: "e/2 > 0" by arith
from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2"
by blast
from e2 y(2) have mp: "min (e/2) (dist x y) > 0"
by simp
from d y C[OF mp] show ?thesis
by metric
qed
then show ?thesis
by (metis islimpt_approachable closed_limpt [where 'a='a])
qed
subsection \<open>Interior\<close>
lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)"
using open_contains_ball_eq [where S="interior S"]
by (simp add: open_subset_interior)
lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)"
by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
subset_trans)
subsection \<open>Frontier\<close>
lemma frontier_straddle:
fixes a :: "'a::metric_space"
shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))"
unfolding frontier_def closure_interior
by (auto simp: mem_interior subset_eq ball_def)
subsection \<open>Limits\<close>
proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)"
by (auto simp: tendsto_iff trivial_limit_eq)
text \<open>Show that they yield usual definitions in the various cases.\<close>
proposition Lim_within_le: "(f \ l)(at a within S) \
(\<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)"
by (auto simp: tendsto_iff eventually_at_le)
proposition Lim_within: "(f \ l) (at a within S) \
(\<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)"
by (auto simp: tendsto_iff eventually_at)
corollary Lim_withinI [intro?]:
assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e"
shows "(f \ l) (at a within S)"
apply (simp add: Lim_within, clarify)
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
done
proposition Lim_at: "(f \ l) (at a) \
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at)
lemma Lim_transform_within_set:
fixes a :: "'a::metric_space" and l :: "'b::metric_space"
shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\
\<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
apply (clarsimp simp: eventually_at Lim_within)
apply (drule_tac x=e in spec, clarify)
apply (rename_tac k)
apply (rule_tac x="min d k" in exI, simp)
done
text \<open>Another limit point characterization.\<close>
lemma limpt_sequential_inj:
fixes x :: "'a::metric_space"
shows "x islimpt S \
(\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then have "\e>0. \x'\S. x' \ x \ dist x' x < e"
by (force simp: islimpt_approachable)
then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e"
by metis
define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
have [simp]: "f 0 = y 1"
"f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
by (simp_all add: f_def)
have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n
proof (induction n)
case 0 show ?case
by (simp add: y)
next
case (Suc n) then show ?case
apply (auto simp: y)
by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)
qed
show ?rhs
proof (rule_tac x=f in exI, intro conjI allI)
show "\n. f n \ S - {x}"
using f by blast
have "dist (f n) x < dist (f m) x" if "m < n" for m n
using that
proof (induction n)
case 0 then show ?case by simp
next
case (Suc n)
then consider "m < n" | "m = n" using less_Suc_eq by blast
then show ?case
proof cases
assume "m < n"
have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
by simp
also have "\ < dist (f n) x"
by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
also have "\ < dist (f m) x"
using Suc.IH \<open>m < n\<close> by blast
finally show ?thesis .
next
assume "m = n" then show ?case
by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)
qed
qed
then show "inj f"
by (metis less_irrefl linorder_injI)
show "f \ x"
apply (rule tendstoI)
apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)
apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
apply (simp add: field_simps)
by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)
qed
next
assume ?rhs
then show ?lhs
by (fastforce simp add: islimpt_approachable lim_sequentially)
qed
lemma Lim_dist_ubound:
assumes "\(trivial_limit net)"
and "(f \ l) net"
and "eventually (\x. dist a (f x) \ e) net"
shows "dist a l \ e"
using assms by (fast intro: tendsto_le tendsto_intros)
subsection \<open>Continuity\<close>
text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
proposition continuous_within_eps_delta:
"continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)"
unfolding continuous_within and Lim_within by fastforce
corollary continuous_at_eps_delta:
"continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)"
using continuous_within_eps_delta [of x UNIV f] by simp
lemma continuous_at_right_real_increasing:
fixes f :: "real \ real"
assumes nondecF: "\x y. x \ y \ f x \ f y"
shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)"
apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
apply (intro all_cong ex_cong, safe)
apply (erule_tac x="a + d" in allE, simp)
apply (simp add: nondecF field_simps)
apply (drule nondecF, simp)
done
lemma continuous_at_left_real_increasing:
assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)"
shows "(continuous (at_left (a :: real)) f) = (\e > 0. \delta > 0. f a - f (a - delta) < e)"
apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
apply (intro all_cong ex_cong, safe)
apply (erule_tac x="a - d" in allE, simp)
apply (simp add: nondecF field_simps)
apply (cut_tac x="a - d" and y=x in nondecF, simp_all)
done
text\<open>Versions in terms of open balls.\<close>
lemma continuous_within_ball:
"continuous (at x within s) f \
(\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e)"
(is "?lhs = ?rhs")
proof
assume ?lhs
{
fix e :: real
assume "e > 0"
then obtain d where d: "d>0" "\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < e"
using \<open>?lhs\<close>[unfolded continuous_within Lim_within] by auto
{
fix y
assume "y \ f ` (ball x d \ s)"
then have "y \ ball (f x) e"
using d(2)
using \<open>e > 0\<close>
by (auto simp: dist_commute)
}
then have "\d>0. f ` (ball x d \ s) \ ball (f x) e"
using \<open>d > 0\<close>
unfolding subset_eq ball_def by (auto simp: dist_commute)
}
then show ?rhs by auto
next
assume ?rhs
then show ?lhs
unfolding continuous_within Lim_within ball_def subset_eq
apply (auto simp: dist_commute)
apply (erule_tac x=e in allE, auto)
done
qed
lemma continuous_at_ball:
"continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
by (metis dist_commute dist_pos_lt dist_self)
next
assume ?rhs
then show ?lhs
unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
by (metis dist_commute)
qed
text\<open>Define setwise continuity in terms of limits within the set.\<close>
lemma continuous_on_iff:
"continuous_on s f \
(\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
unfolding continuous_on_def Lim_within
by (metis dist_pos_lt dist_self)
lemma continuous_within_E:
assumes "continuous (at x within s) f" "e>0"
obtains d where "d>0" "\x'. \x'\ s; dist x' x \ d\ \ dist (f x') (f x) < e"
using assms apply (simp add: continuous_within_eps_delta)
apply (drule spec [of _ e], clarify)
apply (rule_tac d="d/2" in that, auto)
done
lemma continuous_onI [intro?]:
assumes "\x e. \e > 0; x \ s\ \ \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) \ e"
shows "continuous_on s f"
apply (simp add: continuous_on_iff, clarify)
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
done
text\<open>Some simple consequential lemmas.\<close>
lemma continuous_onE:
assumes "continuous_on s f" "x\s" "e>0"
obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e"
using assms
apply (simp add: continuous_on_iff)
apply (elim ballE allE)
apply (auto intro: that [where d="d/2" for d])
done
text\<open>The usual transformation theorems.\<close>
lemma continuous_transform_within:
fixes f g :: "'a::metric_space \ 'b::topological_space"
assumes "continuous (at x within s) f"
and "0 < d"
and "x \ s"
and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'"
shows "continuous (at x within s) g"
using assms
unfolding continuous_within
by (force intro: Lim_transform_within)
subsection \<open>Closure and Limit Characterization\<close>
lemma closure_approachable:
fixes S :: "'a::metric_space set"
shows "x \ closure S \ (\e>0. \y\S. dist y x < e)"
apply (auto simp: closure_def islimpt_approachable)
apply (metis dist_self)
done
lemma closure_approachable_le:
fixes S :: "'a::metric_space set"
shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)"
unfolding closure_approachable
using dense by force
lemma closure_approachableD:
assumes "x \ closure S" "e>0"
shows "\y\S. dist x y < e"
using assms unfolding closure_approachable by (auto simp: dist_commute)
lemma closed_approachable:
fixes S :: "'a::metric_space set"
shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S"
by (metis closure_closed closure_approachable)
lemma closure_contains_Inf:
fixes S :: "real set"
assumes "S \ {}" "bdd_below S"
shows "Inf S \ closure S"
proof -
have *: "\x\S. Inf S \ x"
using cInf_lower[of _ S] assms by metis
{
fix e :: real
assume "e > 0"
then have "Inf S < Inf S + e" by simp
with assms obtain x where "x \ S" "x < Inf S + e"
by (subst (asm) cInf_less_iff) auto
with * have "\x\S. dist x (Inf S) < e"
by (intro bexI[of _ x]) (auto simp: dist_real_def)
}
then show ?thesis unfolding closure_approachable by auto
qed
lemma closure_contains_Sup:
fixes S :: "real set"
assumes "S \ {}" "bdd_above S"
shows "Sup S \ closure S"
proof -
have *: "\x\S. x \ Sup S"
using cSup_upper[of _ S] assms by metis
{
fix e :: real
assume "e > 0"
then have "Sup S - e < Sup S" by simp
with assms obtain x where "x \ S" "Sup S - e < x"
by (subst (asm) less_cSup_iff) auto
with * have "\x\S. dist x (Sup S) < e"
by (intro bexI[of _ x]) (auto simp: dist_real_def)
}
then show ?thesis unfolding closure_approachable by auto
qed
lemma not_trivial_limit_within_ball:
"\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})"
(is "?lhs \ ?rhs")
proof
show ?rhs if ?lhs
proof -
{
fix e :: real
assume "e > 0"
then obtain y where "y \ S - {x}" and "dist y x < e"
using \<open>?lhs\<close> not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
by auto
then have "y \ S \ ball x e - {x}"
unfolding ball_def by (simp add: dist_commute)
then have "S \ ball x e - {x} \ {}" by blast
}
then show ?thesis by auto
qed
show ?lhs if ?rhs
proof -
{
fix e :: real
assume "e > 0"
then obtain y where "y \ S \ ball x e - {x}"
using \<open>?rhs\<close> by blast
then have "y \ S - {x}" and "dist y x < e"
unfolding ball_def by (simp_all add: dist_commute)
then have "\y \ S - {x}. dist y x < e"
by auto
}
then show ?thesis
using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
by auto
qed
qed
subsection \<open>Boundedness\<close>
(* FIXME: This has to be unified with BSEQ!! *)
definition\<^marker>\<open>tag important\<close> (in metric_space) bounded :: "'a set \<Rightarrow> bool"
where "bounded S \ (\x e. \y\S. dist x y \ e)"
lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)"
unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist)
lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)"
unfolding bounded_def
by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)
lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)"
unfolding bounded_any_center [where a=0]
by (simp add: dist_norm)
lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X"
by (simp add: bounded_iff bdd_above_def)
lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)"
by (simp add: bounded_iff)
lemma boundedI:
assumes "\x. x \ S \ norm x \ B"
shows "bounded S"
using assms bounded_iff by blast
lemma bounded_empty [simp]: "bounded {}"
by (simp add: bounded_def)
lemma bounded_subset: "bounded T \ S \ T \ bounded S"
by (metis bounded_def subset_eq)
lemma bounded_interior[intro]: "bounded S \ bounded(interior S)"
by (metis bounded_subset interior_subset)
lemma bounded_closure[intro]:
assumes "bounded S"
shows "bounded (closure S)"
proof -
from assms obtain x and a where a: "\y\S. dist x y \ a"
unfolding bounded_def by auto
{
fix y
assume "y \ closure S"
then obtain f where f: "\n. f n \ S" "(f \ y) sequentially"
unfolding closure_sequential by auto
have "\n. f n \ S \ dist x (f n) \ a" using a by simp
then have "eventually (\n. dist x (f n) \ a) sequentially"
by (simp add: f(1))
then have "dist x y \ a"
using Lim_dist_ubound f(2) trivial_limit_sequentially by blast
}
then show ?thesis
unfolding bounded_def by auto
qed
lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)"
by (simp add: bounded_subset closure_subset image_mono)
lemma bounded_cball[simp,intro]: "bounded (cball x e)"
unfolding bounded_def using mem_cball by blast
lemma bounded_ball[simp,intro]: "bounded (ball x e)"
by (metis ball_subset_cball bounded_cball bounded_subset)
lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T"
by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)
lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)"
by (induct rule: finite_induct[of F]) auto
lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)"
by auto
lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S"
proof -
have "\y\{x}. dist x y \ 0"
by simp
then have "bounded {x}"
unfolding bounded_def by fast
then show ?thesis
by (metis insert_is_Un bounded_Un)
qed
lemma bounded_subset_ballI: "S \ ball x r \ bounded S"
by (meson bounded_ball bounded_subset)
lemma bounded_subset_ballD:
assumes "bounded S" shows "\r. 0 < r \ S \ ball x r"
proof -
obtain e::real and y where "S \ cball y e" "0 \ e"
using assms by (auto simp: bounded_subset_cball)
then show ?thesis
by (intro exI[where x="dist x y + e + 1"]) metric
qed
lemma finite_imp_bounded [intro]: "finite S \ bounded S"
by (induct set: finite) simp_all
lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)"
by (metis Int_lower1 Int_lower2 bounded_subset)
lemma bounded_diff[intro]: "bounded S \ bounded (S - T)"
by (metis Diff_subset bounded_subset)
lemma bounded_dist_comp:
assumes "bounded (f ` S)" "bounded (g ` S)"
shows "bounded ((\x. dist (f x) (g x)) ` S)"
proof -
from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x
by (auto simp: bounded_any_center[of _ undefined] dist_commute)
have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x
using *[OF that]
by metric
then show ?thesis
by (auto intro!: boundedI)
qed
lemma bounded_Times:
assumes "bounded s" "bounded t"
shows "bounded (s \ t)"
proof -
obtain x y a b where "\z\s. dist x z \ a" "\z\t. dist y z \ b"
using assms [unfolded bounded_def] by auto
then have "\z\s \ t. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)"
by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
qed
subsection \<open>Compactness\<close>
lemma compact_imp_bounded:
assumes "compact U"
shows "bounded U"
proof -
have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)"
using assms by auto
then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)"
by (metis compactE_image)
from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"
by (simp add: bounded_UN)
then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>
by (rule bounded_subset)
qed
lemma closure_Int_ball_not_empty:
assumes "S \ closure T" "x \ S" "r > 0"
shows "T \ ball x r \ {}"
using assms centre_in_ball closure_iff_nhds_not_empty by blast
lemma compact_sup_maxdistance:
fixes S :: "'a::metric_space set"
assumes "compact S"
and "S \ {}"
shows "\x\S. \y\S. \u\S. \v\S. dist u v \ dist x y"
proof -
have "compact (S \ S)"
using \<open>compact S\<close> by (intro compact_Times)
moreover have "S \ S \ {}"
using \<open>S \<noteq> {}\<close> by auto
moreover have "continuous_on (S \ S) (\x. dist (fst x) (snd x))"
by (intro continuous_at_imp_continuous_on ballI continuous_intros)
ultimately show ?thesis
using continuous_attains_sup[of "S \ S" "\x. dist (fst x) (snd x)"] by auto
qed
subsubsection\<open>Totally bounded\<close>
lemma cauchy_def: "Cauchy S \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (S m) (S n) < e)"
unfolding Cauchy_def by metis
proposition seq_compact_imp_totally_bounded:
assumes "seq_compact S"
shows "\e>0. \k. finite k \ k \ S \ S \ (\x\k. ball x e)"
proof -
{ fix e::real assume "e > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x e)"
let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < e))"
have "\x. \n::nat. ?Q x n (x n)"
proof (rule dependent_wellorder_choice)
fix n x assume "\y. y < n \ ?Q x y (x y)"
then have "\ S \ (\x\x ` {0..
using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
then obtain z where z:"z\S" "z \ (\x\x ` {0..
unfolding subset_eq by auto
show "\r. ?Q x n r"
using z by auto
qed simp
then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)"
by blast
then obtain l r where "l \ S" and r:"strict_mono r" and "((x \ r) \ l) sequentially"
using assms by (metis seq_compact_def)
then have "Cauchy (x \ r)"
using LIMSEQ_imp_Cauchy by auto
then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e"
unfolding cauchy_def using \<open>e > 0\<close> by blast
then have False
using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
then show ?thesis
by metis
qed
subsubsection\<open>Heine-Borel theorem\<close>
proposition seq_compact_imp_Heine_Borel:
fixes S :: "'a :: metric_space set"
assumes "seq_compact S"
shows "compact S"
proof -
from seq_compact_imp_totally_bounded[OF \<open>seq_compact S\<close>]
obtain f where f: "\e>0. finite (f e) \ f e \ S \ S \ (\x\f e. ball x e)"
unfolding choice_iff' ..
define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)"
have "countably_compact S"
using \<open>seq_compact S\<close> by (rule seq_compact_imp_countably_compact)
then show "compact S"
proof (rule countably_compact_imp_compact)
show "countable K"
unfolding K_def using f
by (auto intro: countable_finite countable_subset countable_rat
intro!: countable_image countable_SIGMA countable_UN)
show "\b\K. open b" by (auto simp: K_def)
next
fix T x
assume T: "open T" "x \ T" and x: "x \ S"
from openE[OF T] obtain e where "0 < e" "ball x e \ T"
by auto
then have "0 < e/2" "ball x (e/2) \ T"
by auto
from Rats_dense_in_real[OF \<open>0 < e/2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e/2"
by auto
from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> S\<close> obtain k where "k \<in> f r" "x \<in> ball k r"
by auto
from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
by (auto simp: K_def)
then show "\b\K. x \ b \ b \ S \ T"
proof (rule bexI[rotated], safe)
fix y
assume "y \ ball k r"
with \<open>r < e/2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"
by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
with \<open>ball x e \<subseteq> T\<close> show "y \<in> T"
by auto
next
show "x \ ball k r" by fact
qed
qed
qed
proposition compact_eq_seq_compact_metric:
"compact (S :: 'a::metric_space set) \ seq_compact S"
using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast
proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
"compact (S :: 'a::metric_space set) \
(\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
unfolding compact_eq_seq_compact_metric seq_compact_def by auto
subsubsection \<open>Complete the chain of compactness variants\<close>
proposition compact_eq_Bolzano_Weierstrass:
fixes S :: "'a::metric_space set"
shows "compact S \ (\T. infinite T \ T \ S \ (\x \ S. x islimpt T))"
using Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass compact_eq_seq_compact_metric
by blast
proposition Bolzano_Weierstrass_imp_bounded:
"(\T. \infinite T; T \ S\ \ (\x \ S. x islimpt T)) \ bounded S"
using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis
subsection \<open>Banach fixed point theorem\<close>
theorem banach_fix:\<comment> \<open>TODO: rename to \<open>Banach_fix\<close>\<close>
assumes s: "complete s" "s \ {}"
and c: "0 \ c" "c < 1"
and f: "f ` s \ s"
and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y"
shows "\!x\s. f x = x"
proof -
from c have "1 - c > 0" by simp
from s(2) obtain z0 where z0: "z0 \ s" by blast
define z where "z n = (f ^^ n) z0" for n
with f z0 have z_in_s: "z n \ s" for n :: nat
by (induct n) auto
define d where "d = dist (z 0) (z 1)"
have fzn: "f (z n) = z (Suc n)" for n
by (simp add: z_def)
have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat
proof (induct n)
case 0
then show ?case
by (simp add: d_def)
next
case (Suc m)
with \<open>0 \<le> c\<close> have "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp
then show ?case
using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
by (simp add: fzn mult_le_cancel_left)
qed
have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat
proof (induct n)
case 0
show ?case by simp
next
case (Suc k)
from c have "(1 - c) * dist (z m) (z (m + Suc k)) \
(1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"
by (simp add: dist_triangle)
also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"
by simp
also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"
by (simp add: field_simps)
also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"
by (simp add: power_add field_simps)
also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)"
by (simp add: field_simps)
finally show ?case by simp
qed
have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e
proof (cases "d = 0")
case True
from \<open>1 - c > 0\<close> have "(1 - c) * x \<le> 0 \<longleftrightarrow> x \<le> 0" for x
by (simp add: mult_le_0_iff)
with c cf_z2[of 0] True have "z n = z0" for n
by (simp add: z_def)
with \<open>e > 0\<close> show ?thesis by simp
next
case False
with zero_le_dist[of "z 0" "z 1"] have "d > 0"
by (metis d_def less_le)
with \<open>1 - c > 0\<close> \<open>e > 0\<close> have "0 < e * (1 - c) / d"
by simp
with c obtain N where N: "c ^ N < e * (1 - c) / d"
using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto
have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat
proof -
from c \<open>n \<ge> N\<close> have *: "c ^ n \<le> c ^ N"
using power_decreasing[OF \<open>n\<ge>N\<close>, of c] by simp
from c \<open>m > n\<close> have "1 - c ^ (m - n) > 0"
using power_strict_mono[of c 1 "m - n"] by simp
with \<open>d > 0\<close> \<open>0 < 1 - c\<close> have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
by simp
from cf_z2[of n "m - n"] \<open>m > n\<close>
have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
by (simp add: pos_le_divide_eq[OF \<open>1 - c > 0\<close>] mult.commute dist_commute)
also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
using mult_right_mono[OF * order_less_imp_le[OF **]]
by (simp add: mult.assoc)
also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)
also from c \<open>d > 0\<close> \<open>1 - c > 0\<close> have "\<dots> = e * (1 - c ^ (m - n))"
by simp
also from c \<open>1 - c ^ (m - n) > 0\<close> \<open>e > 0\<close> have "\<dots> \<le> e"
using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
finally show ?thesis by simp
qed
have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat
proof (cases "n = m")
case True
with \<open>e > 0\<close> show ?thesis by simp
next
case False
with *[of n m] *[of m n] and that show ?thesis
by (auto simp: dist_commute nat_neq_iff)
qed
then show ?thesis by auto
qed
then have "Cauchy z"
by (simp add: cauchy_def)
then obtain x where "x\s" and x:"(z \ x) sequentially"
using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
define e where "e = dist (f x) x"
have "e = 0"
proof (rule ccontr)
assume "e \ 0"
then have "e > 0"
unfolding e_def using zero_le_dist[of "f x" x]
by (metis dist_eq_0_iff dist_nz e_def)
then obtain N where N:"\n\N. dist (z n) x < e/2"
using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
then have N':"dist (z N) x < e/2" by auto
have *: "c * dist (z N) x \ dist (z N) x"
unfolding mult_le_cancel_right2
using zero_le_dist[of "z N" x] and c
by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
have "dist (f (z N)) (f x) \ c * dist (z N) x"
using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
using z_in_s[of N] \<open>x\<in>s\<close>
using c
by auto
also have "\ < e/2"
using N' and c using * by auto
finally show False
unfolding fzn
using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]
unfolding e_def
by auto
qed
then have "f x = x" by (auto simp: e_def)
moreover have "y = x" if "f y = y" "y \ s" for y
proof -
from \<open>x \<in> s\<close> \<open>f x = x\<close> that have "dist x y \<le> c * dist x y"
using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp
with c and zero_le_dist[of x y] have "dist x y = 0"
by (simp add: mult_le_cancel_right1)
then show ?thesis by simp
qed
ultimately show ?thesis
using \<open>x\<in>s\<close> by blast
qed
subsection \<open>Edelstein fixed point theorem\<close>
theorem Edelstein_fix:
fixes S :: "'a::metric_space set"
assumes S: "compact S" "S \ {}"
and gs: "(g ` S) \ S"
and dist: "\x\S. \y\S. x \ y \ dist (g x) (g y) < dist x y"
shows "\!x\S. g x = x"
proof -
let ?D = "(\x. (x, x)) ` S"
have D: "compact ?D" "?D \ {}"
by (rule compact_continuous_image)
(auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
have "\x y e. x \ S \ y \ S \ 0 < e \ dist y x < e \ dist (g y) (g x) < e"
using dist by fastforce
then have "continuous_on S g"
by (auto simp: continuous_on_iff)
then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))"
unfolding continuous_on_eq_continuous_within
by (intro continuous_dist ballI continuous_within_compose)
(auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)
obtain a where "a \ S" and le: "\x. x \ S \ dist (g a) a \ dist (g x) x"
using continuous_attains_inf[OF D cont] by auto
have "g a = a"
proof (rule ccontr)
assume "g a \ a"
with \<open>a \<in> S\<close> gs have "dist (g (g a)) (g a) < dist (g a) a"
by (intro dist[rule_format]) auto
moreover have "dist (g a) a \ dist (g (g a)) (g a)"
using \<open>a \<in> S\<close> gs by (intro le) auto
ultimately show False by auto
qed
moreover have "\x. x \ S \ g x = x \ x = a"
using dist[THEN bspec[where x=a]] \<open>g a = a\<close> and \<open>a\<in>S\<close> by auto
ultimately show "\!x\S. g x = x"
using \<open>a \<in> S\<close> by blast
qed
subsection \<open>The diameter of a set\<close>
definition\<^marker>\<open>tag important\<close> diameter :: "'a::metric_space set \<Rightarrow> real" where
"diameter S = (if S = {} then 0 else SUP (x,y)\S\S. dist x y)"
lemma diameter_empty [simp]: "diameter{} = 0"
by (auto simp: diameter_def)
lemma diameter_singleton [simp]: "diameter{x} = 0"
by (auto simp: diameter_def)
lemma diameter_le:
assumes "S \ {} \ 0 \ d"
and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d"
shows "diameter S \ d"
using assms
by (auto simp: dist_norm diameter_def intro: cSUP_least)
lemma diameter_bounded_bound:
fixes S :: "'a :: metric_space set"
assumes S: "bounded S" "x \ S" "y \ S"
shows "dist x y \ diameter S"
proof -
from S obtain z d where z: "\x. x \ S \ dist z x \ d"
unfolding bounded_def by auto
have "bdd_above (case_prod dist ` (S\S))"
proof (intro bdd_aboveI, safe)
fix a b
assume "a \ S" "b \ S"
with z[of a] z[of b] dist_triangle[of a b z]
show "dist a b \ 2 * d"
by (simp add: dist_commute)
qed
moreover have "(x,y) \ S\S" using S by auto
ultimately have "dist x y \ (SUP (x,y)\S\S. dist x y)"
by (rule cSUP_upper2) simp
with \<open>x \<in> S\<close> show ?thesis
by (auto simp: diameter_def)
qed
lemma diameter_lower_bounded:
fixes S :: "'a :: metric_space set"
assumes S: "bounded S"
and d: "0 < d" "d < diameter S"
shows "\x\S. \y\S. d < dist x y"
proof (rule ccontr)
assume contr: "\ ?thesis"
moreover have "S \ {}"
using d by (auto simp: diameter_def)
ultimately have "diameter S \ d"
by (auto simp: not_less diameter_def intro!: cSUP_least)
with \<open>d < diameter S\<close> show False by auto
qed
lemma diameter_bounded:
assumes "bounded S"
shows "\x\S. \y\S. dist x y \ diameter S"
and "\d>0. d < diameter S \ (\x\S. \y\S. dist x y > d)"
using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms
by auto
lemma bounded_two_points: "bounded S \ (\e. \x\S. \y\S. dist x y \ e)"
by (meson bounded_def diameter_bounded(1))
lemma diameter_compact_attained:
assumes "compact S"
and "S \ {}"
shows "\x\S. \y\S. dist x y = diameter S"
proof -
have b: "bounded S" using assms(1)
by (rule compact_imp_bounded)
then obtain x y where xys: "x\S" "y\S"
and xy: "\u\S. \v\S. dist u v \ dist x y"
using compact_sup_maxdistance[OF assms] by auto
then have "diameter S \ dist x y"
unfolding diameter_def
apply clarsimp
apply (rule cSUP_least, fast+)
done
then show ?thesis
by (metis b diameter_bounded_bound order_antisym xys)
qed
lemma diameter_ge_0:
assumes "bounded S" shows "0 \ diameter S"
by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)
lemma diameter_subset:
assumes "S \ T" "bounded T"
shows "diameter S \ diameter T"
proof (cases "S = {} \ T = {}")
case True
with assms show ?thesis
by (force simp: diameter_ge_0)
next
case False
then have "bdd_above ((\x. case x of (x, xa) \ dist x xa) ` (T \ T))"
using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
with False \<open>S \<subseteq> T\<close> show ?thesis
apply (simp add: diameter_def)
apply (rule cSUP_subset_mono, auto)
done
qed
lemma diameter_closure:
assumes "bounded S"
shows "diameter(closure S) = diameter S"
proof (rule order_antisym)
have "False" if "diameter S < diameter (closure S)"
proof -
define d where "d = diameter(closure S) - diameter(S)"
have "d > 0"
using that by (simp add: d_def)
then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
by simp
have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
by (simp add: d_def field_split_simps)
have bocl: "bounded (closure S)"
using assms by blast
moreover have "0 \ diameter S"
using assms diameter_ge_0 by blast
ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
then obtain x' y' where x'y': "x' \ S" "dist x' x < d/4" "y' \ S" "dist y' y < d/4"
using closure_approachable
by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
then have "dist x' y' \ diameter S"
using assms diameter_bounded_bound by blast
with x'y' have "dist x y \ d / 4 + diameter S + d / 4"
by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
then show ?thesis
using xy d_def by linarith
qed
then show "diameter (closure S) \ diameter S"
by fastforce
next
show "diameter S \ diameter (closure S)"
by (simp add: assms bounded_closure closure_subset diameter_subset)
qed
proposition Lebesgue_number_lemma:
assumes "compact S" "\ \ {}" "S \ \\" and ope: "\B. B \ \ \ open B"
obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
proof (cases "S = {}")
case True
then show ?thesis
by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
next
case False
{ fix x assume "x \ S"
then obtain C where C: "x \ C" "C \ \"
using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
then obtain r where r: "r>0" "ball x (2*r) \ C"
by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)
then have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \"
using C by blast
}
then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)"
by metis
then have "S \ (\x \ S. ball x (r x))"
by auto
then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
by (rule compactE [OF \<open>compact S\<close>]) auto
then obtain S0 where "S0 \ S" "finite S0" and S0: "\ = (\x. ball x (r x)) ` S0"
by (meson finite_subset_image)
then have "S0 \ {}"
using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
define \<delta> where "\<delta> = Inf (r ` S0)"
have "\ > 0"
using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
show ?thesis
proof
show "0 < \"
by (simp add: \<open>0 < \<delta>\<close>)
show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T
proof (cases "T = {}")
case True
then show ?thesis
using \<open>\<C> \<noteq> {}\<close> by blast
next
case False
then obtain y where "y \ T" by blast
then have "y \ S"
using \<open>T \<subseteq> S\<close> by auto
then obtain x where "x \ S0" and x: "y \ ball x (r x)"
using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
have "ball y \ \ ball y (r x)"
by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)
also have "... \ ball x (2*r x)"
using x by metric
finally obtain C where "C \ \" "ball y \ \ C"
by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
have "bounded T"
using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
then have "T \ ball y \"
using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
then show ?thesis
apply (rule_tac x=C in bexI)
using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
qed
qed
qed
subsection \<open>Metric spaces with the Heine-Borel property\<close>
text \<open>
A metric space (or topological vector space) is said to have the
Heine-Borel property if every closed and bounded subset is compact.
\<close>
class heine_borel = metric_space +
assumes bounded_imp_convergent_subsequence:
"bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially"
proposition bounded_closed_imp_seq_compact:
fixes S::"'a::heine_borel set"
assumes "bounded S"
and "closed S"
shows "seq_compact S"
proof (unfold seq_compact_def, clarify)
fix f :: "nat \ 'a"
assume f: "\n. f n \ S"
with \<open>bounded S\<close> have "bounded (range f)"
by (auto intro: bounded_subset)
obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially"
using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
from f have fr: "\n. (f \ r) n \ S"
by simp
have "l \ S" using \closed S\ fr l
by (rule closed_sequentially)
show "\l\S. \r. strict_mono r \ ((f \ r) \ l) sequentially"
using \<open>l \<in> S\<close> r l by blast
qed
lemma compact_eq_bounded_closed:
fixes S :: "'a::heine_borel set"
shows "compact S \ bounded S \ closed S"
using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed
by auto
lemma compact_Inter:
fixes \<F> :: "'a :: heine_borel set set"
assumes com: "\S. S \ \ \ compact S" and "\ \ {}"
shows "compact(\ \)"
using assms
by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)
lemma compact_closure [simp]:
fixes S :: "'a::heine_borel set"
shows "compact(closure S) \ bounded S"
by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
instance\<^marker>\<open>tag important\<close> real :: heine_borel
proof
fix f :: "nat \ real"
assume f: "bounded (range f)"
obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)"
unfolding comp_def by (metis seq_monosub)
then have "Bseq (f \ r)"
unfolding Bseq_eq_bounded using f
by (metis BseqI' bounded_iff comp_apply rangeI)
with r show "\l r. strict_mono r \ (f \ r) \ l"
using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def)
qed
lemma compact_lemma_general:
fixes f :: "nat \ 'a"
fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60)
fixes unproj:: "('b \ 'c) \ 'a"
assumes finite_basis: "finite basis"
assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)"
assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k"
assumes unproj_proj: "\x. unproj (\k. x proj k) = x"
shows "\d\basis. \l::'a. \ r::nat\nat.
strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
proof safe
fix d :: "'b set"
assume d: "d \ basis"
with finite_basis have "finite d"
by (blast intro: finite_subset)
from this d show "\l::'a. \r::nat\nat. strict_mono r \
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
proof (induct d)
case empty
then show ?case
unfolding strict_mono_def by auto
next
case (insert k d)
have k[intro]: "k \ basis"
using insert by auto
have s': "bounded ((\x. x proj k) ` range f)"
using k
by (rule bounded_proj)
obtain l1::"'a" and r1 where r1: "strict_mono r1"
and lr1: "\e > 0. eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
using insert(3) using insert(4) by auto
have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f"
by simp
have "bounded (range (\i. f (r1 i) proj k))"
by (metis (lifting) bounded_subset f' image_subsetI s')
then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\i. f (r1 (r2 i)) proj k) \ l2) sequentially"
using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"]
by (auto simp: o_def)
define r where "r = r1 \ r2"
have r:"strict_mono r"
using r1 and r2 unfolding r_def o_def strict_mono_def by auto
moreover
define l where "l = unproj (\i. if i = k then l2 else l1 proj i)"
{
fix e::real
assume "e > 0"
from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
by blast
from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"
by (rule tendstoD)
from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"
by (rule eventually_subseq)
have "eventually (\n. \i\(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"
using N1' N2
by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)
}
ultimately show ?case by auto
qed
qed
lemma bounded_fst: "bounded s \ bounded (fst ` s)"
unfolding bounded_def
by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)
lemma bounded_snd: "bounded s \ bounded (snd ` s)"
unfolding bounded_def
by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
instance\<^marker>\<open>tag important\<close> prod :: (heine_borel, heine_borel) heine_borel
proof
fix f :: "nat \ 'a \ 'b"
assume f: "bounded (range f)"
then have "bounded (fst ` range f)"
by (rule bounded_fst)
then have s1: "bounded (range (fst \ f))"
by (simp add: image_comp)
obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1"
using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
from f have s2: "bounded (range (snd \ f \ r1))"
by (auto simp: image_comp intro: bounded_snd bounded_subset)
obtain l2 r2 where r2: "strict_mono r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially"
using bounded_imp_convergent_subsequence [OF s2]
unfolding o_def by fast
have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.72 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
