Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Topology_Euclidean_Space.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Author:     L C Paulson, University of Cambridge
    Author:     Amine Chaieb, University of Cambridge
    Author:     Robert Himmelmann, TU Muenchen
    Author:     Brian Huffman, Portland State University
*)

section \<open>Elementary Metric Spaces\<close>

theory Elementary_Metric_Spaces
  imports
    Abstract_Topology_2
    Metric_Arith
begin

subsection \<open>Open and closed balls\<close>

definition\<^marker>\<open>tag important\<close> ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
  where "ball x e = {y. dist x y < e}"

definition\<^marker>\<open>tag important\<close> cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
  where "cball x e = {y. dist x y \ e}"

definition\<^marker>\<open>tag important\<close> sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
  where "sphere x e = {y. dist x y = e}"

lemma mem_ball [simp, metric_unfold]: "y \ ball x e \ dist x y < e"
  by (simp add: ball_def)

lemma mem_cball [simp, metric_unfold]: "y \ cball x e \ dist x y \ e"
  by (simp add: cball_def)

lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e"
  by (simp add: sphere_def)

lemma ball_trivial [simp]: "ball x 0 = {}"
  by (simp add: ball_def)

lemma cball_trivial [simp]: "cball x 0 = {x}"
  by (simp add: cball_def)

lemma sphere_trivial [simp]: "sphere x 0 = {x}"
  by (simp add: sphere_def)

lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}"
  using dist_triangle_less_add not_le by fastforce

lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}"
  by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)

lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}"
  for a :: "'a::metric_space"
  by auto

lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e"
  by simp

lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e"
  by simp

lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e"
  by (simp add: subset_eq)

lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e"
  by auto

lemma sphere_cball [simp,intro]: "sphere z r \ cball z r"
  by force

lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"
  by auto

lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e"
  by auto

lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e"
  by auto

lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f"
  by auto

lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f"
  by auto

lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)"
  by metric

lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s"
  by auto

lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s"
  by auto

lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s"
  by auto

lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s"
  by auto

lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r"
  by auto

lemma open_ball [intro, simp]: "open (ball x e)"
proof -
  have "open (dist x -` {..
    by (intro open_vimage open_lessThan continuous_intros)
  also have "dist x -` {..
    by auto
  finally show ?thesis .
qed

lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)"
  by (simp add: open_dist subset_eq Ball_def dist_commute)

lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S"
  by (auto simp: open_contains_ball)

lemma openE[elim?]:
  assumes "open S" "x\S"
  obtains e where "e>0" "ball x e \ S"
  using assms unfolding open_contains_ball by auto

lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)"
  by (metis open_contains_ball subset_eq centre_in_ball)

lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0"
  unfolding mem_ball set_eq_iff
  by (simp add: not_less) metric

lemma ball_empty: "e \ 0 \ ball x e = {}"
  by simp

lemma closed_cball [iff]: "closed (cball x e)"
proof -
  have "closed (dist x -` {..e})"
    by (intro closed_vimage closed_atMost continuous_intros)
  also have "dist x -` {..e} = cball x e"
    by auto
  finally show ?thesis .
qed

lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)"
proof -
  {
    fix x and e::real
    assume "x\S" "e>0" "ball x e \ S"
    then have "\d>0. cball x d \ S"
      unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
  }
  moreover
  {
    fix x and e::real
    assume "x\S" "e>0" "cball x e \ S"
    then have "\d>0. ball x d \ S"
      using mem_ball_imp_mem_cball by blast
  }
  ultimately show ?thesis
    unfolding open_contains_ball by auto
qed

lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))"
  by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)

lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)"
  by (rule eventually_nhds_in_open) simp_all

lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)"
  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)

lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)"
  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)

lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y"
  by (subst at_within_open) auto

lemma atLeastAtMost_eq_cball:
  fixes a b::real
  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
  by (auto simp: dist_real_def field_simps)

lemma cball_eq_atLeastAtMost:
  fixes a b::real
  shows "cball a b = {a - b .. a + b}"
  by (auto simp: dist_real_def)

lemma greaterThanLessThan_eq_ball:
  fixes a b::real
  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
  by (auto simp: dist_real_def field_simps)

lemma ball_eq_greaterThanLessThan:
  fixes a b::real
  shows "ball a b = {a - b <..< a + b}"
  by (auto simp: dist_real_def)

lemma interior_ball [simp]: "interior (ball x e) = ball x e"
  by (simp add: interior_open)

lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0"
  apply (simp add: set_eq_iff not_le)
  apply (metis zero_le_dist dist_self order_less_le_trans)
  done

lemma cball_empty [simp]: "e < 0 \ cball x e = {}"
  by simp

lemma cball_sing:
  fixes x :: "'a::metric_space"
  shows "e = 0 \ cball x e = {x}"
  by simp

lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e"
  by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one)

lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e"
  using ball_divide_subset one_le_numeral by blast

lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e"
  apply (cases "e < 0", simp add: field_split_simps)
  by (metis div_by_1 frac_le less_numeral_extra(1) not_le order_refl subset_cball)

lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e"
  using cball_divide_subset one_le_numeral by blast

lemma cball_scale:
  assumes "a \ 0"
  shows   "(\x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
  have 1: "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a
  proof safe
    fix x
    assume x: "x \ cball c r"
    have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
      by (auto simp: dist_norm)
    also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
      by (simp add: algebra_simps)
    finally show "a *\<^sub>R x \ cball (a *\<^sub>R c) (\a\ * r)"
      using that x by (auto simp: dist_norm)
  qed

  have "cball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\a\ * r)"
    unfolding image_image using assms by simp
  also have "\ \ (\x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
    using assms by (intro image_mono 1) auto
  also have "\ = (\x. a *\<^sub>R x) ` cball c r"
    using assms by (simp add: algebra_simps)
  finally have "cball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` cball c r" .
  moreover from assms have "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)"
    by (intro 1) auto
  ultimately show ?thesis by blast
qed

lemma ball_scale:
  assumes "a \ 0"
  shows   "(\x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)"
