Theory Elementary_Metric_Spaces
section ‹Elementary Metric Spaces›
theory Elementary_Metric_Spaces
imports
Abstract_Topology_2
Metric_Arith
begin
subsection ‹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
subsection ‹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)
subsection ‹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)
subsection ‹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
subsection ‹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)
subsection ‹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)
subsection ‹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)
subsection ‹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)
subsection ‹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
subsection ‹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
subsection ‹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
subsection ‹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
subsection ‹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
subsection ‹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