(* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University Author: Ata Keskin, TU Muenchen *) chapter ‹Elementary Metric Spaces› theory Elementary_Metric_Spaces imports Abstract_Topology_2 Metric_Arith begin section ‹Open and closed balls› definition✐‹tag important› ball :: "'a::metric_space ⇒ real ⇒ 'a set" where "ball x e = {y. dist x y < e}" definition✐‹tag important› cball :: "'a::metric_space ⇒ real ⇒ 'a set" where "cball x e = {y. dist x y ≤ e}" definition✐‹tag important› 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› (* FIXME: This has to be unified with BSEQ!! *) definition✐‹tag important› (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: ― ‹this is the definition of compactness in HOL Light› "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:― ‹TODO: rename to ‹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✐‹tag important› 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