proof -
  have 1: "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a
  proof safe
    fix x
    assume x: "x \ ball c r"
    have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)"
      by (auto simp: dist_norm)
    also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)"
      by (simp add: algebra_simps)
    finally show "a *\<^sub>R x \ ball (a *\<^sub>R c) (\a\ * r)"
      using that x by (auto simp: dist_norm)
  qed

  have "ball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\a\ * r)"
    unfolding image_image using assms by simp
  also have "\ \ (\x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))"
    using assms by (intro image_mono 1) auto
  also have "\ = (\x. a *\<^sub>R x) ` ball c r"
    using assms by (simp add: algebra_simps)
  finally have "ball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` ball c r" .
  moreover from assms have "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)"
    by (intro 1) auto
  ultimately show ?thesis by blast
qed

subsection \<open>Limit Points\<close>

lemma islimpt_approachable:
  fixes x :: "'a::metric_space"
  shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)"
  unfolding islimpt_iff_eventually eventually_at by fast

lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)"
  for x :: "'a::metric_space"
  unfolding islimpt_approachable
  using approachable_lt_le2 [where f="\y. dist y x" and P="\y. y \ S \ y = x" and Q="\x. True"]
  by auto

lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S"
  for x :: "'a::metric_space"
  apply (clarsimp simp add: islimpt_approachable)
  apply (drule_tac x="e/2" in spec)
  apply (auto simp: simp del: less_divide_eq_numeral1)
  apply (drule_tac x="dist x' x" in spec)
  apply (auto simp del: less_divide_eq_numeral1)
  apply metric
  done

lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"
  using closed_limpt limpt_of_limpts by blast

lemma limpt_of_closure: "x islimpt closure S \ x islimpt S"
  for x :: "'a::metric_space"
  by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)

lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))"
  apply (simp add: islimpt_eq_acc_point, safe)
   apply (metis Int_commute open_ball centre_in_ball)
  by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)

lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))"
  apply (simp add: islimpt_eq_infinite_ball, safe)
   apply (meson Int_mono ball_subset_cball finite_subset order_refl)
  by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)

subsection \<open>Perfect Metric Spaces\<close>

lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r"
  for x :: "'a::{perfect_space,metric_space}"
  using islimpt_UNIV [of x] by (simp add: islimpt_approachable)

lemma cball_eq_sing:
  fixes x :: "'a::{metric_space,perfect_space}"
  shows "cball x e = {x} \ e = 0"
proof (rule linorder_cases)
  assume e: "0 < e"
  obtain a where "a \ x" "dist a x < e"
    using perfect_choose_dist [OF e] by auto
  then have "a \ x" "dist x a \ e"
    by (auto simp: dist_commute)
  with e show ?thesis by (auto simp: set_eq_iff)
qed auto

subsection \<open>?\<close>

lemma finite_ball_include:
  fixes a :: "'a::metric_space"
  assumes "finite S"
  shows "\e>0. S \ ball a e"
  using assms
proof induction
  case (insert x S)
  then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto
  define e where "e = max e0 (2 * dist a x)"
  have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
  moreover have "insert x S \ ball a e"
    using e0 \<open>e>0\<close> unfolding e_def by auto
  ultimately show ?case by auto
qed (auto intro: zero_less_one)

lemma finite_set_avoid:
  fixes a :: "'a::metric_space"
  assumes "finite S"
  shows "\d>0. \x\S. x \ a \ d \ dist a x"
  using assms
proof induction
  case (insert x S)
  then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x"
    by blast
  show ?case
  proof (cases "x = a")
    case True
    with \<open>d > 0 \<close>d show ?thesis by auto
  next
    case False
    let ?d = "min d (dist a x)"
    from False \<open>d > 0\<close> have dp: "?d > 0"
      by auto
    from d have d': "\x\S. x \ a \ ?d \ dist a x"
      by auto
    with dp False show ?thesis
      by (metis insert_iff le_less min_less_iff_conj not_less)
  qed
qed (auto intro: zero_less_one)

lemma discrete_imp_closed:
  fixes S :: "'a::metric_space set"
  assumes e: "0 < e"
    and d: "\x \ S. \y \ S. dist y x < e \ y = x"
  shows "closed S"
proof -
  have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x
  proof -
    from e have e2: "e/2 > 0" by arith
    from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2"
      by blast
    from e2 y(2) have mp: "min (e/2) (dist x y) > 0"
      by simp
    from d y C[OF mp] show ?thesis
      by metric
  qed
  then show ?thesis
    by (metis islimpt_approachable closed_limpt [where 'a='a])
qed

subsection \<open>Interior\<close>

lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)"
  using open_contains_ball_eq [where S="interior S"]
  by (simp add: open_subset_interior)

lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)"
  by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
      subset_trans)

subsection \<open>Frontier\<close>

lemma frontier_straddle:
  fixes a :: "'a::metric_space"
  shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))"
  unfolding frontier_def closure_interior
  by (auto simp: mem_interior subset_eq ball_def)

subsection \<open>Limits\<close>

proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)"
  by (auto simp: tendsto_iff trivial_limit_eq)

text \<open>Show that they yield usual definitions in the various cases.\<close>

proposition Lim_within_le: "(f \ l)(at a within S) \
    (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
  by (auto simp: tendsto_iff eventually_at_le)

proposition Lim_within: "(f \ l) (at a within S) \
    (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
  by (auto simp: tendsto_iff eventually_at)

corollary Lim_withinI [intro?]:
  assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e"
  shows "(f \ l) (at a within S)"
  apply (simp add: Lim_within, clarify)
  apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
  done

proposition Lim_at: "(f \ l) (at a) \
    (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
  by (auto simp: tendsto_iff eventually_at)

lemma Lim_transform_within_set:
  fixes a :: "'a::metric_space" and l :: "'b::metric_space"
  shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\
         \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
apply (clarsimp simp: eventually_at Lim_within)
apply (drule_tac x=e in spec, clarify)
apply (rename_tac k)
apply (rule_tac x="min d k" in exI, simp)
done

text \<open>Another limit point characterization.\<close>

