Theory Elementary_Metric_Spaces
chapter ‹Elementary Metric Spaces›
theory Elementary_Metric_Spaces
imports
Abstract_Topology_2
Metric_Arith
begin
section ‹Open and closed balls›
definition ball :: "'a::metric_space ⇒ real ⇒ 'a set"
where "ball x e = {y. dist x y < e}"
definition cball :: "'a::metric_space ⇒ real ⇒ 'a set"
where "cball x e = {y. dist x y ≤ e}"
definition sphere :: "'a::metric_space ⇒ real ⇒ '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 auto
lemma cball_trivial [simp]: "cball x 0 = {x}"
by auto
lemma sphere_trivial [simp]: "sphere x 0 = {x}"
by auto
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 -` {..<e})"
by (intro open_vimage open_lessThan continuous_intros)
also have "dist x -` {..<e} = ball x e"
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"
by (smt (verit, best) Diff_empty ball_eq_empty cball_diff_sphere centre_in_ball centre_in_cball sphere_empty)
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"
by (smt (verit, best) cball_empty div_by_1 frac_le subset_cball zero_le_divide_iff)
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 *⇩R x) ` cball c r = cball (a *⇩R c :: 'a :: real_normed_vector) (¦a¦ * r)"
proof -
have 1: "(λx. a *⇩R x) ` cball c r ⊆ cball (a *⇩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 *⇩R c) (a *⇩R x) = norm (a *⇩R c - a *⇩R x)"
by (auto simp: dist_norm)
also have "a *⇩R c - a *⇩R x = a *⇩R (c - x)"
by (simp add: algebra_simps)
finally show "a *⇩R x ∈ cball (a *⇩R c) (¦a¦ * r)"
using that x by (auto simp: dist_norm)
qed
have "cball (a *⇩R c) (¦a¦ * r) = (λx. a *⇩R x) ` (λx. inverse a *⇩R x) ` cball (a *⇩R c) (¦a¦ * r)"
unfolding image_image using assms by simp
also have "… ⊆ (λx. a *⇩R x) ` cball (inverse a *⇩R (a *⇩R c)) (¦inverse a¦ * (¦a¦ * r))"
using assms by (intro image_mono 1) auto
also have "… = (λx. a *⇩R x) ` cball c r"
using assms by (simp add: algebra_simps)
finally have "cball (a *⇩R c) (¦a¦ * r) ⊆ (λx. a *⇩R x) ` cball c r" .
moreover from assms have "(λx. a *⇩R x) ` cball c r ⊆ cball (a *⇩R c) (¦a¦ * r)"
by (intro 1) auto
ultimately show ?thesis by blast
qed
lemma ball_scale:
assumes "a ≠ 0"
shows "(λx. a *⇩R x) ` ball c r = ball (a *⇩R c :: 'a :: real_normed_vector) (¦a¦ * r)"
proof -
have 1: "(λx. a *⇩R x) ` ball c r ⊆ ball (a *⇩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 *⇩R c) (a *⇩R x) = norm (a *⇩R c - a *⇩R x)"
by (auto simp: dist_norm)
also have "a *⇩R c - a *⇩R x = a *⇩R (c - x)"
by (simp add: algebra_simps)
finally show "a *⇩R x ∈ ball (a *⇩R c) (¦a¦ * r)"
using that x by (auto simp: dist_norm)
qed
have "ball (a *⇩R c) (¦a¦ * r) = (λx. a *⇩R x) ` (λx. inverse a *⇩R x) ` ball (a *⇩R c) (¦a¦ * r)"
unfolding image_image using assms by simp
also have "… ⊆ (λx. a *⇩R x) ` ball (inverse a *⇩R (a *⇩R c)) (¦inverse a¦ * (¦a¦ * r))"
using assms by (intro image_mono 1) auto
also have "… = (λx. a *⇩R x) ` ball c r"
using assms by (simp add: algebra_simps)
finally have "ball (a *⇩R c) (¦a¦ * r) ⊆ (λx. a *⇩R x) ` ball c r" .
moreover from assms have "(λx. a *⇩R x) ` ball c r ⊆ ball (a *⇩R c) (¦a¦ * r)"
by (intro 1) auto
ultimately show ?thesis by blast
qed
lemma frequently_atE:
fixes x :: "'a :: metric_space"
assumes "frequently P (at x within s)"
shows "∃f. filterlim f (at x within s) sequentially ∧ (∀n. P (f n))"
proof -
have "∃y. y ∈ s ∩ (ball x (1 / real (Suc n)) - {x}) ∧ P y" for n
proof -
have "∃z∈s. z ≠ x ∧ dist z x < (1 / real (Suc n)) ∧ P z"
by (metis assms divide_pos_pos frequently_at of_nat_0_less_iff zero_less_Suc zero_less_one)
then show ?thesis
by (auto simp: dist_commute conj_commute)
qed
then obtain f where f: "⋀n. f n ∈ s ∩ (ball x (1 / real (Suc n)) - {x}) ∧ P (f n)"
by metis
have "filterlim f (nhds x) sequentially"
unfolding tendsto_iff
proof clarify
fix e :: real
assume e: "e > 0"
then obtain n where n: "Suc n > 1 / e"
by (meson le_nat_floor lessI not_le)
have "dist (f k) x < e" if "k ≥ n" for k
proof -
have "dist (f k) x < 1 / real (Suc k)"
using f[of k] by (auto simp: dist_commute)
also have "… ≤ 1 / real (Suc n)"
using that by (intro divide_left_mono) auto
also have "… < e"
using n e by (simp add: field_simps)
finally show ?thesis .
qed
thus "∀⇩F k in sequentially. dist (f k) x < e"
unfolding eventually_at_top_linorder by blast
qed
moreover have "f n ≠ x" for n
using f[of n] by auto
ultimately have "filterlim f (at x within s) sequentially"
using f by (auto simp: filterlim_at)
with f show ?thesis
by blast
qed
section ‹Limit Points›
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"
by (metis islimpt_def islimpt_eq_acc_point mem_Collect_eq)
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))"
unfolding islimpt_eq_acc_point
by (metis open_ball Int_commute Int_mono finite_subset open_contains_ball_eq subset_eq)
lemma islimpt_eq_infinite_cball: "x islimpt S ⟷ (∀e>0. infinite(S ∩ cball x e))"
unfolding islimpt_eq_infinite_ball
by (metis open_ball ball_subset_cball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
section ‹Perfect Metric Spaces›
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"
by (smt (verit, best) open_ball ball_eq_empty ball_subset_cball cball_empty cball_trivial
not_open_singleton subset_singleton_iff)
section ‹Finite and discrete›
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 ‹e0>0› by auto
moreover have "insert x S ⊆ ball a e"
using e0 ‹e>0› 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
by (smt (verit, del_insts) dist_pos_lt insert.IH insert_iff)
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[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
lemma discrete_imp_not_islimpt:
assumes e: "0 < e"
and d: "⋀x y. x ∈ S ⟹ y ∈ S ⟹ dist y x < e ⟹ y = x"
shows "¬ x islimpt S"
proof
assume "x islimpt S"
hence "x islimpt S - {x}"
by (meson islimpt_punctured)
moreover from assms have "closed (S - {x})"
by (intro discrete_imp_closed) auto
ultimately show False
unfolding closed_limpt by blast
qed
section ‹Interior›
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)
lemma ball_iff_cball: "(∃r>0. ball x r ⊆ U) ⟷ (∃r>0. cball x r ⊆ U)"
by (meson mem_interior mem_interior_cball)
section ‹Frontier›
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)
section ‹Limits›
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 ‹Show that they yield usual definitions in the various cases.›
proposition Lim_within_le: "(f ⤏ l)(at a within S) ⟷
(∀e>0. ∃d>0. ∀x∈S. 0 < dist x a ∧ dist x a ≤ d ⟶ dist (f x) l < e)"
by (auto simp: tendsto_iff eventually_at_le)
proposition Lim_within: "(f ⤏ l) (at a within S) ⟷
(∀e >0. ∃d>0. ∀x ∈ S. 0 < dist x a ∧ dist x a < d ⟶ 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)"
unfolding Lim_within by (smt (verit, ccfv_SIG) assms zero_less_dist_iff)
proposition Lim_at: "(f ⤏ l) (at a) ⟷
(∀e >0. ∃d>0. ∀x. 0 < dist x a ∧ dist x a < d ⟶ 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)⟧
⟹ (f ⤏ l) (at a within T)"
by (simp add: eventually_at Lim_within) (smt (verit, best))
text ‹Another limit point characterization.›
lemma limpt_sequential_inj:
fixes x :: "'a::metric_space"
shows "x islimpt S ⟷
(∃f. (∀n::nat. f n ∈ S - {x}) ∧ inj f ∧ (f ⤏ 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"
and fSuc: "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
by (smt (verit, best) fSuc dist_pos_lt inverse_positive_iff_positive y zero_less_power)
qed
show ?rhs
proof (intro exI 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 add: fSuc)
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 ‹m < n› by blast
finally show ?thesis .
next
assume "m = n" then show ?case
by (smt (verit, best) dist_pos_lt f fSuc y)
qed
qed
then show "inj f"
by (metis less_irrefl linorder_injI)
have "⋀e n. ⟦0 < e; nat ⌈1 / e⌉ ≤ n⟧ ⟹ dist (f n) x < e"
apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
by (simp add: divide_simps order_le_less_trans)
then show "f ⇢ x"
using lim_sequentially by blast
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)
section ‹Continuity›
text‹Derive the epsilon-delta forms, which we often use as "definitions"›
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)
by (smt (verit, best) nondecF)
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)
by (smt (verit) nondecF)
text‹Versions in terms of open balls.›
lemma continuous_within_ball:
"continuous (at x within S) f ⟷
(∀e > 0. ∃d > 0. f ` (ball x d ∩ S) ⊆ ball (f x) e)"
(is "?lhs = ?rhs")
proof
assume ?lhs
{
fix e :: real
assume "e > 0"
then obtain d where "d>0" and d: "∀y∈S. 0 < dist y x ∧ dist y x < d ⟶ dist (f y) (f x) < e"
using ‹?lhs›[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 ‹e > 0› by (auto simp: dist_commute)
}
then have "∃d>0. f ` (ball x d ∩ S) ⊆ ball (f x) e"
using ‹d > 0› by blast
}
then show ?rhs by auto
next
assume ?rhs
then show ?lhs
apply (simp add: continuous_within Lim_within ball_def subset_eq)
by (metis (mono_tags, lifting) Int_iff dist_commute mem_Collect_eq)
qed
lemma continuous_at_ball:
"continuous (at x) f ⟷ (∀e>0. ∃d>0. f ` (ball x d) ⊆ ball (f x) e)"
apply (simp add: continuous_at Lim_at subset_eq Ball_def Bex_def image_iff)
by (smt (verit, ccfv_threshold) dist_commute dist_self)
text‹Define setwise continuity in terms of limits within the set.›
lemma continuous_on_iff:
"continuous_on s f ⟷
(∀x∈s. ∀e>0. ∃d>0. ∀x'∈s. dist x' x < d ⟶ 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 unfolding continuous_within_eps_delta
by (metis dense order_le_less_trans)
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‹Some simple consequential lemmas.›
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
unfolding continuous_on_iff by (metis dense order_le_less_trans)
text‹The usual transformation theorems.›
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)
section ‹Closure and Limit Characterization›
lemma closure_approachable:
fixes S :: "'a::metric_space set"
shows "x ∈ closure S ⟷ (∀e>0. ∃y∈S. dist y x < e)"
using dist_self by (force simp: closure_def islimpt_approachable)
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"
using cInf_lessD by blast
with * have "∃x∈S. dist x (Inf S) < e"
using dist_real_def by force
}
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"
using less_cSupE by blast
with * have "∃x∈S. dist x (Sup S) < e"
using dist_real_def by force
}
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 ‹?lhs› 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 ‹?rhs› 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
section ‹Boundedness›
definition (in metric_space) bounded :: "'a set ⇒ 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⇧2 + b⇧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
section ‹Compactness›
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 ‹finite D› have "bounded (⋃x∈D. ball x 1)"
by (simp add: bounded_UN)
then show "bounded U" using ‹U ⊆ (⋃x∈D. ball x 1)›
by (rule bounded_subset)
qed
lemma continuous_on_compact_bound:
assumes "compact A" "continuous_on A f"
obtains B where "B ≥ 0" "⋀x. x ∈ A ⟹ norm (f x) ≤ B"
proof -
have "compact (f ` A)" by (metis assms compact_continuous_image)
then obtain B where "∀x∈A. norm (f x) ≤ B"
by (auto dest!: compact_imp_bounded simp: bounded_iff)
hence "max B 0 ≥ 0" and "∀x∈A. norm (f x) ≤ max B 0" by auto
thus ?thesis using that by blast
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 ‹compact S› by (intro compact_Times)
moreover have "S × S ≠ {}"
using ‹S ≠ {}› 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
text ‹
If ‹A› is a compact subset of an open set ‹B› in a metric space, then there exists an ‹ε > 0›
such that the Minkowski sum of ‹A› with an open ball of radius ‹ε› is also a subset of ‹B›.
›
lemma compact_subset_open_imp_ball_epsilon_subset:
assumes "compact A" "open B" "A ⊆ B"
obtains e where "e > 0" "(⋃x∈A. ball x e) ⊆ B"
proof -
have "∀x∈A. ∃e. e > 0 ∧ ball x e ⊆ B"
using assms unfolding open_contains_ball by blast
then obtain e where e: "⋀x. x ∈ A ⟹ e x > 0" "⋀x. x ∈ A ⟹ ball x (e x) ⊆ B"
by metis
define C where "C = e ` A"
obtain X where X: "X ⊆ A" "finite X" "A ⊆ (⋃c∈X. ball c (e c / 2))"
using assms(1)
proof (rule compactE_image)
show "open (ball x (e x / 2))" if "x ∈ A" for x
by simp
show "A ⊆ (⋃c∈A. ball c (e c / 2))"
using e by auto
qed auto
define e' where "e' = Min (insert 1 ((λx. e x / 2) ` X))"
have "e' > 0"
unfolding e'_def using e X by (subst Min_gr_iff) auto
have e': "e' ≤ e x / 2" if "x ∈ X" for x
using that X unfolding e'_def by (intro Min.coboundedI) auto
show ?thesis
proof
show "e' > 0"
by fact
next
show "(⋃x∈A. ball x e') ⊆ B"
proof clarify
fix x y assume xy: "x ∈ A" "y ∈ ball x e'"
from xy(1) X obtain z where z: "z ∈ X" "x ∈ ball z (e z / 2)"
by auto
have "dist y z ≤ dist x y + dist z x"
by (metis dist_commute dist_triangle)
also have "dist z x < e z / 2"
using xy z by auto
also have "dist x y < e'"
using xy by auto
also have "… ≤ e z / 2"
using z by (intro e') auto
finally have "y ∈ ball z (e z)"
by (simp add: dist_commute)
also have "… ⊆ B"
using z X by (intro e) auto
finally show "y ∈ B" .
qed
qed
qed
lemma compact_subset_open_imp_cball_epsilon_subset:
assumes "compact A" "open B" "A ⊆ B"
obtains e where "e > 0" "(⋃x∈A. cball x e) ⊆ B"
proof -
obtain e where "e > 0" and e: "(⋃x∈A. ball x e) ⊆ B"
using compact_subset_open_imp_ball_epsilon_subset [OF assms] by blast
then have "(⋃x∈A. cball x (e / 2)) ⊆ (⋃x∈A. ball x e)"
by auto
with ‹0 < e› that show ?thesis
by (metis e half_gt_zero_iff order_trans)
qed
subsubsection‹Totally bounded›
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..<n}. ball x e)"
using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
then obtain z where z:"z∈S" "z ∉ (⋃x∈x ` {0..<n}. ball x e)"
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 ‹e > 0› 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‹Heine-Borel theorem›
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 ‹seq_compact S›]
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 ‹seq_compact S› 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 ‹0 < e/2›] obtain r where "r ∈ ℚ" "0 < r" "r < e/2"
by auto
from f[rule_format, of r] ‹0 < r› ‹x ∈ S› obtain k where "k ∈ f r" "x ∈ ball k r"
by auto
from ‹r ∈ ℚ› ‹0 < r› ‹k ∈ f r› have "ball k r ∈ 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 ‹r < e/2› ‹x ∈ ball k r› have "dist x y < e"
by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
with ‹ball x e ⊆ T› show "y ∈ 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:
"compact (S :: 'a::metric_space set) ⟷
(∀f. (∀n. f n ∈ S) ⟶ (∃l∈S. ∃r::nat⇒nat. strict_mono r ∧ (f ∘ r) ⇢ l))"
unfolding compact_eq_seq_compact_metric seq_compact_def by auto
subsubsection ‹Complete the chain of compactness variants›
proposition compact_eq_Bolzano_Weierstrass:
fixes S :: "'a::metric_space set"
shows "compact S ⟷ (∀T. infinite T ∧ T ⊆ S ⟶ (∃x ∈ S. x islimpt T))"
by (meson Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass seq_compact_imp_Heine_Borel)
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
section ‹Banach fixed point theorem›
theorem banach_fix:
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 ‹0 ≤ c› have "c * dist (z m) (z (Suc m)) ≤ 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 ‹1 - c > 0› have "(1 - c) * x ≤ 0 ⟷ x ≤ 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 ‹e > 0› 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 ‹1 - c > 0› ‹e > 0› 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 ‹n ≥ N› have *: "c ^ n ≤ c ^ N"
using power_decreasing[OF ‹n≥N›, of c] by simp
from c ‹m > n› have "1 - c ^ (m - n) > 0"
using power_strict_mono[of c 1 "m - n"] by simp
with ‹d > 0› ‹0 < 1 - c› have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
by simp
from cf_z2[of n "m - n"] ‹m > n›
have "dist (z m) (z n) ≤ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
by (simp add: pos_le_divide_eq[OF ‹1 - c > 0›] 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 ‹d > 0› ‹1 - c > 0› have "… = e * (1 - c ^ (m - n))"
by simp
also from c ‹1 - c ^ (m - n) > 0› ‹e > 0› have "… ≤ 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 ‹e > 0› 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 (metis metric_CauchyI)
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] ‹x∈s›
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 ‹x ∈ s› ‹f x = x› that have "dist x y ≤ 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 ‹x∈s› by blast
qed
section ‹Edelstein fixed point theorem›
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 ‹a ∈ S› 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 ‹a ∈ S› 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]] ‹g a = a› and ‹a∈S› by auto
ultimately show "∃!x∈S. g x = x"
using ‹a ∈ S› by blast
qed
section ‹The diameter of a set›
definition diameter :: "'a::metric_space set ⇒ 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 ‹x ∈ S› 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 ‹d < diameter S› 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 by (force intro!: cSUP_least)
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 ‹bounded T› diameter_bounded_bound by (force simp: bdd_above_def)
with False ‹S ⊆ T› 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 d_less_d: "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 dle: "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"
by (smt (verit) dle d_less_d d_def dd diameter_lower_bounded)
then obtain x' y' where x'y': "x' ∈ S" "dist x' x < d/4" "y' ∈ S" "dist y' y < d/4"
by (metis ‹0 < d› zero_less_divide_iff zero_less_numeral closure_approachable)
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 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 δ where "0 < δ" "⋀T. ⟦T ⊆ S; diameter T < δ⟧ ⟹ ∃B ∈ 𝒞. T ⊆ B"
proof (cases "S = {}")
case True
then show ?thesis
by (metis ‹𝒞 ≠ {}› 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 ‹S ⊆ ⋃𝒞› 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 𝒯 where "finite 𝒯" "S ⊆ ⋃𝒯" and 𝒯: "𝒯 ⊆ (λx. ball x (r x)) ` S"
by (rule compactE [OF ‹compact S›]) 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 ‹S ⊆ ⋃𝒯› by auto
define δ where "δ = Inf (r ` S0)"
have "δ > 0"
using ‹finite S0› ‹S0 ⊆ S› ‹S0 ≠ {}› r by (auto simp: δ_def finite_less_Inf_iff)
show ?thesis
proof
show "0 < δ"
by (simp add: ‹0 < δ›)
show "∃B ∈ 𝒞. T ⊆ B" if "T ⊆ S" and dia: "diameter T < δ" for T
proof (cases "T = {}")
case True
then show ?thesis
using ‹𝒞 ≠ {}› by blast
next
case False
then obtain y where "y ∈ T" by blast
then have "y ∈ S"
using ‹T ⊆ S› by auto
then obtain x where "x ∈ S0" and x: "y ∈ ball x (r x)"
using ‹S ⊆ ⋃𝒯› S0 that by blast
have "ball y δ ⊆ ball y (r x)"
by (metis δ_def ‹S0 ≠ {}› ‹finite S0› ‹x ∈ S0› 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 ‹S0 ⊆ S› ‹x ∈ S0› dual_order.trans subsetCE)
have "bounded T"
using ‹compact S› bounded_subset compact_imp_bounded ‹T ⊆ S› by blast
then have "T ⊆ ball y δ"
using ‹y ∈ T› dia diameter_bounded_bound by fastforce
then show ?thesis
by (meson ‹C ∈ 𝒞› ‹ball y δ ⊆ C› subset_eq)
qed
qed
qed
section ‹Metric spaces with the Heine-Borel property›
text ‹
A metric space (or topological vector space) is said to have the
Heine-Borel property if every closed and bounded subset is compact.
›
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 ‹bounded S› 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 ‹bounded (range f)›] by auto
from f have fr: "∀n. (f ∘ r) n ∈ S"
by simp
show "∃l∈S. ∃r. strict_mono r ∧ (f ∘ r) ⇢ l"
using assms(2) closed_sequentially fr l r 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 bounded_infinite_imp_islimpt:
fixes S :: "'a::heine_borel set"
assumes "T ⊆ S" "bounded S" "infinite T"
obtains x where "x islimpt S"
by (meson assms closed_limpt compact_eq_Bolzano_Weierstrass compact_eq_bounded_closed islimpt_subset)
lemma compact_Inter:
fixes ℱ :: "'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 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 by (metis f 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 ∧ (∀e>0. eventually (λn. ∀i∈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 ∧
(∀e>0. eventually (λn. ∀i∈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. ∀⇩F n in sequentially. ∀i∈d. dist (f (r1 n) proj i) (l1 proj i) < e"
using insert 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"
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 ‹e > 0› have N1: "∀⇩F n in sequentially. ∀i∈d. dist (f (r1 n) proj i) (l1 proj i) < e"
by blast
from lr2 ‹e > 0› have N2: "∀⇩F n in sequentially. dist (f (r1 (r2 n)) proj k) l2 < e"
by (rule tendstoD)
from r2 N1 have N1': "∀⇩F n in sequentially. ∀i∈d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e"
by (rule eventually_subseq)
have "∀⇩F n in sequentially. ∀i∈insert k d. dist (f (r n) proj i) (l proj i) < e"
using N1' N2
by eventually_elim (use insert.prems in ‹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, opaque_lifting) dist_fst_le image_iff order_trans)
lemma bounded_snd: "bounded s ⟹ bounded (snd ` s)"
unfolding bounded_def
by (metis (no_types, opaque_lifting) dist_snd_le image_iff order.trans)
instance 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"
using bounded_imp_convergent_subsequence [OF s2]
unfolding o_def by fast
have l1': "((λn. fst (f (r1 (r2 n)))) ⤏ l1) sequentially"
using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
have l: "((f ∘ (r1 ∘ r2)) ⤏ (l1, l2)) sequentially"
using tendsto_Pair [OF l1' l2] unfolding o_def by simp
have r: "strict_mono (r1 ∘ r2)"
using r1 r2 unfolding strict_mono_def by simp
show "∃l r. strict_mono r ∧ ((f ∘ r) ⤏ l) sequentially"
using l r by fast
qed
section ‹Completeness›
proposition (in metric_space) completeI:
assumes "⋀f. ∀n. f n ∈ s ⟹ Cauchy f ⟹ ∃l∈s. f ⇢ l"
shows "complete s"
using assms unfolding complete_def by fast
proposition (in metric_space) completeE:
assumes "complete s" and "∀n. f n ∈ s" and "Cauchy f"
obtains l where "l ∈ s" and "f ⇢ l"
using assms unfolding complete_def by fast
lemma compact_imp_complete:
fixes s :: "'a::metric_space set"
assumes "compact s"
shows "complete s"
proof -
{
fix f
assume as: "(∀n::nat. f n ∈ s)" "Cauchy f"
from as(1) obtain l r where lr: "l∈s" "strict_mono r" "(f ∘ r) ⇢ l"
using assms unfolding compact_def by blast
note lr' = seq_suble [OF lr(2)]
{
fix e :: real
assume "e > 0"
from as(2) obtain N where N:"∀m n. N ≤ m ∧ N ≤ n ⟶ dist (f m) (f n) < e/2"
unfolding Cauchy_def using ‹e > 0› by (meson half_gt_zero)
then obtain M where M:"∀n≥M. dist ((f ∘ r) n) l < e/2"
by (metis dist_self lim_sequentially lr(3))
{
fix n :: nat
assume n: "n ≥ max N M"
have "dist ((f ∘ r) n) l < e/2"
using n M by auto
moreover have "r n ≥ N"
using lr'[of n] n by auto
then have "dist (f n) ((f ∘ r) n) < e/2"
using N and n by auto
ultimately have "dist (f n) l < e" using n M
by metric
}
then have "∃N. ∀n≥N. dist (f n) l < e" by blast
}
then have "∃l∈s. (f ⤏ l) sequentially" using ‹l∈s›
unfolding lim_sequentially by auto
}
then show ?thesis unfolding complete_def by auto
qed
proposition compact_eq_totally_bounded:
"compact s ⟷ complete s ∧ (∀e>0. ∃k. finite k ∧ s ⊆ (⋃x∈k. ball x e))"
(is "_ ⟷ ?rhs")
proof
assume assms: "?rhs"
then obtain k where k: "⋀e. 0 < e ⟹ finite (k e)" "⋀e. 0 < e ⟹ s ⊆ (⋃x∈k e. ball x e)"
by (auto simp: choice_iff')
show "compact s"
proof cases
assume "s = {}"
then show "compact s" by (simp add: compact_def)
next
assume "s ≠ {}"
show ?thesis
unfolding compact_def
proof safe
fix f :: "nat ⇒ 'a"
assume f: "∀n. f n ∈ s"
define e where "e n = 1 / (2 * Suc n)" for n
then have [simp]: "⋀n. 0 < e n" by auto
define B where "B n U = (SOME b. infinite {n. f n ∈ b} ∧ (∃x. b ⊆ ball x (e n) ∩ U))" for n U
{
fix n U
assume "infinite {n. f n ∈ U}"
then have "∃b∈k (e n). infinite {i∈{n. f n ∈ U}. f i ∈ ball b (e n)}"
using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
then obtain a where
"a ∈ k (e n)"
"infinite {i ∈ {n. f n ∈ U}. f i ∈ ball a (e n)}" ..
then have "∃b. infinite {i. f i ∈ b} ∧ (∃x. b ⊆ ball x (e n) ∩ U)"
by (intro exI[of _ "ball a (e n) ∩ U"] exI[of _ a]) (auto simp: ac_simps)
from someI_ex[OF this]
have "infinite {i. f i ∈ B n U}" "∃x. B n U ⊆ ball x (e n) ∩ U"
unfolding B_def by auto
}
note B = this
define F where "F = rec_nat (B 0 UNIV) B"
{
fix n
have "infinite {i. f i ∈ F n}"
by (induct n) (auto simp: F_def B)
}
then have F: "⋀n. ∃x. F (Suc n) ⊆ ball x (e n) ∩ F n"
using B by (simp add: F_def)
then have F_dec: "⋀m n. m ≤ n ⟹ F n ⊆ F m"
using decseq_SucI[of F] by (auto simp: decseq_def)
obtain sel where sel: "⋀k i. i < sel k i" "⋀k i. f (sel k i) ∈ F k"
proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)
fix k i
have "infinite ({n. f n ∈ F k} - {.. i})"
using ‹infinite {n. f n ∈ F k}› by auto
from infinite_imp_nonempty[OF this]
show "∃x>i. f x ∈ F k"
by (simp add: set_eq_iff not_le conj_commute)
qed
define t where "t = rec_nat (sel 0 0) (λn i. sel (Suc n) i)"
have "strict_mono t"
unfolding strict_mono_Suc_iff by (simp add: t_def sel)
moreover have "∀i. (f ∘ t) i ∈ s"
using f by auto
moreover
have t: "(f ∘ t) n ∈ F n" for n
by (cases n) (simp_all add: t_def sel)
have "Cauchy (f ∘ t)"
proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
fix r :: real and N n m
assume "1 / Suc N < r" "Suc N ≤ n" "Suc N ≤ m"
then have "(f ∘ t) n ∈ F (Suc N)" "(f ∘ t) m ∈ F (Suc N)" "2 * e N < r"
using F_dec t by (auto simp: e_def field_simps)
with F[of N] obtain x where "dist x ((f ∘ t) n) < e N" "dist x ((f ∘ t) m) < e N"
by (auto simp: subset_eq)
with ‹2 * e N < r› show "dist ((f ∘ t) m) ((f ∘ t) n) < r"
by metric
qed
ultimately show "∃l∈s. ∃r. strict_mono r ∧ (f ∘ r) ⇢ l"
using assms unfolding complete_def by blast
qed
qed
qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
lemma cauchy_imp_bounded:
assumes "Cauchy s"
shows "bounded (range s)"
proof -
from assms obtain N :: nat where "∀m n. N ≤ m ∧ N ≤ n ⟶ dist (s m) (s n) < 1"
by (meson Cauchy_def zero_less_one)
then have N:"∀n. N ≤ n ⟶ dist (s N) (s n) < 1" by auto
moreover
have "bounded (s ` {0..N})"
using finite_imp_bounded[of "s ` {1..N}"] by auto
then obtain a where a:"∀x∈s ` {0..N}. dist (s N) x ≤ a"
unfolding bounded_any_center [where a="s N"] by auto
ultimately show "?thesis"
unfolding bounded_any_center [where a="s N"]
apply (rule_tac x="max a 1" in exI, auto)
apply (erule_tac x=y in allE)
apply (erule_tac x=y in ballE, auto)
done
qed
instance heine_borel < complete_space
proof
fix f :: "nat ⇒ 'a" assume "Cauchy f"
then show "convergent f"
unfolding convergent_def
using Cauchy_converges_subseq cauchy_imp_bounded bounded_imp_convergent_subsequence by blast
qed
lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"
proof (rule completeI)
fix f :: "nat ⇒ 'a" assume "Cauchy f"
then show "∃l∈UNIV. f ⇢ l"
using Cauchy_convergent convergent_def by blast
qed
lemma complete_imp_closed:
fixes S :: "'a::metric_space set"
shows "complete S ⟹ closed S"
by (metis LIMSEQ_imp_Cauchy LIMSEQ_unique closed_sequential_limits completeE)
lemma complete_Int_closed:
fixes S :: "'a::metric_space set"
assumes "complete S" and "closed t"
shows "complete (S ∩ t)"
by (metis Int_iff assms closed_sequentially completeE completeI)
lemma complete_closed_subset:
fixes S :: "'a::metric_space set"
assumes "closed S" and "S ⊆ t" and "complete t"
shows "complete S"
using assms complete_Int_closed [of t S] by (simp add: Int_absorb1)
lemma complete_eq_closed:
fixes S :: "('a::complete_space) set"
shows "complete S ⟷ closed S"
proof
assume "closed S" then show "complete S"
using subset_UNIV complete_UNIV by (rule complete_closed_subset)
next
assume "complete S" then show "closed S"
by (rule complete_imp_closed)
qed
lemma convergent_eq_Cauchy:
fixes S :: "nat ⇒ 'a::complete_space"
shows "(∃l. (S ⤏ l) sequentially) ⟷ Cauchy S"
unfolding Cauchy_convergent_iff convergent_def ..
lemma convergent_imp_bounded:
fixes S :: "nat ⇒ 'a::metric_space"
shows "(S ⤏ l) sequentially ⟹ bounded (range S)"
by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
lemma frontier_subset_compact:
fixes S :: "'a::heine_borel set"
shows "compact S ⟹ frontier S ⊆ S"
using frontier_subset_closed compact_eq_bounded_closed
by blast
lemma banach_fix_type:
fixes f::"'a::complete_space⇒'a"
assumes c:"0 ≤ c" "c < 1"
and lipschitz:"∀x. ∀y. dist (f x) (f y) ≤ c * dist x y"
shows "∃!x. (f x = x)"
using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
by auto
section ‹Cauchy continuity›
definition Cauchy_continuous_on where
"Cauchy_continuous_on ≡ λS f. ∀σ. Cauchy σ ⟶ range σ ⊆ S ⟶ Cauchy (f ∘ σ)"
lemma continuous_closed_imp_Cauchy_continuous:
fixes S :: "('a::complete_space) set"
shows "⟦continuous_on S f; closed S⟧ ⟹ Cauchy_continuous_on S f"
unfolding Cauchy_continuous_on_def
by (metis LIMSEQ_imp_Cauchy completeE complete_eq_closed continuous_on_sequentially range_subsetD)
lemma uniformly_continuous_imp_Cauchy_continuous:
fixes f :: "'a::metric_space ⇒ 'b::metric_space"
shows "uniformly_continuous_on S f ⟹ Cauchy_continuous_on S f"
by (simp add: uniformly_continuous_on_def Cauchy_continuous_on_def Cauchy_def image_subset_iff) metis
lemma Cauchy_continuous_on_imp_continuous:
fixes f :: "'a::metric_space ⇒ 'b::metric_space"
assumes "Cauchy_continuous_on S f"
shows "continuous_on S f"
proof -
have False if x: "∀n. ∃x'∈S. dist x' x < inverse(Suc n) ∧ ¬ dist (f x') (f x) < ε" "ε>0" "x ∈ S" for x and ε::real
proof -
obtain ρ where ρ: "∀n. ρ n ∈ S" and dx: "∀n. dist (ρ n) x < inverse(Suc n)" and dfx: "∀n. ¬ dist (f (ρ n)) (f x) < ε"
using x by metis
define σ where "σ ≡ λn. if even n then ρ n else x"
with ρ ‹x ∈ S› have "range σ ⊆ S"
by auto
have "σ ⇢ x"
unfolding tendsto_iff
proof (intro strip)
fix e :: real
assume "e>0"
then obtain N where "inverse (Suc N) < e"
using reals_Archimedean by blast
then have "∀n. N ≤ n ⟶ dist (ρ n) x < e"
by (smt (verit, ccfv_SIG) dx inverse_Suc inverse_less_iff_less inverse_positive_iff_positive of_nat_Suc of_nat_mono)
with ‹e>0› show "∀⇩F n in sequentially. dist (σ n) x < e"
by (auto simp add: eventually_sequentially σ_def)
qed
then have "Cauchy σ"
by (intro LIMSEQ_imp_Cauchy)
then have Cf: "Cauchy (f ∘ σ)"
by (meson Cauchy_continuous_on_def ‹range σ ⊆ S› assms)
have "(f ∘ σ) ⇢ f x"
unfolding tendsto_iff
proof (intro strip)
fix e :: real
assume "e>0"
then obtain N where N: "∀m≥N. ∀n≥N. dist ((f ∘ σ) m) ((f ∘ σ) n) < e"
using Cf unfolding Cauchy_def by presburger
moreover have "(f ∘ σ) (Suc(N+N)) = f x"
by (simp add: σ_def)
ultimately have "∀n≥N. dist ((f ∘ σ) n) (f x) < e"
by (metis add_Suc le_add2)
then show "∀⇩F n in sequentially. dist ((f ∘ σ) n) (f x) < e"
using eventually_sequentially by blast
qed
moreover have "⋀n. ¬ dist (f (σ (2*n))) (f x) < ε"
using dfx by (simp add: σ_def)
ultimately show False
using ‹ε>0› by (fastforce simp: mult_2 nat_le_iff_add tendsto_iff eventually_sequentially)
qed
then show ?thesis
unfolding continuous_on_iff by (meson inverse_Suc)
qed
section‹ Finite intersection property›
text‹Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.›
lemma closed_imp_fip:
fixes S :: "'a::heine_borel set"
assumes "closed S"
and T: "T ∈ ℱ" "bounded T"
and clof: "⋀T. T ∈ ℱ ⟹ closed T"
and "⋀ℱ'. ⟦finite ℱ'; ℱ' ⊆ ℱ⟧ ⟹ S ∩ ⋂ℱ' ≠ {}"
shows "S ∩ ⋂ℱ ≠ {}"
proof -
have "compact (S ∩ T)"
using ‹closed S› clof compact_eq_bounded_closed T by blast
then have "(S ∩ T) ∩ ⋂ℱ ≠ {}"
by (smt (verit, best) Inf_insert Int_assoc assms compact_imp_fip finite_insert insert_subset)
then show ?thesis by blast
qed
lemma closed_imp_fip_compact:
fixes S :: "'a::heine_borel set"
shows
"⟦closed S; ⋀T. T ∈ ℱ ⟹ compact T;
⋀ℱ'. ⟦finite ℱ'; ℱ' ⊆ ℱ⟧ ⟹ S ∩ ⋂ℱ' ≠ {}⟧
⟹ S ∩ ⋂ℱ ≠ {}"
by (metis closed_imp_fip compact_eq_bounded_closed equals0I finite.emptyI order.refl)
lemma closed_fip_Heine_Borel:
fixes ℱ :: "'a::heine_borel set set"
assumes "T ∈ ℱ" "bounded T"
and "⋀T. T ∈ ℱ ⟹ closed T"
and "⋀ℱ'. ⟦finite ℱ'; ℱ' ⊆ ℱ⟧ ⟹ ⋂ℱ' ≠ {}"
shows "⋂ℱ ≠ {}"
using closed_imp_fip [OF closed_UNIV] assms by auto
lemma compact_fip_Heine_Borel:
fixes ℱ :: "'a::heine_borel set set"
assumes clof: "⋀T. T ∈ ℱ ⟹ compact T"
and none: "⋀ℱ'. ⟦finite ℱ'; ℱ' ⊆ ℱ⟧ ⟹ ⋂ℱ' ≠ {}"
shows "⋂ℱ ≠ {}"
by (metis InterI clof closed_fip_Heine_Borel compact_eq_bounded_closed equals0D none)
lemma compact_sequence_with_limit:
fixes f :: "nat ⇒ 'a::heine_borel"
shows "f ⇢ l ⟹ compact (insert l (range f))"
by (simp add: closed_limpt compact_eq_bounded_closed convergent_imp_bounded islimpt_insert sequence_unique_limpt)
section ‹Properties of Balls and Spheres›
lemma compact_cball[simp]:
fixes x :: "'a::heine_borel"
shows "compact (cball x e)"
using compact_eq_bounded_closed bounded_cball closed_cball by blast
lemma compact_frontier_bounded[intro]:
fixes S :: "'a::heine_borel set"
shows "bounded S ⟹ compact (frontier S)"
unfolding frontier_def
using compact_eq_bounded_closed by blast
lemma compact_frontier[intro]:
fixes S :: "'a::heine_borel set"
shows "compact S ⟹ compact (frontier S)"
using compact_eq_bounded_closed compact_frontier_bounded by blast
lemma no_limpt_imp_countable:
assumes "⋀z. ¬z islimpt (X :: 'a :: {real_normed_vector, heine_borel} set)"
shows "countable X"
proof -
have "countable (⋃n. cball 0 (real n) ∩ X)"
proof (intro countable_UN[OF _ countable_finite])
fix n :: nat
show "finite (cball 0 (real n) ∩ X)"
using assms by (intro finite_not_islimpt_in_compact) auto
qed auto
also have "(⋃n. cball 0 (real n)) = (UNIV :: 'a set)"
by (force simp: real_arch_simple)
hence "(⋃n. cball 0 (real n) ∩ X) = X"
by blast
finally show "countable X" .
qed
section ‹Distance from a Set›
lemma distance_attains_sup:
assumes "compact s" "s ≠ {}"
shows "∃x∈s. ∀y∈s. dist a y ≤ dist a x"
proof (rule continuous_attains_sup [OF assms])
{
fix x
assume "x∈s"
have "(dist a ⤏ dist a x) (at x within s)"
by (intro tendsto_dist tendsto_const tendsto_ident_at)
}
then show "continuous_on s (dist a)"
unfolding continuous_on ..
qed
text ‹For \emph{minimal} distance, we only need closure, not compactness.›
lemma distance_attains_inf:
fixes a :: "'a::heine_borel"
assumes "closed s" and "s ≠ {}"
obtains x where "x∈s" "⋀y. y ∈ s ⟹ dist a x ≤ dist a y"
proof -
from assms obtain b where "b ∈ s" by auto
let ?B = "s ∩ cball a (dist b a)"
have "?B ≠ {}" using ‹b ∈ s›
by (auto simp: dist_commute)
moreover have "continuous_on ?B (dist a)"
by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
moreover have "compact ?B"
by (intro closed_Int_compact ‹closed s› compact_cball)
ultimately obtain x where "x ∈ ?B" "∀y∈?B. dist a x ≤ dist a y"
by (metis continuous_attains_inf)
with that show ?thesis by fastforce
qed
section ‹Infimum Distance›
definition "infdist x A = (if A = {} then 0 else INF a∈A. dist x a)"
lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
by (auto intro!: zero_le_dist)
lemma infdist_notempty: "A ≠ {} ⟹ infdist x A = (INF a∈A. dist x a)"
by (simp add: infdist_def)
lemma infdist_nonneg: "0 ≤ infdist x A"
by (auto simp: infdist_def intro: cINF_greatest)
lemma infdist_le: "a ∈ A ⟹ infdist x A ≤ dist x a"
by (auto intro: cINF_lower simp add: infdist_def)
lemma infdist_le2: "a ∈ A ⟹ dist x a ≤ d ⟹ infdist x A ≤ d"
by (auto intro!: cINF_lower2 simp add: infdist_def)
lemma infdist_zero[simp]: "a ∈ A ⟹ infdist a A = 0"
by (auto intro!: antisym infdist_nonneg infdist_le2)
lemma infdist_Un_min:
assumes "A ≠ {}" "B ≠ {}"
shows "infdist x (A ∪ B) = min (infdist x A) (infdist x B)"
using assms by (simp add: infdist_def cINF_union inf_real_def)
lemma infdist_triangle: "infdist x A ≤ infdist y A + dist x y"
proof (cases "A = {}")
case True
then show ?thesis by (simp add: infdist_def)
next
case False
then obtain a where "a ∈ A" by auto
have "infdist x A ≤ Inf {dist x y + dist y a |a. a ∈ A}"
proof (rule cInf_greatest)
from ‹A ≠ {}› show "{dist x y + dist y a |a. a ∈ A} ≠ {}"
by simp
fix d
assume "d ∈ {dist x y + dist y a |a. a ∈ A}"
then obtain a where d: "d = dist x y + dist y a" "a ∈ A"
by auto
show "infdist x A ≤ d"
unfolding infdist_notempty[OF ‹A ≠ {}›]
proof (rule cINF_lower2)
show "a ∈ A" by fact
show "dist x a ≤ d"
unfolding d by (rule dist_triangle)
qed simp
qed
also have "… = dist x y + infdist y A"
proof (rule cInf_eq, safe)
fix a
assume "a ∈ A"
then show "dist x y + infdist y A ≤ dist x y + dist y a"
by (auto intro: infdist_le)
next
fix i
assume inf: "⋀d. d ∈ {dist x y + dist y a |a. a ∈ A} ⟹ i ≤ d"
then have "i - dist x y ≤ infdist y A"
unfolding infdist_notempty[OF ‹A ≠ {}›] using ‹a ∈ A›
by (intro cINF_greatest) (auto simp: field_simps)
then show "i ≤ dist x y + infdist y A"
by simp
qed
finally show ?thesis by simp
qed
lemma infdist_triangle_abs: "¦infdist x A - infdist y A¦ ≤ dist x y"
by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)
lemma in_closure_iff_infdist_zero:
assumes "A ≠ {}"
shows "x ∈ closure A ⟷ infdist x A = 0"
proof
assume "x ∈ closure A"
show "infdist x A = 0"
proof (rule ccontr)
assume "infdist x A ≠ 0"
with infdist_nonneg[of x A] have "infdist x A > 0"
by auto
then have "ball x (infdist x A) ∩ closure A = {}"
by (smt (verit, best) ‹x ∈ closure A› closure_approachableD infdist_le)
then have "x ∉ closure A"
by (metis ‹0 < infdist x A› centre_in_ball disjoint_iff_not_equal)
then show False using ‹x ∈ closure A› by simp
qed
next
assume x: "infdist x A = 0"
then obtain a where "a ∈ A"
by atomize_elim (metis all_not_in_conv assms)
have False if "e > 0" "¬ (∃y∈A. dist y x < e)" for e
proof -
have "infdist x A ≥ e" using ‹a ∈ A›
unfolding infdist_def using that
by (force simp: dist_commute intro: cINF_greatest)
with x ‹e > 0› show False by auto
qed
then show "x ∈ closure A"
using closure_approachable by blast
qed
lemma in_closed_iff_infdist_zero:
assumes "closed A" "A ≠ {}"
shows "x ∈ A ⟷ infdist x A = 0"
proof -
have "x ∈ closure A ⟷ infdist x A = 0"
by (simp add: ‹A ≠ {}› in_closure_iff_infdist_zero)
with assms show ?thesis by simp
qed
lemma infdist_pos_not_in_closed:
assumes "closed S" "S ≠ {}" "x ∉ S"
shows "infdist x S > 0"
by (smt (verit, best) assms in_closed_iff_infdist_zero infdist_nonneg)
lemma
infdist_attains_inf:
fixes X::"'a::heine_borel set"
assumes "closed X"
assumes "X ≠ {}"
obtains x where "x ∈ X" "infdist y X = dist y x"
proof -
have "bdd_below (dist y ` X)"
by auto
from distance_attains_inf[OF assms, of y]
obtain x where "x ∈ X" "⋀z. z ∈ X ⟹ dist y x ≤ dist y z" by auto
then have "infdist y X = dist y x"
by (metis antisym assms(2) cINF_greatest infdist_def infdist_le)
with ‹x ∈ X› show ?thesis ..
qed
text ‹Every metric space is a T4 space:›
instance metric_space ⊆ t4_space
proof
fix S T::"'a set" assume H: "closed S" "closed T" "S ∩ T = {}"
consider "S = {}" | "T = {}" | "S ≠ {} ∧ T ≠ {}" by auto
then show "∃U V. open U ∧ open V ∧ S ⊆ U ∧ T ⊆ V ∧ U ∩ V = {}"
proof (cases)
case 1 then show ?thesis by blast
next
case 2 then show ?thesis by blast
next
case 3
define U where "U = (⋃x∈S. ball x ((infdist x T)/2))"
have A: "open U" unfolding U_def by auto
have "infdist x T > 0" if "x ∈ S" for x
using H that 3 by (auto intro!: infdist_pos_not_in_closed)
then have B: "S ⊆ U" unfolding U_def by auto
define V where "V = (⋃x∈T. ball x ((infdist x S)/2))"
have C: "open V" unfolding V_def by auto
have "infdist x S > 0" if "x ∈ T" for x
using H that 3 by (auto intro!: infdist_pos_not_in_closed)
then have D: "T ⊆ V" unfolding V_def by auto
have "(ball x ((infdist x T)/2)) ∩ (ball y ((infdist y S)/2)) = {}" if "x ∈ S" "y ∈ T" for x y
proof auto
fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
have "2 * dist x y ≤ 2 * dist x z + 2 * dist y z"
by metric
also have "... < infdist x T + infdist y S"
using H by auto
finally have "dist x y < infdist x T ∨ dist x y < infdist y S"
by auto
then show False
using infdist_le[OF ‹x ∈ S›, of y] infdist_le[OF ‹y ∈ T›, of x] by (auto simp add: dist_commute)
qed
then have E: "U ∩ V = {}"
unfolding U_def V_def by auto
show ?thesis
using A B C D E by blast
qed
qed
lemma tendsto_infdist [tendsto_intros]:
assumes f: "(f ⤏ l) F"
shows "((λx. infdist (f x) A) ⤏ infdist l A) F"
proof (rule tendstoI)
fix e ::real
assume "e > 0"
from tendstoD[OF f this]
show "eventually (λx. dist (infdist (f x) A) (infdist l A) < e) F"
proof (eventually_elim)
fix x
from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
have "dist (infdist (f x) A) (infdist l A) ≤ dist (f x) l"
by (simp add: dist_commute dist_real_def)
also assume "dist (f x) l < e"
finally show "dist (infdist (f x) A) (infdist l A) < e" .
qed
qed
lemma continuous_infdist[continuous_intros]:
assumes "continuous F f"
shows "continuous F (λx. infdist (f x) A)"
using assms unfolding continuous_def by (rule tendsto_infdist)
lemma continuous_on_infdist [continuous_intros]:
assumes "continuous_on S f"
shows "continuous_on S (λx. infdist (f x) A)"
using assms unfolding continuous_on by (auto intro: tendsto_infdist)
lemma compact_infdist_le:
fixes A::"'a::heine_borel set"
assumes "A ≠ {}"
assumes "compact A"
assumes "e > 0"
shows "compact {x. infdist x A ≤ e}"
proof -
from continuous_closed_vimage[of "{0..e}" "λx. infdist x A"]
continuous_infdist[OF continuous_ident, of _ UNIV A]
have "closed {x. infdist x A ≤ e}" by (auto simp: vimage_def infdist_nonneg)
moreover
from assms obtain x0 b where b: "⋀x. x ∈ A ⟹ dist x0 x ≤ b" "closed A"
by (auto simp: compact_eq_bounded_closed bounded_def)
{
fix y
assume "infdist y A ≤ e"
moreover
from infdist_attains_inf[OF ‹closed A› ‹A ≠ {}›, of y]
obtain z where "z ∈ A" "infdist y A = dist y z" by blast
ultimately
have "dist x0 y ≤ b + e" using b by metric
} then
have "bounded {x. infdist x A ≤ e}"
by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
ultimately show "compact {x. infdist x A ≤ e}"
by (simp add: compact_eq_bounded_closed)
qed
section ‹Separation between Points and Sets›
proposition separate_point_closed:
fixes S :: "'a::heine_borel set"
assumes "closed S" and "a ∉ S"
shows "∃d>0. ∀x∈S. d ≤ dist a x"
by (metis assms distance_attains_inf empty_iff gt_ex zero_less_dist_iff)
proposition separate_compact_closed:
fixes S T :: "'a::heine_borel set"
assumes "compact S"
and T: "closed T" "S ∩ T = {}"
shows "∃d>0. ∀x∈S. ∀y∈T. d ≤ dist x y"
proof cases
assume "S ≠ {} ∧ T ≠ {}"
then have "S ≠ {}" "T ≠ {}" by auto
let ?inf = "λx. infdist x T"
have "continuous_on S ?inf"
by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
then obtain x where x: "x ∈ S" "∀y∈S. ?inf x ≤ ?inf y"
using continuous_attains_inf[OF ‹compact S› ‹S ≠ {}›] by auto
then have "0 < ?inf x"
using T ‹T ≠ {}› in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)
moreover have "∀x'∈S. ∀y∈T. ?inf x ≤ dist x' y"
using x by (auto intro: order_trans infdist_le)
ultimately show ?thesis by auto
qed (auto intro!: exI[of _ 1])
proposition separate_closed_compact:
fixes S T :: "'a::heine_borel set"
assumes S: "closed S"
and T: "compact T"
and dis: "S ∩ T = {}"
shows "∃d>0. ∀x∈S. ∀y∈T. d ≤ dist x y"
by (metis separate_compact_closed[OF T S] dis dist_commute inf_commute)
proposition compact_in_open_separated:
fixes A::"'a::heine_borel set"
assumes A: "A ≠ {}" "compact A"
assumes "open B"
assumes "A ⊆ B"
obtains e where "e > 0" "{x. infdist x A ≤ e} ⊆ B"
proof atomize_elim
have "closed (- B)" "compact A" "- B ∩ A = {}"
using assms by (auto simp: open_Diff compact_eq_bounded_closed)
from separate_closed_compact[OF this]
obtain d'::real where d': "d'>0" "⋀x y. x ∉ B ⟹ y ∈ A ⟹ d' ≤ dist x y"
by auto
define d where "d = d' / 2"
hence "d>0" "d < d'" using d' by auto
with d' have d: "⋀x y. x ∉ B ⟹ y ∈ A ⟹ d < dist x y"
by force
show "∃e>0. {x. infdist x A ≤ e} ⊆ B"
proof (rule ccontr)
assume "∄e. 0 < e ∧ {x. infdist x A ≤ e} ⊆ B"
with ‹d > 0› obtain x where x: "infdist x A ≤ d" "x ∉ B"
by auto
then show False
by (metis A compact_eq_bounded_closed infdist_attains_inf x d linorder_not_less)
qed
qed
section ‹Uniform Continuity›
lemma uniformly_continuous_onE:
assumes "uniformly_continuous_on s f" "0 < e"
obtains d where "d>0" "⋀x x'. ⟦x∈s; x'∈s; dist x' x < d⟧ ⟹ dist (f x') (f x) < e"
using assms
by (auto simp: uniformly_continuous_on_def)
lemma uniformly_continuous_on_sequentially:
"uniformly_continuous_on s f ⟷ (∀x y. (∀n. x n ∈ s) ∧ (∀n. y n ∈ s) ∧
(λn. dist (x n) (y n)) ⇢ 0 ⟶ (λn. dist (f(x n)) (f(y n))) ⇢ 0)" (is "?lhs = ?rhs")
proof
assume ?lhs
{
fix x y
assume x: "∀n. x n ∈ s"
and y: "∀n. y n ∈ s"
and xy: "((λn. dist (x n) (y n)) ⤏ 0) sequentially"
{
fix e :: real
assume "e > 0"
then obtain d where "d > 0" and d: "∀x∈s. ∀x'∈s. dist x' x < d ⟶ dist (f x') (f x) < e"
by (metis ‹?lhs› uniformly_continuous_onE)
obtain N where N: "∀n≥N. dist (x n) (y n) < d"
using xy[unfolded lim_sequentially dist_norm] and ‹d>0› by auto
then have "∃N. ∀n≥N. dist (f (x n)) (f (y n)) < e"
using d x y by blast
}
then have "((λn. dist (f(x n)) (f(y n))) ⤏ 0) sequentially"
unfolding lim_sequentially and dist_real_def by auto
}
then show ?rhs by auto
next
assume ?rhs
{
assume "¬ ?lhs"
then obtain e where "e > 0" "∀d>0. ∃x∈s. ∃x'∈s. dist x' x < d ∧ ¬ dist (f x') (f x) < e"
unfolding uniformly_continuous_on_def by auto
then obtain fa where fa:
"∀x. 0 < x ⟶ fst (fa x) ∈ s ∧ snd (fa x) ∈ s ∧ dist (fst (fa x)) (snd (fa x)) < x ∧ ¬ dist (f (fst (fa x))) (f (snd (fa x))) < e"
using choice[of "λd x. d>0 ⟶ fst x ∈ s ∧ snd x ∈ s ∧ dist (snd x) (fst x) < d ∧ ¬ dist (f (snd x)) (f (fst x)) < e"]
by (auto simp: Bex_def dist_commute)
define x where "x n = fst (fa (inverse (real n + 1)))" for n
define y where "y n = snd (fa (inverse (real n + 1)))" for n
have xyn: "∀n. x n ∈ s ∧ y n ∈ s"
and xy0: "∀n. dist (x n) (y n) < inverse (real n + 1)"
and fxy:"∀n. ¬ dist (f (x n)) (f (y n)) < e"
unfolding x_def and y_def using fa
by auto
{
fix e :: real
assume "e > 0"
then obtain N :: nat where "N ≠ 0" and N: "0 < inverse (real N) ∧ inverse (real N) < e"
unfolding real_arch_inverse[of e] by auto
then have "∃N. ∀n≥N. dist (x n) (y n) < e"
by (smt (verit, ccfv_SIG) inverse_le_imp_le nat_le_real_less of_nat_le_0_iff xy0)
}
then have "∀e>0. ∃N. ∀n≥N. dist (f (x n)) (f (y n)) < e"
using ‹?rhs›[THEN spec[where x=x], THEN spec[where x=y]] and xyn
unfolding lim_sequentially dist_real_def by auto
then have False using fxy and ‹e>0› by auto
}
then show ?lhs
unfolding uniformly_continuous_on_def by blast
qed
section ‹Continuity on a Compact Domain Implies Uniform Continuity›
text‹From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)›
lemma Heine_Borel_lemma:
assumes "compact S" and Ssub: "S ⊆ ⋃𝒢" and opn: "⋀G. G ∈ 𝒢 ⟹ open G"
obtains e where "0 < e" "⋀x. x ∈ S ⟹ ∃G ∈ 𝒢. ball x e ⊆ G"
proof -
have False if neg: "⋀e. 0 < e ⟹ ∃x ∈ S. ∀G ∈ 𝒢. ¬ ball x e ⊆ G"
proof -
have "∃x ∈ S. ∀G ∈ 𝒢. ¬ ball x (1 / Suc n) ⊆ G" for n
using neg by simp
then obtain f where "⋀n. f n ∈ S" and fG: "⋀G n. G ∈ 𝒢 ⟹ ¬ ball (f n) (1 / Suc n) ⊆ G"
by metis
then obtain l r where "l ∈ S" "strict_mono r" and to_l: "(f ∘ r) ⇢ l"
using ‹compact S› compact_def that by metis
then obtain G where "l ∈ G" "G ∈ 𝒢"
using Ssub by auto
then obtain e where "0 < e" and e: "⋀z. dist z l < e ⟹ z ∈ G"
using opn open_dist by blast
obtain N1 where N1: "⋀n. n ≥ N1 ⟹ dist (f (r n)) l < e/2"
using to_l apply (simp add: lim_sequentially)
using ‹0 < e› half_gt_zero that by blast
obtain N2 where N2: "of_nat N2 > 2/e"
using reals_Archimedean2 by blast
obtain x where "x ∈ ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x ∉ G"
using fG [OF ‹G ∈ 𝒢›, of "r (max N1 N2)"] by blast
then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))"
by simp
also have "... ≤ 1 / real (Suc (max N1 N2))"
by (meson Suc_le_mono ‹strict_mono r› inverse_of_nat_le nat.discI seq_suble)
also have "... ≤ 1 / real (Suc N2)"
by (simp add: field_simps)
also have "... < e/2"
using N2 ‹0 < e› by (simp add: field_simps)
finally have "dist (f (r (max N1 N2))) x < e/2" .
moreover have "dist (f (r (max N1 N2))) l < e/2"
using N1 max.cobounded1 by blast
ultimately have "dist x l < e"
by metric
then show ?thesis
using e ‹x ∉ G› by blast
qed
then show ?thesis
by (meson that)
qed
lemma compact_uniformly_equicontinuous:
assumes "compact S"
and cont: "⋀x e. ⟦x ∈ S; 0 < e⟧
⟹ ∃d. 0 < d ∧
(∀f ∈ ℱ. ∀x' ∈ S. dist x' x < d ⟶ dist (f x') (f x) < e)"
and "0 < e"
obtains d where "0 < d"
"⋀f x x'. ⟦f ∈ ℱ; x ∈ S; x' ∈ S; dist x' x < d⟧ ⟹ dist (f x') (f x) < e"
proof -
obtain d where d_pos: "⋀x e. ⟦x ∈ S; 0 < e⟧ ⟹ 0 < d x e"
and d_dist : "⋀x x' e f. ⟦dist x' x < d x e; x ∈ S; x' ∈ S; 0 < e; f ∈ ℱ⟧ ⟹ dist (f x') (f x) < e"
using cont by metis
let ?𝒢 = "((λx. ball x (d x (e/2))) ` S)"
have Ssub: "S ⊆ ⋃ ?𝒢"
using ‹0 < e› d_pos by auto
then obtain k where "0 < k" and k: "⋀x. x ∈ S ⟹ ∃G ∈ ?𝒢. ball x k ⊆ G"
by (rule Heine_Borel_lemma [OF ‹compact S›]) auto
moreover have "dist (f v) (f u) < e" if "f ∈ ℱ" "u ∈ S" "v ∈ S" "dist v u < k" for f u v
proof -
obtain G where "G ∈ ?𝒢" "u ∈ G" "v ∈ G"
using k that
by (metis ‹dist v u < k› ‹u ∈ S› ‹0 < k› centre_in_ball subsetD dist_commute mem_ball)
then obtain w where w: "dist w u < d w (e/2)" "dist w v < d w (e/2)" "w ∈ S"
by auto
with that d_dist have "dist (f w) (f v) < e/2"
by (metis ‹0 < e› dist_commute half_gt_zero)
moreover
have "dist (f w) (f u) < e/2"
using that d_dist w by (metis ‹0 < e› dist_commute divide_pos_pos zero_less_numeral)
ultimately show ?thesis
using dist_triangle_half_r by blast
qed
ultimately show ?thesis using that by blast
qed
corollary compact_uniformly_continuous:
fixes f :: "'a :: metric_space ⇒ 'b :: metric_space"
assumes f: "continuous_on S f" and S: "compact S"
shows "uniformly_continuous_on S f"
using f
unfolding continuous_on_iff uniformly_continuous_on_def
by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
section‹ Theorems relating continuity and uniform continuity to closures›
lemma continuous_on_closure:
"continuous_on (closure S) f ⟷
(∀x e. x ∈ closure S ∧ 0 < e
⟶ (∃d. 0 < d ∧ (∀y. y ∈ S ∧ dist y x < d ⟶ dist (f y) (f x) < e)))"
(is "?lhs = ?rhs")
proof
assume ?lhs then show ?rhs
unfolding continuous_on_iff by (metis Un_iff closure_def)
next
assume R [rule_format]: ?rhs
show ?lhs
proof
fix x and e::real
assume "0 < e" and x: "x ∈ closure S"
obtain δ::real where "δ > 0"
and δ: "⋀y. ⟦y ∈ S; dist y x < δ⟧ ⟹ dist (f y) (f x) < e/2"
using R [of x "e/2"] ‹0 < e› x by auto
have "dist (f y) (f x) ≤ e" if y: "y ∈ closure S" and dyx: "dist y x < δ/2" for y
proof -
obtain δ'::real where "δ' > 0"
and δ': "⋀z. ⟦z ∈ S; dist z y < δ'⟧ ⟹ dist (f z) (f y) < e/2"
using R [of y "e/2"] ‹0 < e› y by auto
obtain z where "z ∈ S" and z: "dist z y < min δ' δ / 2"
using closure_approachable y
by (metis ‹0 < δ'› ‹0 < δ› divide_pos_pos min_less_iff_conj zero_less_numeral)
have "dist (f z) (f y) < e/2"
using δ' [OF ‹z ∈ S›] z ‹0 < δ'› by metric
moreover have "dist (f z) (f x) < e/2"
using δ[OF ‹z ∈ S›] z dyx by metric
ultimately show ?thesis
by metric
qed
then show "∃d>0. ∀x'∈closure S. dist x' x < d ⟶ dist (f x') (f x) ≤ e"
by (rule_tac x="δ/2" in exI) (simp add: ‹δ > 0›)
qed
qed
lemma continuous_on_closure_sequentially:
fixes f :: "'a::metric_space ⇒ 'b :: metric_space"
shows
"continuous_on (closure S) f ⟷
(∀x a. a ∈ closure S ∧ (∀n. x n ∈ S) ∧ x ⇢ a ⟶ (f ∘ x) ⇢ f a)"
(is "?lhs = ?rhs")
proof -
have "continuous_on (closure S) f ⟷
(∀x ∈ closure S. continuous (at x within S) f)"
by (force simp: continuous_on_closure continuous_within_eps_delta)
also have "... = ?rhs"
by (force simp: continuous_within_sequentially)
finally show ?thesis .
qed
lemma uniformly_continuous_on_closure:
fixes f :: "'a::metric_space ⇒ 'b::metric_space"
assumes ucont: "uniformly_continuous_on S f"
and cont: "continuous_on (closure S) f"
shows "uniformly_continuous_on (closure S) f"
unfolding uniformly_continuous_on_def
proof (intro allI impI)
fix e::real
assume "0 < e"
then obtain d::real
where "d>0"
and d: "⋀x x'. ⟦x∈S; x'∈S; dist x' x < d⟧ ⟹ dist (f x') (f x) < e/3"
using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto
show "∃d>0. ∀x∈closure S. ∀x'∈closure S. dist x' x < d ⟶ dist (f x') (f x) < e"
proof (rule exI [where x="d/3"], clarsimp simp: ‹d > 0›)
fix x y
assume x: "x ∈ closure S" and y: "y ∈ closure S" and dyx: "dist y x * 3 < d"
obtain d1::real where "d1 > 0"
and d1: "⋀w. ⟦w ∈ closure S; dist w x < d1⟧ ⟹ dist (f w) (f x) < e/3"
using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] ‹0 < e› x by auto
obtain x' where "x' ∈ S" and x': "dist x' x < min d1 (d / 3)"
using closure_approachable [of x S]
by (metis ‹0 < d1› ‹0 < d› divide_pos_pos min_less_iff_conj x zero_less_numeral)
obtain d2::real where "d2 > 0"
and d2: "∀w ∈ closure S. dist w y < d2 ⟶ dist (f w) (f y) < e/3"
using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] ‹0 < e› y by auto
obtain y' where "y' ∈ S" and y': "dist y' y < min d2 (d / 3)"
using closure_approachable [of y S]
by (metis ‹0 < d2› ‹0 < d› divide_pos_pos min_less_iff_conj y zero_less_numeral)
have "dist x' x < d/3" using x' by auto
then have "dist x' y' < d"
using dyx y' by metric
then have "dist (f x') (f y') < e/3"
by (rule d [OF ‹y' ∈ S› ‹x' ∈ S›])
moreover have "dist (f x') (f x) < e/3" using ‹x' ∈ S› closure_subset x' d1
by (simp add: closure_def)
moreover have "dist (f y') (f y) < e/3" using ‹y' ∈ S› closure_subset y' d2
by (simp add: closure_def)
ultimately show "dist (f y) (f x) < e" by metric
qed
qed
lemma uniformly_continuous_on_extension_at_closure:
fixes f::"'a::metric_space ⇒ 'b::complete_space"
assumes uc: "uniformly_continuous_on X f"
assumes "x ∈ closure X"
obtains l where "(f ⤏ l) (at x within X)"
proof -
from assms obtain xs where xs: "xs ⇢ x" "⋀n. xs n ∈ X"
by (auto simp: closure_sequential)
from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs]
obtain l where l: "(λn. f (xs n)) ⇢ l"
by atomize_elim (simp only: convergent_eq_Cauchy)
have "(f ⤏ l) (at x within X)"
proof (safe intro!: Lim_within_LIMSEQ)
fix xs'
assume "∀n. xs' n ≠ x ∧ xs' n ∈ X"
and xs': "xs' ⇢ x"
then have "xs' n ≠ x" "xs' n ∈ X" for n by auto
from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF ‹xs' ⇢ x› ‹xs' _ ∈ X›]
obtain l' where l': "(λn. f (xs' n)) ⇢ l'"
by atomize_elim (simp only: convergent_eq_Cauchy)
show "(λn. f (xs' n)) ⇢ l"
proof (rule tendstoI)
fix e::real assume "e > 0"
define e' where "e' ≡ e/2"
have "e' > 0" using ‹e > 0› by (simp add: e'_def)
have "∀⇩F n in sequentially. dist (f (xs n)) l < e'"
by (simp add: ‹0 < e'› l tendstoD)
moreover
from uc[unfolded uniformly_continuous_on_def, rule_format, OF ‹e' > 0›]
obtain d where d: "d > 0" "⋀x x'. x ∈ X ⟹ x' ∈ X ⟹ dist x x' < d ⟹ dist (f x) (f x') < e'"
by auto
have "∀⇩F n in sequentially. dist (xs n) (xs' n) < d"
by (auto intro!: ‹0 < d› order_tendstoD tendsto_eq_intros xs xs')
ultimately
show "∀⇩F n in sequentially. dist (f (xs' n)) l < e"
proof eventually_elim
case (elim n)
have "dist (f (xs' n)) l ≤ dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l"
by metric
also have "dist (f (xs n)) (f (xs' n)) < e'"
by (auto intro!: d xs ‹xs' _ ∈ _› elim)
also note ‹dist (f (xs n)) l < e'›
also have "e' + e' = e" by (simp add: e'_def)
finally show ?case by simp
qed
qed
qed
thus ?thesis ..
qed
lemma uniformly_continuous_on_extension_on_closure:
fixes f::"'a::metric_space ⇒ 'b::complete_space"
assumes uc: "uniformly_continuous_on X f"
obtains g where "uniformly_continuous_on (closure X) g" "⋀x. x ∈ X ⟹ f x = g x"
"⋀Y h x. X ⊆ Y ⟹ Y ⊆ closure X ⟹ continuous_on Y h ⟹ (⋀x. x ∈ X ⟹ f x = h x) ⟹ x ∈ Y ⟹ h x = g x"
proof -
from uc have cont_f: "continuous_on X f"
by (simp add: uniformly_continuous_imp_continuous)
obtain y where y: "(f ⤏ y x) (at x within X)" if "x ∈ closure X" for x
using uniformly_continuous_on_extension_at_closure[OF assms] by meson
let ?g = "λx. if x ∈ X then f x else y x"
have "uniformly_continuous_on (closure X) ?g"
unfolding uniformly_continuous_on_def
proof safe
fix e::real assume "e > 0"
define e' where "e' ≡ e / 3"
have "e' > 0" using ‹e > 0› by (simp add: e'_def)
from uc[unfolded uniformly_continuous_on_def, rule_format, OF ‹0 < e'›]
obtain d where "d > 0" and d: "⋀x x'. x ∈ X ⟹ x' ∈ X ⟹ dist x' x < d ⟹ dist (f x') (f x) < e'"
by auto
define d' where "d' = d / 3"
have "d' > 0" using ‹d > 0› by (simp add: d'_def)
show "∃d>0. ∀x∈closure X. ∀x'∈closure X. dist x' x < d ⟶ dist (?g x') (?g x) < e"
proof (safe intro!: exI[where x=d'] ‹d' > 0›)
fix x x' assume x: "x ∈ closure X" and x': "x' ∈ closure X" and dist: "dist x' x < d'"
then obtain xs xs' where xs: "xs ⇢ x" "⋀n. xs n ∈ X"
and xs': "xs' ⇢ x'" "⋀n. xs' n ∈ X"
by (auto simp: closure_sequential)
have "∀⇩F n in sequentially. dist (xs' n) x' < d'"
and "∀⇩F n in sequentially. dist (xs n) x < d'"
by (auto intro!: ‹0 < d'› order_tendstoD tendsto_eq_intros xs xs')
moreover
have "(λx. f (xs x)) ⇢ y x" if "x ∈ closure X" "x ∉ X" "xs ⇢ x" "⋀n. xs n ∈ X" for xs x
using that not_eventuallyD
by (force intro!: filterlim_compose[OF y[OF ‹x ∈ closure X›]] simp: filterlim_at)
then have "(λx. f (xs' x)) ⇢ ?g x'" "(λx. f (xs x)) ⇢ ?g x"
using x x'
by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs)
then have "∀⇩F n in sequentially. dist (f (xs' n)) (?g x') < e'"
"∀⇩F n in sequentially. dist (f (xs n)) (?g x) < e'"
by (auto intro!: ‹0 < e'› order_tendstoD tendsto_eq_intros)
ultimately
have "∀⇩F n in sequentially. dist (?g x') (?g x) < e"
proof eventually_elim
case (elim n)
have "dist (?g x') (?g x) ≤
dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)"
by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le)
also
from ‹dist (xs' n) x' < d'› ‹dist x' x < d'› ‹dist (xs n) x < d'›
have "dist (xs' n) (xs n) < d" unfolding d'_def by metric
with ‹xs _ ∈ X› ‹xs' _ ∈ X› have "dist (f (xs' n)) (f (xs n)) < e'"
by (rule d)
also note ‹dist (f (xs' n)) (?g x') < e'›
also note ‹dist (f (xs n)) (?g x) < e'›
finally show ?case by (simp add: e'_def)
qed
then show "dist (?g x') (?g x) < e" by simp
qed
qed
moreover have "f x = ?g x" if "x ∈ X" for x using that by simp
moreover
{
fix Y h x
assume Y: "x ∈ Y" "X ⊆ Y" "Y ⊆ closure X" and cont_h: "continuous_on Y h"
and extension: "(⋀x. x ∈ X ⟹ f x = h x)"
{
assume "x ∉ X"
have "x ∈ closure X" using Y by auto
then obtain xs where xs: "xs ⇢ x" "⋀n. xs n ∈ X"
by (auto simp: closure_sequential)
from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
have hx: "(λx. f (xs x)) ⇢ h x"
by (auto simp: subsetD extension)
then have "(λx. f (xs x)) ⇢ y x"
using ‹x ∉ X› not_eventuallyD xs(2)
by (force intro!: filterlim_compose[OF y[OF ‹x ∈ closure X›]] simp: filterlim_at xs)
with hx have "h x = y x" by (rule LIMSEQ_unique)
} then
have "h x = ?g x"
using extension by auto
}
ultimately show ?thesis ..
qed
lemma bounded_uniformly_continuous_image:
fixes f :: "'a :: heine_borel ⇒ 'b :: heine_borel"
assumes "uniformly_continuous_on S f" "bounded S"
shows "bounded(f ` S)"
by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
section ‹With Abstract Topology (TODO: move and remove dependency?)›
lemma openin_contains_ball:
"openin (top_of_set T) S ⟷
S ⊆ T ∧ (∀x ∈ S. ∃e. 0 < e ∧ ball x e ∩ T ⊆ S)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (metis IntD2 Int_commute Int_lower1 Int_mono inf.idem openE openin_open)
next
assume ?rhs
then show ?lhs
by (smt (verit) open_ball Int_commute Int_iff centre_in_ball in_mono openin_open_Int openin_subopen)
qed
lemma openin_contains_cball:
"openin (top_of_set T) S ⟷
S ⊆ T ∧ (∀x ∈ S. ∃e. 0 < e ∧ cball x e ∩ T ⊆ S)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (force simp add: openin_contains_ball intro: exI [where x="_/2"])
next
assume ?rhs
then show ?lhs
by (force simp add: openin_contains_ball)
qed
section ‹Closed Nest›
text ‹Bounded closed nest property (proof does not use Heine-Borel)›
lemma bounded_closed_nest:
fixes S :: "nat ⇒ ('a::heine_borel) set"
assumes "⋀n. closed (S n)"
and "⋀n. S n ≠ {}"
and "⋀m n. m ≤ n ⟹ S n ⊆ S m"
and "bounded (S 0)"
obtains a where "⋀n. a ∈ S n"
proof -
from assms(2) obtain x where x: "∀n. x n ∈ S n"
using choice[of "λn x. x ∈ S n"] by auto
from assms(4,1) have "seq_compact (S 0)"
by (simp add: bounded_closed_imp_seq_compact)
then obtain l r where lr: "l ∈ S 0" "strict_mono r" "(x ∘ r) ⇢ l"
using x and assms(3) unfolding seq_compact_def by blast
have "∀n. l ∈ S n"
proof
fix n :: nat
have "closed (S n)"
using assms(1) by simp
moreover have "∀i. (x ∘ r) i ∈ S i"
using x and assms(3) and lr(2) [THEN seq_suble] by auto
then have "∀i. (x ∘ r) (i + n) ∈ S n"
using assms(3) by (fast intro!: le_add2)
moreover have "(λi. (x ∘ r) (i + n)) ⇢ l"
using lr(3) by (rule LIMSEQ_ignore_initial_segment)
ultimately show "l ∈ S n"
by (metis closed_sequentially)
qed
then show ?thesis
using that by blast
qed
text ‹Decreasing case does not even need compactness, just completeness.›
lemma decreasing_closed_nest:
fixes S :: "nat ⇒ ('a::complete_space) set"
assumes "⋀n. closed (S n)"
"⋀n. S n ≠ {}"
"⋀m n. m ≤ n ⟹ S n ⊆ S m"
"⋀e. e>0 ⟹ ∃n. ∀x∈S n. ∀y∈S n. dist x y < e"
obtains a where "⋀n. a ∈ S n"
proof -
obtain t where t: "∀n. t n ∈ S n"
by (meson assms(2) equals0I)
{
fix e :: real
assume "e > 0"
then obtain N where N: "∀x∈S N. ∀y∈S N. dist x y < e"
using assms(4) by blast
{
fix m n :: nat
assume "N ≤ m ∧ N ≤ n"
then have "t m ∈ S N" "t n ∈ S N"
using assms(3) t unfolding subset_eq t by blast+
then have "dist (t m) (t n) < e"
using N by auto
}
then have "∃N. ∀m n. N ≤ m ∧ N ≤ n ⟶ dist (t m) (t n) < e"
by auto
}
then have "Cauchy t"
by (metis metric_CauchyI)
then obtain l where l:"(t ⤏ l) sequentially"
using complete_UNIV unfolding complete_def by auto
{ fix n :: nat
{ fix e :: real
assume "e > 0"
then obtain N :: nat where N: "∀n≥N. dist (t n) l < e"
using l[unfolded lim_sequentially] by auto
have "t (max n N) ∈ S n"
by (meson assms(3) contra_subsetD max.cobounded1 t)
then have "∃y∈S n. dist y l < e"
using N max.cobounded2 by blast
}
then have "l ∈ S n"
using closed_approachable[of "S n" l] assms(1) by auto
}
then show ?thesis
using that by blast
qed
text ‹Strengthen it to the intersection actually being a singleton.›
lemma decreasing_closed_nest_sing:
fixes S :: "nat ⇒ 'a::complete_space set"
assumes "⋀n. closed(S n)"
"⋀n. S n ≠ {}"
"⋀m n. m ≤ n ⟹ S n ⊆ S m"
"⋀e. e>0 ⟹ ∃n. ∀x ∈ (S n). ∀ y∈(S n). dist x y < e"
shows "∃a. ⋂(range S) = {a}"
proof -
obtain a where a: "∀n. a ∈ S n"
using decreasing_closed_nest[of S] using assms by auto
{ fix b
assume b: "b ∈ ⋂(range S)"
{ fix e :: real
assume "e > 0"
then have "dist a b < e"
using assms(4) and b and a by blast
}
then have "dist a b = 0"
by (metis dist_eq_0_iff dist_nz less_le)
}
with a have "⋂(range S) = {a}"
unfolding image_def by auto
then show ?thesis ..
qed
section ‹Making a continuous function avoid some value in a neighbourhood›
lemma continuous_within_avoid:
fixes f :: "'a::metric_space ⇒ 'b::t1_space"
assumes "continuous (at x within s) f"
and "f x ≠ a"
shows "∃e>0. ∀y ∈ s. dist x y < e --> f y ≠ a"
proof -
obtain U where "open U" and "f x ∈ U" and "a ∉ U"
using t1_space [OF ‹f x ≠ a›] by fast
have "(f ⤏ f x) (at x within s)"
using assms(1) by (simp add: continuous_within)
then have "eventually (λy. f y ∈ U) (at x within s)"
using ‹open U› and ‹f x ∈ U›
unfolding tendsto_def by fast
then have "eventually (λy. f y ≠ a) (at x within s)"
using ‹a ∉ U› by (fast elim: eventually_mono)
then show ?thesis
using ‹f x ≠ a› by (auto simp: dist_commute eventually_at)
qed
lemma continuous_at_avoid:
fixes f :: "'a::metric_space ⇒ 'b::t1_space"
assumes "continuous (at x) f"
and "f x ≠ a"
shows "∃e>0. ∀y. dist x y < e ⟶ f y ≠ a"
using assms continuous_within_avoid[of x UNIV f a] by simp
lemma continuous_on_avoid:
fixes f :: "'a::metric_space ⇒ 'b::t1_space"
assumes "continuous_on s f"
and "x ∈ s"
and "f x ≠ a"
shows "∃e>0. ∀y ∈ s. dist x y < e ⟶ f y ≠ a"
using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x],
OF assms(2)] continuous_within_avoid[of x s f a]
using assms(3)
by auto
lemma continuous_on_open_avoid:
fixes f :: "'a::metric_space ⇒ 'b::t1_space"
assumes "continuous_on s f"
and "open s"
and "x ∈ s"
and "f x ≠ a"
shows "∃e>0. ∀y. dist x y < e ⟶ f y ≠ a"
using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)]
using continuous_at_avoid[of x f a] assms(4)
by auto
section ‹Consequences for Real Numbers›
lemma closed_contains_Inf:
fixes S :: "real set"
shows "S ≠ {} ⟹ bdd_below S ⟹ closed S ⟹ Inf S ∈ S"
by (metis closure_contains_Inf closure_closed)
lemma closed_subset_contains_Inf:
fixes A C :: "real set"
shows "closed C ⟹ A ⊆ C ⟹ A ≠ {} ⟹ bdd_below A ⟹ Inf A ∈ C"
by (metis closure_contains_Inf closure_minimal subset_eq)
lemma closed_contains_Sup:
fixes S :: "real set"
shows "S ≠ {} ⟹ bdd_above S ⟹ closed S ⟹ Sup S ∈ S"
by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
lemma closed_subset_contains_Sup:
fixes A C :: "real set"
shows "closed C ⟹ A ⊆ C ⟹ A ≠ {} ⟹ bdd_above A ⟹ Sup A ∈ C"
by (metis closure_contains_Sup closure_minimal subset_eq)
lemma atLeastAtMost_subset_contains_Inf:
fixes A :: "real set" and a b :: real
shows "A ≠ {} ⟹ a ≤ b ⟹ A ⊆ {a..b} ⟹ Inf A ∈ {a..b}"
by (rule closed_subset_contains_Inf)
(auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a])
lemma bounded_real: "bounded (S::real set) ⟷ (∃a. ∀x∈S. ¦x¦ ≤ a)"
by (simp add: bounded_iff)
lemma bounded_imp_bdd_above: "bounded S ⟹ bdd_above (S :: real set)"
by (auto simp: bounded_def bdd_above_def dist_real_def)
(metis abs_le_D1 abs_minus_commute diff_le_eq)
lemma bounded_imp_bdd_below: "bounded S ⟹ bdd_below (S :: real set)"
by (auto simp: bounded_def bdd_below_def dist_real_def)
(metis abs_le_D1 add.commute diff_le_eq)
lemma bounded_norm_le_SUP_norm:
"bounded (range f) ⟹ norm (f x) ≤ (SUP x. norm (f x))"
by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
lemma bounded_has_Sup:
fixes S :: "real set"
assumes "bounded S"
and "S ≠ {}"
shows "∀x∈S. x ≤ Sup S"
and "∀b. (∀x∈S. x ≤ b) ⟶ Sup S ≤ b"
proof
show "∀b. (∀x∈S. x ≤ b) ⟶ Sup S ≤ b"
using assms by (metis cSup_least)
qed (metis cSup_upper assms(1) bounded_imp_bdd_above)
lemma Sup_insert:
fixes S :: "real set"
shows "bounded S ⟹ Sup (insert x S) = (if S = {} then x else max x (Sup S))"
by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If)
lemma bounded_has_Inf:
fixes S :: "real set"
assumes "bounded S"
and "S ≠ {}"
shows "∀x∈S. x ≥ Inf S"
and "∀b. (∀x∈S. x ≥ b) ⟶ Inf S ≥ b"
proof
show "∀b. (∀x∈S. x ≥ b) ⟶ Inf S ≥ b"
using assms by (metis cInf_greatest)
qed (metis cInf_lower assms(1) bounded_imp_bdd_below)
lemma Inf_insert:
fixes S :: "real set"
shows "bounded S ⟹ Inf (insert x S) = (if S = {} then x else min x (Inf S))"
by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If)
lemma open_real:
fixes s :: "real set"
shows "open s ⟷ (∀x ∈ s. ∃e>0. ∀x'. ¦x' - x¦ < e --> x' ∈ s)"
unfolding open_dist dist_norm by simp
lemma islimpt_approachable_real:
fixes s :: "real set"
shows "x islimpt s ⟷ (∀e>0. ∃x'∈ s. x' ≠ x ∧ ¦x' - x¦ < e)"
unfolding islimpt_approachable dist_norm by simp
lemma closed_real:
fixes s :: "real set"
shows "closed s ⟷ (∀x. (∀e>0. ∃x' ∈ s. x' ≠ x ∧ ¦x' - x¦ < e) ⟶ x ∈ s)"
unfolding closed_limpt islimpt_approachable dist_norm by simp
lemma continuous_at_real_range:
fixes f :: "'a::real_normed_vector ⇒ real"
shows "continuous (at x) f ⟷ (∀e>0. ∃d>0. ∀x'. norm(x' - x) < d --> ¦f x' - f x¦ < e)"
by (metis (mono_tags, opaque_lifting) LIM_eq continuous_within norm_eq_zero real_norm_def right_minus_eq)
lemma continuous_on_real_range:
fixes f :: "'a::real_normed_vector ⇒ real"
shows "continuous_on s f ⟷
(∀x ∈ s. ∀e>0. ∃d>0. (∀x' ∈ s. norm(x' - x) < d ⟶ ¦f x' - f x¦ < e))"
unfolding continuous_on_iff dist_norm by simp
lemma continuous_on_closed_Collect_le:
fixes f g :: "'a::topological_space ⇒ real"
assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"
shows "closed {x ∈ s. f x ≤ g x}"
proof -
have "closed ((λx. g x - f x) -` {0..} ∩ s)"
using closed_real_atLeast continuous_on_diff [OF g f]
by (simp add: continuous_on_closed_vimage [OF s])
also have "((λx. g x - f x) -` {0..} ∩ s) = {x∈s. f x ≤ g x}"
by auto
finally show ?thesis .
qed
lemma continuous_le_on_closure:
fixes a::real
assumes f: "continuous_on (closure s) f"
and x: "x ∈ closure(s)"
and xlo: "⋀x. x ∈ s ==> f(x) ≤ a"
shows "f(x) ≤ a"
using image_closure_subset [OF f, where T=" {x. x ≤ a}" ] assms
continuous_on_closed_Collect_le[of "UNIV" "λx. x" "λx. a"]
by auto
lemma continuous_ge_on_closure:
fixes a::real
assumes f: "continuous_on (closure s) f"
and x: "x ∈ closure(s)"
and xlo: "⋀x. x ∈ s ==> f(x) ≥ a"
shows "f(x) ≥ a"
using image_closure_subset [OF f, where T=" {x. a ≤ x}"] assms
continuous_on_closed_Collect_le[of "UNIV" "λx. a" "λx. x"]
by auto
section‹The infimum of the distance between two sets›
definition setdist :: "'a::metric_space set ⇒ 'a set ⇒ real" where
"setdist s t ≡
(if s = {} ∨ t = {} then 0
else Inf {dist x y| x y. x ∈ s ∧ y ∈ t})"
lemma setdist_empty1 [simp]: "setdist {} t = 0"
by (simp add: setdist_def)
lemma setdist_empty2 [simp]: "setdist t {} = 0"
by (simp add: setdist_def)
lemma setdist_pos_le [simp]: "0 ≤ setdist s t"
by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
lemma le_setdistI:
assumes "s ≠ {}" "t ≠ {}" "⋀x y. ⟦x ∈ s; y ∈ t⟧ ⟹ d ≤ dist x y"
shows "d ≤ setdist s t"
using assms
by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)
lemma setdist_le_dist: "⟦x ∈ s; y ∈ t⟧ ⟹ setdist s t ≤ dist x y"
unfolding setdist_def
by (auto intro!: bdd_belowI [where m=0] cInf_lower)
lemma le_setdist_iff:
"d ≤ setdist S T ⟷
(∀x ∈ S. ∀y ∈ T. d ≤ dist x y) ∧ (S = {} ∨ T = {} ⟶ d ≤ 0)"
by (smt (verit) le_setdistI setdist_def setdist_le_dist)
lemma setdist_ltE:
assumes "setdist S T < b" "S ≠ {}" "T ≠ {}"
obtains x y where "x ∈ S" "y ∈ T" "dist x y < b"
using assms
by (auto simp: not_le [symmetric] le_setdist_iff)
lemma setdist_refl: "setdist S S = 0"
by (metis dist_eq_0_iff ex_in_conv order_antisym setdist_def setdist_le_dist setdist_pos_le)
lemma setdist_sym: "setdist S T = setdist T S"
by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
lemma setdist_triangle: "setdist S T ≤ setdist S {a} + setdist {a} T"
proof (cases "S = {} ∨ T = {}")
case True then show ?thesis
using setdist_pos_le by fastforce
next
case False
then have "⋀x. x ∈ S ⟹ setdist S T - dist x a ≤ setdist {a} T"
using dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff
by (smt (verit, best) dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff)
then have "setdist S T - setdist {a} T ≤ setdist S {a}"
using False by (fastforce intro: le_setdistI)
then show ?thesis
by (simp add: algebra_simps)
qed
lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
by (simp add: setdist_def)
lemma setdist_Lipschitz: "¦setdist {x} S - setdist {y} S¦ ≤ dist x y"
apply (subst setdist_singletons [symmetric])
by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (λy. (setdist {y} S))"
by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
lemma continuous_on_setdist [continuous_intros]: "continuous_on T (λy. (setdist {y} S))"
by (metis continuous_at_setdist continuous_at_imp_continuous_on)
lemma uniformly_continuous_on_setdist: "uniformly_continuous_on T (λy. (setdist {y} S))"
by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
lemma setdist_subset_right: "⟦T ≠ {}; T ⊆ u⟧ ⟹ setdist S u ≤ setdist S T"
by (smt (verit, best) in_mono le_setdist_iff)
lemma setdist_subset_left: "⟦S ≠ {}; S ⊆ T⟧ ⟹ setdist T u ≤ setdist S u"
by (metis setdist_subset_right setdist_sym)
lemma setdist_closure_1 [simp]: "setdist (closure S) T = setdist S T"
proof (cases "S = {} ∨ T = {}")
case True then show ?thesis by force
next
case False
{ fix y
assume "y ∈ T"
have "continuous_on (closure S) (λa. dist a y)"
by (auto simp: continuous_intros dist_norm)
then have *: "⋀x. x ∈ closure S ⟹ setdist S T ≤ dist x y"
by (fast intro: setdist_le_dist ‹y ∈ T› continuous_ge_on_closure)
} then
show ?thesis
by (metis False antisym closure_eq_empty closure_subset le_setdist_iff setdist_subset_left)
qed
lemma setdist_closure_2 [simp]: "setdist T (closure S) = setdist T S"
by (metis setdist_closure_1 setdist_sym)
lemma setdist_eq_0I: "⟦x ∈ S; x ∈ T⟧ ⟹ setdist S T = 0"
by (metis antisym dist_self setdist_le_dist setdist_pos_le)
lemma setdist_unique:
"⟦a ∈ S; b ∈ T; ⋀x y. x ∈ S ∧ y ∈ T ==> dist a b ≤ dist x y⟧
⟹ setdist S T = dist a b"
by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)
lemma setdist_le_sing: "x ∈ S ==> setdist S T ≤ setdist {x} T"
using setdist_subset_left by auto
lemma infdist_eq_setdist: "infdist x A = setdist {x} A"
by (simp add: infdist_def setdist_def Setcompr_eq_image)
lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a∈A. infdist a B)"
proof -
have "Inf {dist x y |x y. x ∈ A ∧ y ∈ B} = (INF x∈A. Inf (dist x ` B))"
if "b ∈ B" "a ∈ A" for a b
proof (rule order_antisym)
have "Inf {dist x y |x y. x ∈ A ∧ y ∈ B} ≤ Inf (dist x ` B)"
if "b ∈ B" "a ∈ A" "x ∈ A" for x
proof -
have "⋀b'. b' ∈ B ⟹ Inf {dist x y |x y. x ∈ A ∧ y ∈ B} ≤ dist x b'"
by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3))
then show ?thesis
by (smt (verit) cINF_greatest ex_in_conv ‹b ∈ B›)
qed
then show "Inf {dist x y |x y. x ∈ A ∧ y ∈ B} ≤ (INF x∈A. Inf (dist x ` B))"
by (metis (mono_tags, lifting) cINF_greatest emptyE that)
next
have *: "⋀x y. ⟦b ∈ B; a ∈ A; x ∈ A; y ∈ B⟧ ⟹ ∃a∈A. Inf (dist a ` B) ≤ dist x y"
by (meson bdd_below_image_dist cINF_lower)
show "(INF x∈A. Inf (dist x ` B)) ≤ Inf {dist x y |x y. x ∈ A ∧ y ∈ B}"
proof (rule conditionally_complete_lattice_class.cInf_mono)
show "bdd_below ((λx. Inf (dist x ` B)) ` A)"
by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1))
qed (use that in ‹auto simp: *›)
qed
then show ?thesis
by (auto simp: setdist_def infdist_def)
qed
lemma infdist_mono:
assumes "A ⊆ B" "A ≠ {}"
shows "infdist x B ≤ infdist x A"
by (simp add: assms infdist_eq_setdist setdist_subset_right)
lemma infdist_singleton [simp]: "infdist x {y} = dist x y"
by (simp add: infdist_eq_setdist)
proposition setdist_attains_inf:
assumes "compact B" "B ≠ {}"
obtains y where "y ∈ B" "setdist A B = infdist y A"
proof (cases "A = {}")
case True
then show thesis
by (metis assms diameter_compact_attained infdist_def setdist_def that)
next
case False
obtain y where "y ∈ B" and min: "⋀y'. y' ∈ B ⟹ infdist y A ≤ infdist y' A"
by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id)
show thesis
proof
have "setdist A B = (INF y∈B. infdist y A)"
by (metis ‹B ≠ {}› setdist_eq_infdist setdist_sym)
also have "… = infdist y A"
proof (rule order_antisym)
show "(INF y∈B. infdist y A) ≤ infdist y A"
by (meson ‹y ∈ B› bdd_belowI2 cInf_lower image_eqI infdist_nonneg)
next
show "infdist y A ≤ (INF y∈B. infdist y A)"
by (simp add: ‹B ≠ {}› cINF_greatest min)
qed
finally show "setdist A B = infdist y A" .
qed (fact ‹y ∈ B›)
qed
section ‹Diameter Lemma›
text ‹taken from the AFP entry Martingales, by Ata Keskin, TU München›
lemma diameter_comp_strict_mono:
fixes s :: "nat ⇒ 'a :: metric_space"
assumes "strict_mono r" "bounded {s i |i. r n ≤ i}"
shows "diameter {s (r i) | i. n ≤ i} ≤ diameter {s i | i. r n ≤ i}"
proof (rule diameter_subset)
show "{s (r i) | i. n ≤ i} ⊆ {s i | i. r n ≤ i}" using assms(1) monotoneD strict_mono_mono by fastforce
qed (intro assms(2))
lemma diameter_bounded_bound':
fixes S :: "'a :: metric_space set"
assumes S: "bdd_above (case_prod dist ` (S×S))" and "x ∈ S" "y ∈ S"
shows "dist x y ≤ diameter S"
proof -
have "(x,y) ∈ S×S" using assms by auto
then have "dist x y ≤ (SUP (x,y)∈S×S. dist x y)"
by (metis S cSUP_upper case_prod_conv)
with ‹x ∈ S› show ?thesis by (auto simp: diameter_def)
qed
lemma bounded_imp_dist_bounded:
assumes "bounded (range s)"
shows "bounded ((λ(i, j). dist (s i) (s j)) ` ({n..} × {n..}))"
using bounded_dist_comp[OF bounded_fst bounded_snd, OF bounded_Times(1,1)[OF assms(1,1)]] by (rule bounded_subset, force)
text ‹A sequence is Cauchy, if and only if it is bounded and its diameter tends to zero. The diameter is well-defined only if the sequence is bounded.›
lemma cauchy_iff_diameter_tends_to_zero_and_bounded:
fixes s :: "nat ⇒ 'a :: metric_space"
shows "Cauchy s ⟷ ((λn. diameter {s i | i. i ≥ n}) ⇢ 0 ∧ bounded (range s))"
proof -
have "{s i |i. N ≤ i} ≠ {}" for N by blast
hence diameter_SUP: "diameter {s i |i. N ≤ i} = (SUP (i, j) ∈ {N..} × {N..}. dist (s i) (s j))" for N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup])
show ?thesis
proof (intro iffI)
assume asm: "Cauchy s"
have "∃N. ∀n≥N. norm (diameter {s i |i. n ≤ i}) < e" if e_pos: "e > 0" for e
proof -
obtain N where dist_less: "dist (s n) (s m) < (1/2) * e" if "n ≥ N" "m ≥ N" for n m using asm e_pos by (metis Cauchy_def mult_pos_pos zero_less_divide_iff zero_less_numeral zero_less_one)
{
fix r assume "r ≥ N"
hence "dist (s n) (s m) < (1/2) * e" if "n ≥ r" "m ≥ r" for n m using dist_less that by simp
hence "(SUP (i, j) ∈ {r..} × {r..}. dist (s i) (s j)) ≤ (1/2) * e" by (intro cSup_least) fastforce+
also have "... < e" using e_pos by simp
finally have "diameter {s i |i. r ≤ i} < e" using diameter_SUP by presburger
}
moreover have "diameter {s i |i. r ≤ i} ≥ 0" for r unfolding diameter_SUP using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above, OF asm] by (intro cSup_upper2, auto)
ultimately show ?thesis by auto
qed
thus "(λn. diameter {s i |i. n ≤ i}) ⇢ 0 ∧ bounded (range s)" using cauchy_imp_bounded[OF asm] by (simp add: LIMSEQ_iff)
next
assume asm: "(λn. diameter {s i |i. n ≤ i}) ⇢ 0 ∧ bounded (range s)"
have "∃N. ∀n≥N. ∀m≥N. dist (s n) (s m) < e" if e_pos: "e > 0" for e
proof -
obtain N where diam_less: "diameter {s i |i. r ≤ i} < e" if "r ≥ N" for r using LIMSEQ_D asm(1) e_pos by fastforce
{
fix n m assume "n ≥ N" "m ≥ N"
hence "dist (s n) (s m) < e" using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above], OF _ diam_less[unfolded diameter_SUP]] asm by auto
}
thus ?thesis by blast
qed
then show "Cauchy s" by (simp add: Cauchy_def)
qed
qed
end