lemma limpt_sequential_inj:
  fixes x :: "'a::metric_space"
  shows "x islimpt S \
         (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"
         (is "?lhs = ?rhs")
proof
  assume ?lhs
  then have "\e>0. \x'\S. x' \ x \ dist x' x < e"
    by (force simp: islimpt_approachable)
  then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e"
    by metis
  define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
  have [simp]: "f 0 = y 1"
               "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
    by (simp_all add: f_def)
  have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n
  proof (induction n)
    case 0 show ?case
      by (simp add: y)
  next
    case (Suc n) then show ?case
      apply (auto simp: y)
      by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)
  qed
  show ?rhs
  proof (rule_tac x=f in exI, intro conjI allI)
    show "\n. f n \ S - {x}"
      using f by blast
    have "dist (f n) x < dist (f m) x" if "m < n" for m n
    using that
    proof (induction n)
      case 0 then show ?case by simp
    next
      case (Suc n)
      then consider "m < n" | "m = n" using less_Suc_eq by blast
      then show ?case
      proof cases
        assume "m < n"
        have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
          by simp
        also have "\ < dist (f n) x"
          by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
        also have "\ < dist (f m) x"
          using Suc.IH \<open>m < n\<close> by blast
        finally show ?thesis .
      next
        assume "m = n" then show ?case
          by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)
      qed
    qed
    then show "inj f"
      by (metis less_irrefl linorder_injI)
    show "f \ x"
      apply (rule tendstoI)
      apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)
      apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
      apply (simp add: field_simps)
      by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)
  qed
next
  assume ?rhs
  then show ?lhs
    by (fastforce simp add: islimpt_approachable lim_sequentially)
qed

lemma Lim_dist_ubound:
  assumes "\(trivial_limit net)"
    and "(f \ l) net"
    and "eventually (\x. dist a (f x) \ e) net"
  shows "dist a l \ e"
  using assms by (fast intro: tendsto_le tendsto_intros)

subsection \<open>Continuity\<close>

text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>

proposition continuous_within_eps_delta:
  "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)"
  unfolding continuous_within and Lim_within  by fastforce

corollary continuous_at_eps_delta:
  "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)"
  using continuous_within_eps_delta [of x UNIV f] by simp

lemma continuous_at_right_real_increasing:
  fixes f :: "real \ real"
  assumes nondecF: "\x y. x \ y \ f x \ f y"
  shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)"
  apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
  apply (intro all_cong ex_cong, safe)
  apply (erule_tac x="a + d" in allE, simp)
  apply (simp add: nondecF field_simps)
  apply (drule nondecF, simp)
  done

lemma continuous_at_left_real_increasing:
  assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)"
  shows "(continuous (at_left (a :: real)) f) = (\e > 0. \delta > 0. f a - f (a - delta) < e)"
  apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
  apply (intro all_cong ex_cong, safe)
  apply (erule_tac x="a - d" in allE, simp)
  apply (simp add: nondecF field_simps)
  apply (cut_tac x="a - d" and y=x in nondecF, simp_all)
  done

text\<open>Versions in terms of open balls.\<close>

lemma continuous_within_ball:
  "continuous (at x within s) f \
    (\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  {
    fix e :: real
    assume "e > 0"
    then obtain d where d: "d>0" "\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < e"
      using \<open>?lhs\<close>[unfolded continuous_within Lim_within] by auto
    {
      fix y
      assume "y \ f ` (ball x d \ s)"
      then have "y \ ball (f x) e"
        using d(2)
        using \<open>e > 0\<close>
        by (auto simp: dist_commute)
    }
    then have "\d>0. f ` (ball x d \ s) \ ball (f x) e"
      using \<open>d > 0\<close>
      unfolding subset_eq ball_def by (auto simp: dist_commute)
  }
  then show ?rhs by auto
next
  assume ?rhs
  then show ?lhs
    unfolding continuous_within Lim_within ball_def subset_eq
    apply (auto simp: dist_commute)
    apply (erule_tac x=e in allE, auto)
    done
qed

lemma continuous_at_ball:
  "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
    by (metis dist_commute dist_pos_lt dist_self)
next
  assume ?rhs
  then show ?lhs
    unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
    by (metis dist_commute)
qed

text\<open>Define setwise continuity in terms of limits within the set.\<close>

lemma continuous_on_iff:
  "continuous_on s f \
    (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
  unfolding continuous_on_def Lim_within
  by (metis dist_pos_lt dist_self)

lemma continuous_within_E:
  assumes "continuous (at x within s) f" "e>0"
  obtains d where "d>0"  "\x'. \x'\ s; dist x' x \ d\ \ dist (f x') (f x) < e"
  using assms apply (simp add: continuous_within_eps_delta)
  apply (drule spec [of _ e], clarify)
  apply (rule_tac d="d/2" in that, auto)
  done

lemma continuous_onI [intro?]:
  assumes "\x e. \e > 0; x \ s\ \ \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) \ e"
  shows "continuous_on s f"
apply (simp add: continuous_on_iff, clarify)
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
done

text\<open>Some simple consequential lemmas.\<close>

lemma continuous_onE:
    assumes "continuous_on s f" "x\s" "e>0"
    obtains d where "d>0"  "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e"
  using assms
  apply (simp add: continuous_on_iff)
  apply (elim ballE allE)
  apply (auto intro: that [where d="d/2" for d])
  done

text\<open>The usual transformation theorems.\<close>

lemma continuous_transform_within:
  fixes f g :: "'a::metric_space \ 'b::topological_space"
  assumes "continuous (at x within s) f"
    and "0 < d"
    and "x \ s"
    and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'"
  shows "continuous (at x within s) g"
  using assms
  unfolding continuous_within
  by (force intro: Lim_transform_within)

subsection \<open>Closure and Limit Characterization\<close>

lemma closure_approachable:
  fixes S :: "'a::metric_space set"
  shows "x \ closure S \ (\e>0. \y\S. dist y x < e)"
  apply (auto simp: closure_def islimpt_approachable)
  apply (metis dist_self)
  done

lemma closure_approachable_le:
  fixes S :: "'a::metric_space set"
  shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)"
  unfolding closure_approachable
  using dense by force

lemma closure_approachableD:
  assumes "x \ closure S" "e>0"
  shows "\y\S. dist x y < e"
  using assms unfolding closure_approachable by (auto simp: dist_commute)

lemma closed_approachable:
  fixes S :: "'a::metric_space set"
  shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S"
  by (metis closure_closed closure_approachable)

lemma closure_contains_Inf:
  fixes S :: "real set"
  assumes "S \ {}" "bdd_below S"
  shows "Inf S \ closure S"
proof -
  have *: "\x\S. Inf S \ x"
    using cInf_lower[of _ S] assms by metis
  {
    fix e :: real
    assume "e > 0"
    then have "Inf S < Inf S + e" by simp
    with assms obtain x where "x \ S" "x < Inf S + e"
      by (subst (asm) cInf_less_iff) auto
    with * have "\x\S. dist x (Inf S) < e"
      by (intro bexI[of _ x]) (auto simp: dist_real_def)
  }
  then show ?thesis unfolding closure_approachable by auto
qed

lemma closure_contains_Sup:
  fixes S :: "real set"
  assumes "S \ {}" "bdd_above S"
  shows "Sup S \ closure S"
proof -
  have *: "\x\S. x \ Sup S"
    using cSup_upper[of _ S] assms by metis
  {
    fix e :: real
    assume "e > 0"
    then have "Sup S - e < Sup S" by simp
    with assms obtain x where "x \ S" "Sup S - e < x"
      by (subst (asm) less_cSup_iff) auto
    with * have "\x\S. dist x (Sup S) < e"
      by (intro bexI[of _ x]) (auto simp: dist_real_def)
  }
  then show ?thesis unfolding closure_approachable by auto
qed

lemma not_trivial_limit_within_ball:
  "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})"
  (is "?lhs \ ?rhs")
proof
  show ?rhs if ?lhs
  proof -
    {
      fix e :: real
      assume "e > 0"
      then obtain y where "y \ S - {x}" and "dist y x < e"
        using \<open>?lhs\<close> not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
        by auto
      then have "y \ S \ ball x e - {x}"
        unfolding ball_def by (simp add: dist_commute)
      then have "S \ ball x e - {x} \ {}" by blast
    }
    then show ?thesis by auto
  qed
  show ?lhs if ?rhs
  proof -
    {
      fix e :: real
      assume "e > 0"
      then obtain y where "y \ S \ ball x e - {x}"
        using \<open>?rhs\<close> by blast
      then have "y \ S - {x}" and "dist y x < e"
        unfolding ball_def by (simp_all add: dist_commute)
      then have "\y \ S - {x}. dist y x < e"
        by auto
    }
    then show ?thesis
      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
      by auto
  qed
qed

subsection \<open>Boundedness\<close>

  (* FIXME: This has to be unified with BSEQ!! *)
definition\<^marker>\<open>tag important\<close> (in metric_space) bounded :: "'a set \<Rightarrow> bool"
  where "bounded S \ (\x e. \y\S. dist x y \ e)"

lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)"
  unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)

lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)"
  unfolding bounded_def
  by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)

lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)"
  unfolding bounded_any_center [where a=0]
  by (simp add: dist_norm)

lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X"
  by (simp add: bounded_iff bdd_above_def)

lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)"
  by (simp add: bounded_iff)

lemma boundedI:
  assumes "\x. x \ S \ norm x \ B"
  shows "bounded S"
  using assms bounded_iff by blast

lemma bounded_empty [simp]: "bounded {}"
  by (simp add: bounded_def)

lemma bounded_subset: "bounded T \ S \ T \ bounded S"
  by (metis bounded_def subset_eq)

lemma bounded_interior[intro]: "bounded S \ bounded(interior S)"
  by (metis bounded_subset interior_subset)

lemma bounded_closure[intro]:
  assumes "bounded S"
  shows "bounded (closure S)"
proof -
  from assms obtain x and a where a: "\y\S. dist x y \ a"
    unfolding bounded_def by auto
  {
    fix y
    assume "y \ closure S"
    then obtain f where f: "\n. f n \ S" "(f \ y) sequentially"
      unfolding closure_sequential by auto
    have "\n. f n \ S \ dist x (f n) \ a" using a by simp
    then have "eventually (\n. dist x (f n) \ a) sequentially"
      by (simp add: f(1))
    then have "dist x y \ a"
      using Lim_dist_ubound f(2) trivial_limit_sequentially by blast
  }
  then show ?thesis
    unfolding bounded_def by auto
qed

lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)"
  by (simp add: bounded_subset closure_subset image_mono)

lemma bounded_cball[simp,intro]: "bounded (cball x e)"
  unfolding bounded_def  using mem_cball by blast

lemma bounded_ball[simp,intro]: "bounded (ball x e)"
  by (metis ball_subset_cball bounded_cball bounded_subset)

lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T"
  by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)

lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)"
  by (induct rule: finite_induct[of F]) auto

lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)"
  by auto

lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S"
proof -
  have "\y\{x}. dist x y \ 0"
    by simp
  then have "bounded {x}"
    unfolding bounded_def by fast
  then show ?thesis
    by (metis insert_is_Un bounded_Un)
qed

lemma bounded_subset_ballI: "S \ ball x r \ bounded S"
  by (meson bounded_ball bounded_subset)

lemma bounded_subset_ballD:
  assumes "bounded S" shows "\r. 0 < r \ S \ ball x r"
proof -
  obtain e::real and y where "S \ cball y e" "0 \ e"
    using assms by (auto simp: bounded_subset_cball)
  then show ?thesis
    by (intro exI[where x="dist x y + e + 1"]) metric
qed

lemma finite_imp_bounded [intro]: "finite S \ bounded S"
  by (induct set: finite) simp_all

lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)"
  by (metis Int_lower1 Int_lower2 bounded_subset)

lemma bounded_diff[intro]: "bounded S \ bounded (S - T)"
  by (metis Diff_subset bounded_subset)

lemma bounded_dist_comp:
  assumes "bounded (f ` S)" "bounded (g ` S)"
  shows "bounded ((\x. dist (f x) (g x)) ` S)"
proof -
  from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x
    by (auto simp: bounded_any_center[of _ undefined] dist_commute)
  have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x
    using *[OF that]
    by metric
  then show ?thesis
    by (auto intro!: boundedI)
qed

lemma bounded_Times:
  assumes "bounded s" "bounded t"
  shows "bounded (s \ t)"
proof -
  obtain x y a b where "\z\s. dist x z \ a" "\z\t. dist y z \ b"
    using assms [unfolded bounded_def] by auto
  then have "\z\s \ t. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)"
    by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
  then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
qed

subsection \<open>Compactness\<close>

lemma compact_imp_bounded:
  assumes "compact U"
  shows "bounded U"
proof -
  have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)"
    using assms by auto
  then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)"
    by (metis compactE_image)
  from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"
    by (simp add: bounded_UN)
  then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>
    by (rule bounded_subset)
qed

lemma closure_Int_ball_not_empty:
  assumes "S \ closure T" "x \ S" "r > 0"
  shows "T \ ball x r \ {}"
  using assms centre_in_ball closure_iff_nhds_not_empty by blast

lemma compact_sup_maxdistance:
  fixes S :: "'a::metric_space set"
  assumes "compact S"
    and "S \ {}"
  shows "\x\S. \y\S. \u\S. \v\S. dist u v \ dist x y"
proof -
  have "compact (S \ S)"
    using \<open>compact S\<close> by (intro compact_Times)
  moreover have "S \ S \ {}"
    using \<open>S \<noteq> {}\<close> by auto
  moreover have "continuous_on (S \ S) (\x. dist (fst x) (snd x))"
    by (intro continuous_at_imp_continuous_on ballI continuous_intros)
  ultimately show ?thesis
    using continuous_attains_sup[of "S \ S" "\x. dist (fst x) (snd x)"] by auto
qed

subsubsection\<open>Totally bounded\<close>

lemma cauchy_def: "Cauchy S \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (S m) (S n) < e)"
  unfolding Cauchy_def by metis

proposition seq_compact_imp_totally_bounded:
  assumes "seq_compact S"
  shows "\e>0. \k. finite k \ k \ S \ S \ (\x\k. ball x e)"
proof -
  { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x e)"
    let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < e))"
    have "\x. \n::nat. ?Q x n (x n)"
    proof (rule dependent_wellorder_choice)
      fix n x assume "\y. y < n \ ?Q x y (x y)"
      then have "\ S \ (\x\x ` {0..
        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
      then obtain z where z:"z\S" "z \ (\x\x ` {0..
        unfolding subset_eq by auto
      show "\r. ?Q x n r"
        using z by auto
    qed simp
    then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)"
      by blast
    then obtain l r where "l \ S" and r:"strict_mono r" and "((x \ r) \ l) sequentially"
      using assms by (metis seq_compact_def)
    then have "Cauchy (x \ r)"
      using LIMSEQ_imp_Cauchy by auto
    then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e"
      unfolding cauchy_def using \<open>e > 0\<close> by blast
    then have False
      using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
  then show ?thesis
    by metis
qed

subsubsection\<open>Heine-Borel theorem\<close>

proposition seq_compact_imp_Heine_Borel:
  fixes S :: "'a :: metric_space set"
  assumes "seq_compact S"
  shows "compact S"
proof -
  from seq_compact_imp_totally_bounded[OF \<open>seq_compact S\<close>]
  obtain f where f: "\e>0. finite (f e) \ f e \ S \ S \ (\x\f e. ball x e)"
    unfolding choice_iff' ..
  define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)"
  have "countably_compact S"
    using \<open>seq_compact S\<close> by (rule seq_compact_imp_countably_compact)
  then show "compact S"
  proof (rule countably_compact_imp_compact)
    show "countable K"
      unfolding K_def using f
      by (auto intro: countable_finite countable_subset countable_rat
               intro!: countable_image countable_SIGMA countable_UN)
    show "\b\K. open b" by (auto simp: K_def)
  next
    fix T x
    assume T: "open T" "x \ T" and x: "x \ S"
    from openE[OF T] obtain e where "0 < e" "ball x e \ T"
      by auto
    then have "0 < e/2" "ball x (e/2) \ T"
      by auto
    from Rats_dense_in_real[OF \<open>0 < e/2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e/2"
      by auto
    from f[rule_format, of r] \<open>0 < r\<close> \<open>x \<in> S\<close> obtain k where "k \<in> f r" "x \<in> ball k r"
      by auto
    from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
      by (auto simp: K_def)
    then show "\b\K. x \ b \ b \ S \ T"
    proof (rule bexI[rotated], safe)
      fix y
      assume "y \ ball k r"
      with \<open>r < e/2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"
        by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
      with \<open>ball x e \<subseteq> T\<close> show "y \<in> T"
        by auto
    next
      show "x \ ball k r" by fact
    qed
  qed
qed

proposition compact_eq_seq_compact_metric:
  "compact (S :: 'a::metric_space set) \ seq_compact S"
  using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast

proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
  "compact (S :: 'a::metric_space set) \
   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
  unfolding compact_eq_seq_compact_metric seq_compact_def by auto

subsubsection \<open>Complete the chain of compactness variants\<close>

proposition compact_eq_Bolzano_Weierstrass:
  fixes S :: "'a::metric_space set"
  shows "compact S \ (\T. infinite T \ T \ S \ (\x \ S. x islimpt T))"
  using Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass compact_eq_seq_compact_metric
  by blast

proposition Bolzano_Weierstrass_imp_bounded:
  "(\T. \infinite T; T \ S\ \ (\x \ S. x islimpt T)) \ bounded S"
  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis

subsection \<open>Banach fixed point theorem\<close>

theorem banach_fix:\<comment> \<open>TODO: rename to \<open>Banach_fix\<close>\<close>
  assumes s: "complete s" "s \ {}"
    and c: "0 \ c" "c < 1"
    and f: "f ` s \ s"
    and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y"
  shows "\!x\s. f x = x"
proof -
  from c have "1 - c > 0" by simp

  from s(2) obtain z0 where z0: "z0 \ s" by blast
  define z where "z n = (f ^^ n) z0" for n
  with f z0 have z_in_s: "z n \ s" for n :: nat
    by (induct n) auto
  define d where "d = dist (z 0) (z 1)"

  have fzn: "f (z n) = z (Suc n)" for n
    by (simp add: z_def)
  have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat
  proof (induct n)
    case 0
    then show ?case
      by (simp add: d_def)
  next
    case (Suc m)
    with \<open>0 \<le> c\<close> have "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
      using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp
    then show ?case
      using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
      by (simp add: fzn mult_le_cancel_left)
  qed

  have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat
  proof (induct n)
    case 0
    show ?case by simp
  next
    case (Suc k)
    from c have "(1 - c) * dist (z m) (z (m + Suc k)) \
        (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"
      by (simp add: dist_triangle)
    also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"
      by simp
    also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"
      by (simp add: field_simps)
    also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"
      by (simp add: power_add field_simps)
    also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)"
      by (simp add: field_simps)
    finally show ?case by simp
  qed

  have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e
  proof (cases "d = 0")
    case True
    from \<open>1 - c > 0\<close> have "(1 - c) * x \<le> 0 \<longleftrightarrow> x \<le> 0" for x
      by (simp add: mult_le_0_iff)
    with c cf_z2[of 0] True have "z n = z0" for n
      by (simp add: z_def)
    with \<open>e > 0\<close> show ?thesis by simp
  next
    case False
    with zero_le_dist[of "z 0" "z 1"] have "d > 0"
      by (metis d_def less_le)
    with \<open>1 - c > 0\<close> \<open>e > 0\<close> have "0 < e * (1 - c) / d"
      by simp
    with c obtain N where N: "c ^ N < e * (1 - c) / d"
      using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto
    have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat
    proof -
      from c \<open>n \<ge> N\<close> have *: "c ^ n \<le> c ^ N"
        using power_decreasing[OF \<open>n\<ge>N\<close>, of c] by simp
      from c \<open>m > n\<close> have "1 - c ^ (m - n) > 0"
        using power_strict_mono[of c 1 "m - n"] by simp
      with \<open>d > 0\<close> \<open>0 < 1 - c\<close> have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
        by simp
      from cf_z2[of n "m - n"] \<open>m > n\<close>
      have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
        by (simp add: pos_le_divide_eq[OF \<open>1 - c > 0\<close>] mult.commute dist_commute)
      also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
        using mult_right_mono[OF * order_less_imp_le[OF **]]
        by (simp add: mult.assoc)
      also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
        using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)
      also from c \<open>d > 0\<close> \<open>1 - c > 0\<close> have "\<dots> = e * (1 - c ^ (m - n))"
        by simp
      also from c \<open>1 - c ^ (m - n) > 0\<close> \<open>e > 0\<close> have "\<dots> \<le> e"
        using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
      finally show ?thesis by simp
    qed
    have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat
    proof (cases "n = m")
      case True
      with \<open>e > 0\<close> show ?thesis by simp
    next
      case False
      with *[of n m] *[of m n] and that show ?thesis
        by (auto simp: dist_commute nat_neq_iff)
    qed
    then show ?thesis by auto
  qed
  then have "Cauchy z"
    by (simp add: cauchy_def)
  then obtain x where "x\s" and x:"(z \ x) sequentially"
    using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto

  define e where "e = dist (f x) x"
  have "e = 0"
  proof (rule ccontr)
    assume "e \ 0"
    then have "e > 0"
      unfolding e_def using zero_le_dist[of "f x" x]
      by (metis dist_eq_0_iff dist_nz e_def)
    then obtain N where N:"\n\N. dist (z n) x < e/2"
      using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
    then have N':"dist (z N) x < e/2" by auto
    have *: "c * dist (z N) x \ dist (z N) x"
      unfolding mult_le_cancel_right2
      using zero_le_dist[of "z N" x] and c
      by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
    have "dist (f (z N)) (f x) \ c * dist (z N) x"
      using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
      using z_in_s[of N] \<open>x\<in>s\<close>
      using c
      by auto
    also have "\ < e/2"
      using N' and c using * by auto
    finally show False
      unfolding fzn
      using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]
      unfolding e_def
      by auto
  qed
  then have "f x = x" by (auto simp: e_def)
  moreover have "y = x" if "f y = y" "y \ s" for y
  proof -
    from \<open>x \<in> s\<close> \<open>f x = x\<close> that have "dist x y \<le> c * dist x y"
      using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp
    with c and zero_le_dist[of x y] have "dist x y = 0"
      by (simp add: mult_le_cancel_right1)
    then show ?thesis by simp
  qed
  ultimately show ?thesis
    using \<open>x\<in>s\<close> by blast
qed

subsection \<open>Edelstein fixed point theorem\<close>

theorem Edelstein_fix:
  fixes S :: "'a::metric_space set"
  assumes S: "compact S" "S \ {}"
    and gs: "(g ` S) \ S"
    and dist: "\x\S. \y\S. x \ y \ dist (g x) (g y) < dist x y"
  shows "\!x\S. g x = x"
proof -
  let ?D = "(\x. (x, x)) ` S"
  have D: "compact ?D" "?D \ {}"
    by (rule compact_continuous_image)
       (auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)

  have "\x y e. x \ S \ y \ S \ 0 < e \ dist y x < e \ dist (g y) (g x) < e"
    using dist by fastforce
  then have "continuous_on S g"
    by (auto simp: continuous_on_iff)
  then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))"
    unfolding continuous_on_eq_continuous_within
    by (intro continuous_dist ballI continuous_within_compose)
       (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)

  obtain a where "a \ S" and le: "\x. x \ S \ dist (g a) a \ dist (g x) x"
    using continuous_attains_inf[OF D cont] by auto

  have "g a = a"
  proof (rule ccontr)
    assume "g a \ a"
    with \<open>a \<in> S\<close> gs have "dist (g (g a)) (g a) < dist (g a) a"
      by (intro dist[rule_format]) auto
    moreover have "dist (g a) a \ dist (g (g a)) (g a)"
      using \<open>a \<in> S\<close> gs by (intro le) auto
    ultimately show False by auto
  qed
  moreover have "\x. x \ S \ g x = x \ x = a"
    using dist[THEN bspec[where x=a]] \<open>g a = a\<close> and \<open>a\<in>S\<close> by auto
  ultimately show "\!x\S. g x = x"
    using \<open>a \<in> S\<close> by blast
qed

subsection \<open>The diameter of a set\<close>

definition\<^marker>\<open>tag important\<close> diameter :: "'a::metric_space set \<Rightarrow> real" where
  "diameter S = (if S = {} then 0 else SUP (x,y)\S\S. dist x y)"

lemma diameter_empty [simp]: "diameter{} = 0"
  by (auto simp: diameter_def)

lemma diameter_singleton [simp]: "diameter{x} = 0"
  by (auto simp: diameter_def)

lemma diameter_le:
  assumes "S \ {} \ 0 \ d"
    and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d"
  shows "diameter S \ d"
  using assms
  by (auto simp: dist_norm diameter_def intro: cSUP_least)

lemma diameter_bounded_bound:
  fixes S :: "'a :: metric_space set"
  assumes S: "bounded S" "x \ S" "y \ S"
  shows "dist x y \ diameter S"
proof -
  from S obtain z d where z: "\x. x \ S \ dist z x \ d"
    unfolding bounded_def by auto
  have "bdd_above (case_prod dist ` (S\S))"
  proof (intro bdd_aboveI, safe)
    fix a b
    assume "a \ S" "b \ S"
    with z[of a] z[of b] dist_triangle[of a b z]
    show "dist a b \ 2 * d"
      by (simp add: dist_commute)
  qed
  moreover have "(x,y) \ S\S" using S by auto
  ultimately have "dist x y \ (SUP (x,y)\S\S. dist x y)"
    by (rule cSUP_upper2) simp
  with \<open>x \<in> S\<close> show ?thesis
    by (auto simp: diameter_def)
qed

lemma diameter_lower_bounded:
  fixes S :: "'a :: metric_space set"
  assumes S: "bounded S"
    and d: "0 < d" "d < diameter S"
  shows "\x\S. \y\S. d < dist x y"
proof (rule ccontr)
  assume contr: "\ ?thesis"
  moreover have "S \ {}"
    using d by (auto simp: diameter_def)
  ultimately have "diameter S \ d"
    by (auto simp: not_less diameter_def intro!: cSUP_least)
  with \<open>d < diameter S\<close> show False by auto
qed

lemma diameter_bounded:
  assumes "bounded S"
  shows "\x\S. \y\S. dist x y \ diameter S"
    and "\d>0. d < diameter S \ (\x\S. \y\S. dist x y > d)"
  using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms
  by auto

lemma bounded_two_points: "bounded S \ (\e. \x\S. \y\S. dist x y \ e)"
  by (meson bounded_def diameter_bounded(1))

lemma diameter_compact_attained:
  assumes "compact S"
    and "S \ {}"
  shows "\x\S. \y\S. dist x y = diameter S"
proof -
  have b: "bounded S" using assms(1)
    by (rule compact_imp_bounded)
  then obtain x y where xys: "x\S" "y\S"
    and xy: "\u\S. \v\S. dist u v \ dist x y"
    using compact_sup_maxdistance[OF assms] by auto
  then have "diameter S \ dist x y"
    unfolding diameter_def
    apply clarsimp
    apply (rule cSUP_least, fast+)
    done
  then show ?thesis
    by (metis b diameter_bounded_bound order_antisym xys)
qed

lemma diameter_ge_0:
  assumes "bounded S"  shows "0 \ diameter S"
  by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)

lemma diameter_subset:
  assumes "S \ T" "bounded T"
  shows "diameter S \ diameter T"
proof (cases "S = {} \ T = {}")
  case True
  with assms show ?thesis
    by (force simp: diameter_ge_0)
next
  case False
  then have "bdd_above ((\x. case x of (x, xa) \ dist x xa) ` (T \ T))"
    using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
  with False \<open>S \<subseteq> T\<close> show ?thesis
    apply (simp add: diameter_def)
    apply (rule cSUP_subset_mono, auto)
    done
qed

lemma diameter_closure:
  assumes "bounded S"
  shows "diameter(closure S) = diameter S"
proof (rule order_antisym)
  have "False" if "diameter S < diameter (closure S)"
  proof -
    define d where "d = diameter(closure S) - diameter(S)"
    have "d > 0"
      using that by (simp add: d_def)
    then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
      by simp
    have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
      by (simp add: d_def field_split_simps)
     have bocl: "bounded (closure S)"
      using assms by blast
    moreover have "0 \ diameter S"
      using assms diameter_ge_0 by blast
    ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
      using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
    then obtain x' y' where x'y': "x' \ S" "dist x' x < d/4" "y' \ S" "dist y' y < d/4"
      using closure_approachable
      by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
    then have "dist x' y' \ diameter S"
      using assms diameter_bounded_bound by blast
    with x'y' have "dist x y \ d / 4 + diameter S + d / 4"
      by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
    then show ?thesis
      using xy d_def by linarith
  qed
  then show "diameter (closure S) \ diameter S"
    by fastforce
  next
    show "diameter S \ diameter (closure S)"
      by (simp add: assms bounded_closure closure_subset diameter_subset)
qed

proposition Lebesgue_number_lemma:
  assumes "compact S" "\ \ {}" "S \ \\" and ope: "\B. B \ \ \ open B"
  obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
proof (cases "S = {}")
  case True
  then show ?thesis
    by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
next
  case False
  { fix x assume "x \ S"
    then obtain C where C: "x \ C" "C \ \"
      using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
    then obtain r where r: "r>0" "ball x (2*r) \ C"
      by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)
    then have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \"
      using C by blast
  }
  then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)"
    by metis
  then have "S \ (\x \ S. ball x (r x))"
    by auto
  then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
    by (rule compactE [OF \<open>compact S\<close>]) auto
  then obtain S0 where "S0 \ S" "finite S0" and S0: "\ = (\x. ball x (r x)) ` S0"
    by (meson finite_subset_image)
  then have "S0 \ {}"
    using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
  define \<delta> where "\<delta> = Inf (r ` S0)"
  have "\ > 0"
    using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
  show ?thesis
  proof
    show "0 < \"
      by (simp add: \<open>0 < \<delta>\<close>)
    show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T
    proof (cases "T = {}")
      case True
      then show ?thesis
        using \<open>\<C> \<noteq> {}\<close> by blast
    next
      case False
      then obtain y where "y \ T" by blast
      then have "y \ S"
        using \<open>T \<subseteq> S\<close> by auto
      then obtain x where "x \ S0" and x: "y \ ball x (r x)"
        using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
      have "ball y \ \ ball y (r x)"
        by (metis \<delta>_def \<open>S0 \<noteq> {}\<close> \<open>finite S0\<close> \<open>x \<in> S0\<close> empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)
      also have "... \ ball x (2*r x)"
        using x by metric
      finally obtain C where "C \ \" "ball y \ \ C"
        by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
      have "bounded T"
        using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
      then have "T \ ball y \"
        using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
      then show ?thesis
        apply (rule_tac x=C in bexI)
        using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
    qed
  qed
qed

subsection \<open>Metric spaces with the Heine-Borel property\<close>

text \<open>
  A metric space (or topological vector space) is said to have the
  Heine-Borel property if every closed and bounded subset is compact.
\<close>

class heine_borel = metric_space +
  assumes bounded_imp_convergent_subsequence:
    "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially"

proposition bounded_closed_imp_seq_compact:
  fixes S::"'a::heine_borel set"
  assumes "bounded S"
    and "closed S"
  shows "seq_compact S"
proof (unfold seq_compact_def, clarify)
  fix f :: "nat \ 'a"
  assume f: "\n. f n \ S"
  with \<open>bounded S\<close> have "bounded (range f)"
    by (auto intro: bounded_subset)
  obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially"
    using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
  from f have fr: "\n. (f \ r) n \ S"
    by simp
  have "l \ S" using \closed S\ fr l
    by (rule closed_sequentially)
  show "\l\S. \r. strict_mono r \ ((f \ r) \ l) sequentially"
    using \<open>l \<in> S\<close> r l by blast
qed

lemma compact_eq_bounded_closed:
  fixes S :: "'a::heine_borel set"
  shows "compact S \ bounded S \ closed S"
  using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed
  by auto

lemma compact_Inter:
  fixes \<F> :: "'a :: heine_borel set set"
  assumes com: "\S. S \ \ \ compact S" and "\ \ {}"
  shows "compact(\ \)"
  using assms
  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)

lemma compact_closure [simp]:
  fixes S :: "'a::heine_borel set"
  shows "compact(closure S) \ bounded S"
by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)

instance\<^marker>\<open>tag important\<close> real :: heine_borel
proof
  fix f :: "nat \ real"
  assume f: "bounded (range f)"
  obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)"
    unfolding comp_def by (metis seq_monosub)
  then have "Bseq (f \ r)"
    unfolding Bseq_eq_bounded using f
    by (metis BseqI' bounded_iff comp_apply rangeI)
  with r show "\l r. strict_mono r \ (f \ r) \ l"
    using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def)
qed

lemma compact_lemma_general:
  fixes f :: "nat \ 'a"
  fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60)
  fixes unproj:: "('b \ 'c) \ 'a"
  assumes finite_basis: "finite basis"
  assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)"
  assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k"
  assumes unproj_proj: "\x. unproj (\k. x proj k) = x"
  shows "\d\basis. \l::'a. \ r::nat\nat.
    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
proof safe
  fix d :: "'b set"
  assume d: "d \ basis"
  with finite_basis have "finite d"
    by (blast intro: finite_subset)
  from this d show "\l::'a. \r::nat\nat. strict_mono r \
    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
  proof (induct d)
    case empty
    then show ?case
      unfolding strict_mono_def by auto
  next
    case (insert k d)
    have k[intro]: "k \ basis"
      using insert by auto
    have s': "bounded ((\x. x proj k) ` range f)"
      using k
      by (rule bounded_proj)
    obtain l1::"'a" and r1 where r1: "strict_mono r1"
      and lr1: "\e > 0. eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
      using insert(3) using insert(4) by auto
    have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f"
      by simp
    have "bounded (range (\i. f (r1 i) proj k))"
      by (metis (lifting) bounded_subset f' image_subsetI s')
    then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\i. f (r1 (r2 i)) proj k) \ l2) sequentially"
      using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"]
      by (auto simp: o_def)
    define r where "r = r1 \ r2"
    have r:"strict_mono r"
      using r1 and r2 unfolding r_def o_def strict_mono_def by auto
    moreover
    define l where "l = unproj (\i. if i = k then l2 else l1 proj i)"
    {
      fix e::real
      assume "e > 0"
      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
        by blast
      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"
        by (rule tendstoD)
      from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"
        by (rule eventually_subseq)
      have "eventually (\n. \i\(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"
        using N1' N2
        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)
    }
    ultimately show ?case by auto
  qed
qed

lemma bounded_fst: "bounded s \ bounded (fst ` s)"
  unfolding bounded_def
  by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)

lemma bounded_snd: "bounded s \ bounded (snd ` s)"
  unfolding bounded_def
  by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)

instance\<^marker>\<open>tag important\<close> prod :: (heine_borel, heine_borel) heine_borel
proof
  fix f :: "nat \ 'a \ 'b"
  assume f: "bounded (range f)"
  then have "bounded (fst ` range f)"
    by (rule bounded_fst)
  then have s1: "bounded (range (fst \ f))"
    by (simp add: image_comp)
  obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1"
    using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
  from f have s2: "bounded (range (snd \ f \ r1))"
    by (auto simp: image_comp intro: bounded_snd bounded_subset)
  obtain l2 r2 where r2: "strict_mono r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially"
    using bounded_imp_convergent_subsequence [OF s2]
    unfolding o_def by fast
  have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.54 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.