src/HOL/Analysis/Elementary_Metric_Spaces.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69922 4a9167f377b0
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
immler@69544
     1
(*  Author:     L C Paulson, University of Cambridge
immler@69544
     2
    Author:     Amine Chaieb, University of Cambridge
immler@69544
     3
    Author:     Robert Himmelmann, TU Muenchen
immler@69544
     4
    Author:     Brian Huffman, Portland State University
immler@69544
     5
*)
immler@69544
     6
immler@69676
     7
chapter \<open>Functional Analysis\<close>
immler@69544
     8
immler@69544
     9
theory Elementary_Metric_Spaces
immler@69544
    10
  imports
immler@69616
    11
    Abstract_Topology_2
immler@69544
    12
begin
immler@69544
    13
immler@69676
    14
section \<open>Elementary Metric Spaces\<close>
immler@69676
    15
immler@69544
    16
subsection \<open>Open and closed balls\<close>
immler@69544
    17
immler@69544
    18
definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
immler@69544
    19
  where "ball x e = {y. dist x y < e}"
immler@69544
    20
immler@69544
    21
definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
immler@69544
    22
  where "cball x e = {y. dist x y \<le> e}"
immler@69544
    23
immler@69544
    24
definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
immler@69544
    25
  where "sphere x e = {y. dist x y = e}"
immler@69544
    26
immler@69544
    27
lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
immler@69544
    28
  by (simp add: ball_def)
immler@69544
    29
immler@69544
    30
lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
immler@69544
    31
  by (simp add: cball_def)
immler@69544
    32
immler@69544
    33
lemma mem_sphere [simp]: "y \<in> sphere x e \<longleftrightarrow> dist x y = e"
immler@69544
    34
  by (simp add: sphere_def)
immler@69544
    35
immler@69544
    36
lemma ball_trivial [simp]: "ball x 0 = {}"
immler@69544
    37
  by (simp add: ball_def)
immler@69544
    38
immler@69544
    39
lemma cball_trivial [simp]: "cball x 0 = {x}"
immler@69544
    40
  by (simp add: cball_def)
immler@69544
    41
immler@69544
    42
lemma sphere_trivial [simp]: "sphere x 0 = {x}"
immler@69544
    43
  by (simp add: sphere_def)
immler@69544
    44
immler@69544
    45
lemma disjoint_ballI: "dist x y \<ge> r+s \<Longrightarrow> ball x r \<inter> ball y s = {}"
immler@69544
    46
  using dist_triangle_less_add not_le by fastforce
immler@69544
    47
immler@69544
    48
lemma disjoint_cballI: "dist x y > r + s \<Longrightarrow> cball x r \<inter> cball y s = {}"
immler@69544
    49
  by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)
immler@69544
    50
immler@69544
    51
lemma sphere_empty [simp]: "r < 0 \<Longrightarrow> sphere a r = {}"
immler@69544
    52
  for a :: "'a::metric_space"
immler@69544
    53
  by auto
immler@69544
    54
immler@69544
    55
lemma centre_in_ball [simp]: "x \<in> ball x e \<longleftrightarrow> 0 < e"
immler@69544
    56
  by simp
immler@69544
    57
immler@69544
    58
lemma centre_in_cball [simp]: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
immler@69544
    59
  by simp
immler@69544
    60
immler@69544
    61
lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"
immler@69544
    62
  by (simp add: subset_eq)
immler@69544
    63
immler@69544
    64
lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
immler@69544
    65
  by (auto simp: mem_ball mem_cball)
immler@69544
    66
immler@69544
    67
lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
immler@69544
    68
  by force
immler@69544
    69
immler@69544
    70
lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"
immler@69544
    71
  by auto
immler@69544
    72
immler@69544
    73
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
immler@69544
    74
  by (simp add: subset_eq)
immler@69544
    75
immler@69544
    76
lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
immler@69544
    77
  by (simp add: subset_eq)
immler@69544
    78
immler@69544
    79
lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
immler@69544
    80
  by (auto simp: mem_ball mem_cball)
immler@69544
    81
immler@69544
    82
lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
immler@69544
    83
  by (auto simp: mem_ball mem_cball)
immler@69544
    84
immler@69544
    85
lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
immler@69544
    86
  unfolding mem_cball
immler@69544
    87
proof -
immler@69544
    88
  have "dist z x \<le> dist z y + dist y x"
immler@69544
    89
    by (rule dist_triangle)
immler@69544
    90
  also assume "dist z y \<le> b"
immler@69544
    91
  also assume "dist y x \<le> a"
immler@69544
    92
  finally show "dist z x \<le> b + a" by arith
immler@69544
    93
qed
immler@69544
    94
immler@69544
    95
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
immler@69544
    96
  by (simp add: set_eq_iff) arith
immler@69544
    97
immler@69544
    98
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
immler@69544
    99
  by (simp add: set_eq_iff)
immler@69544
   100
immler@69544
   101
lemma cball_max_Un: "cball a (max r s) = cball a r \<union> cball a s"
immler@69544
   102
  by (simp add: set_eq_iff) arith
immler@69544
   103
immler@69544
   104
lemma cball_min_Int: "cball a (min r s) = cball a r \<inter> cball a s"
immler@69544
   105
  by (simp add: set_eq_iff)
immler@69544
   106
immler@69544
   107
lemma cball_diff_eq_sphere: "cball a r - ball a r =  sphere a r"
immler@69544
   108
  by (auto simp: cball_def ball_def dist_commute)
immler@69544
   109
immler@69544
   110
lemma open_ball [intro, simp]: "open (ball x e)"
immler@69544
   111
proof -
immler@69544
   112
  have "open (dist x -` {..<e})"
immler@69544
   113
    by (intro open_vimage open_lessThan continuous_intros)
immler@69544
   114
  also have "dist x -` {..<e} = ball x e"
immler@69544
   115
    by auto
immler@69544
   116
  finally show ?thesis .
immler@69544
   117
qed
immler@69544
   118
immler@69544
   119
lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
immler@69544
   120
  by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute)
immler@69544
   121
immler@69544
   122
lemma openI [intro?]: "(\<And>x. x\<in>S \<Longrightarrow> \<exists>e>0. ball x e \<subseteq> S) \<Longrightarrow> open S"
immler@69544
   123
  by (auto simp: open_contains_ball)
immler@69544
   124
immler@69544
   125
lemma openE[elim?]:
immler@69544
   126
  assumes "open S" "x\<in>S"
immler@69544
   127
  obtains e where "e>0" "ball x e \<subseteq> S"
immler@69544
   128
  using assms unfolding open_contains_ball by auto
immler@69544
   129
immler@69544
   130
lemma open_contains_ball_eq: "open S \<Longrightarrow> x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
immler@69544
   131
  by (metis open_contains_ball subset_eq centre_in_ball)
immler@69544
   132
immler@69544
   133
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
immler@69544
   134
  unfolding mem_ball set_eq_iff
immler@69544
   135
  apply (simp add: not_less)
immler@69544
   136
  apply (metis zero_le_dist order_trans dist_self)
immler@69544
   137
  done
immler@69544
   138
immler@69544
   139
lemma ball_empty: "e \<le> 0 \<Longrightarrow> ball x e = {}" by simp
immler@69544
   140
immler@69544
   141
lemma closed_cball [iff]: "closed (cball x e)"
immler@69544
   142
proof -
immler@69544
   143
  have "closed (dist x -` {..e})"
immler@69544
   144
    by (intro closed_vimage closed_atMost continuous_intros)
immler@69544
   145
  also have "dist x -` {..e} = cball x e"
immler@69544
   146
    by auto
immler@69544
   147
  finally show ?thesis .
immler@69544
   148
qed
immler@69544
   149
immler@69544
   150
lemma open_contains_cball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0.  cball x e \<subseteq> S)"
immler@69544
   151
proof -
immler@69544
   152
  {
immler@69544
   153
    fix x and e::real
immler@69544
   154
    assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
immler@69544
   155
    then have "\<exists>d>0. cball x d \<subseteq> S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
immler@69544
   156
  }
immler@69544
   157
  moreover
immler@69544
   158
  {
immler@69544
   159
    fix x and e::real
immler@69544
   160
    assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
immler@69544
   161
    then have "\<exists>d>0. ball x d \<subseteq> S"
immler@69544
   162
      unfolding subset_eq
immler@69544
   163
      apply (rule_tac x="e/2" in exI, auto)
immler@69544
   164
      done
immler@69544
   165
  }
immler@69544
   166
  ultimately show ?thesis
immler@69544
   167
    unfolding open_contains_ball by auto
immler@69544
   168
qed
immler@69544
   169
immler@69544
   170
lemma open_contains_cball_eq: "open S \<Longrightarrow> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
immler@69544
   171
  by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)
immler@69544
   172
immler@69544
   173
lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
immler@69544
   174
  by (rule eventually_nhds_in_open) simp_all
immler@69544
   175
immler@69544
   176
lemma eventually_at_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<in> A) (at z within A)"
immler@69544
   177
  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
immler@69544
   178
immler@69544
   179
lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
immler@69544
   180
  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
immler@69544
   181
immler@69544
   182
lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"
immler@69544
   183
  by (subst at_within_open) auto
immler@69544
   184
immler@69544
   185
lemma atLeastAtMost_eq_cball:
immler@69544
   186
  fixes a b::real
immler@69544
   187
  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
immler@69544
   188
  by (auto simp: dist_real_def field_simps mem_cball)
immler@69544
   189
immler@69544
   190
lemma greaterThanLessThan_eq_ball:
immler@69544
   191
  fixes a b::real
immler@69544
   192
  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
immler@69544
   193
  by (auto simp: dist_real_def field_simps mem_ball)
immler@69544
   194
immler@69611
   195
lemma interior_ball [simp]: "interior (ball x e) = ball x e"
immler@69611
   196
  by (simp add: interior_open)
immler@69611
   197
immler@69611
   198
lemma cball_eq_empty [simp]: "cball x e = {} \<longleftrightarrow> e < 0"
immler@69611
   199
  apply (simp add: set_eq_iff not_le)
immler@69611
   200
  apply (metis zero_le_dist dist_self order_less_le_trans)
immler@69611
   201
  done
immler@69611
   202
immler@69611
   203
lemma cball_empty [simp]: "e < 0 \<Longrightarrow> cball x e = {}"
immler@69611
   204
  by simp
immler@69611
   205
immler@69611
   206
lemma cball_sing:
immler@69611
   207
  fixes x :: "'a::metric_space"
immler@69611
   208
  shows "e = 0 \<Longrightarrow> cball x e = {x}"
immler@69611
   209
  by (auto simp: set_eq_iff)
immler@69611
   210
immler@69611
   211
lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
immler@69611
   212
  apply (cases "e \<le> 0")
immler@69611
   213
  apply (simp add: ball_empty divide_simps)
immler@69611
   214
  apply (rule subset_ball)
immler@69611
   215
  apply (simp add: divide_simps)
immler@69611
   216
  done
immler@69611
   217
immler@69611
   218
lemma ball_divide_subset_numeral: "ball x (e / numeral w) \<subseteq> ball x e"
immler@69611
   219
  using ball_divide_subset one_le_numeral by blast
immler@69611
   220
immler@69611
   221
lemma cball_divide_subset: "d \<ge> 1 \<Longrightarrow> cball x (e/d) \<subseteq> cball x e"
immler@69611
   222
  apply (cases "e < 0")
immler@69611
   223
  apply (simp add: divide_simps)
immler@69611
   224
  apply (rule subset_cball)
immler@69611
   225
  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)
immler@69611
   226
  done
immler@69611
   227
immler@69611
   228
lemma cball_divide_subset_numeral: "cball x (e / numeral w) \<subseteq> cball x e"
immler@69611
   229
  using cball_divide_subset one_le_numeral by blast
immler@69611
   230
immler@69544
   231
immler@69544
   232
subsection \<open>Limit Points\<close>
immler@69544
   233
immler@69544
   234
lemma islimpt_approachable:
immler@69544
   235
  fixes x :: "'a::metric_space"
immler@69544
   236
  shows "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e)"
immler@69544
   237
  unfolding islimpt_iff_eventually eventually_at by fast
immler@69544
   238
immler@69544
   239
lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x \<le> e)"
immler@69544
   240
  for x :: "'a::metric_space"
immler@69544
   241
  unfolding islimpt_approachable
immler@69544
   242
  using approachable_lt_le [where f="\<lambda>y. dist y x" and P="\<lambda>y. y \<notin> S \<or> y = x",
immler@69544
   243
    THEN arg_cong [where f=Not]]
immler@69544
   244
  by (simp add: Bex_def conj_commute conj_left_commute)
immler@69544
   245
immler@69544
   246
lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \<Longrightarrow> x islimpt S"
immler@69544
   247
  for x :: "'a::metric_space"
immler@69544
   248
  apply (clarsimp simp add: islimpt_approachable)
immler@69544
   249
  apply (drule_tac x="e/2" in spec)
immler@69544
   250
  apply (auto simp: simp del: less_divide_eq_numeral1)
immler@69544
   251
  apply (drule_tac x="dist x' x" in spec)
immler@69544
   252
  apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)
immler@69544
   253
  apply (erule rev_bexI)
immler@69544
   254
  apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl)
immler@69544
   255
  done
immler@69544
   256
immler@69544
   257
lemma closed_limpts:  "closed {x::'a::metric_space. x islimpt S}"
immler@69544
   258
  using closed_limpt limpt_of_limpts by blast
immler@69544
   259
immler@69544
   260
lemma limpt_of_closure: "x islimpt closure S \<longleftrightarrow> x islimpt S"
immler@69544
   261
  for x :: "'a::metric_space"
immler@69544
   262
  by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)
immler@69544
   263
immler@69544
   264
lemma islimpt_eq_infinite_ball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> ball x e))"
immler@69544
   265
  apply (simp add: islimpt_eq_acc_point, safe)
immler@69544
   266
   apply (metis Int_commute open_ball centre_in_ball)
immler@69544
   267
  by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)
immler@69544
   268
immler@69544
   269
lemma islimpt_eq_infinite_cball: "x islimpt S \<longleftrightarrow> (\<forall>e>0. infinite(S \<inter> cball x e))"
immler@69544
   270
  apply (simp add: islimpt_eq_infinite_ball, safe)
immler@69544
   271
   apply (meson Int_mono ball_subset_cball finite_subset order_refl)
immler@69544
   272
  by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)
immler@69544
   273
immler@69544
   274
immler@69611
   275
subsection \<open>Perfect Metric Spaces\<close>
immler@69611
   276
immler@69611
   277
lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
immler@69611
   278
  for x :: "'a::{perfect_space,metric_space}"
immler@69611
   279
  using islimpt_UNIV [of x] by (simp add: islimpt_approachable)
immler@69611
   280
immler@69611
   281
lemma cball_eq_sing:
immler@69611
   282
  fixes x :: "'a::{metric_space,perfect_space}"
immler@69611
   283
  shows "cball x e = {x} \<longleftrightarrow> e = 0"
immler@69611
   284
proof (rule linorder_cases)
immler@69611
   285
  assume e: "0 < e"
immler@69611
   286
  obtain a where "a \<noteq> x" "dist a x < e"
immler@69611
   287
    using perfect_choose_dist [OF e] by auto
immler@69611
   288
  then have "a \<noteq> x" "dist x a \<le> e"
immler@69611
   289
    by (auto simp: dist_commute)
immler@69611
   290
  with e show ?thesis by (auto simp: set_eq_iff)
immler@69611
   291
qed auto
immler@69611
   292
immler@69611
   293
immler@69544
   294
subsection \<open>?\<close>
immler@69544
   295
immler@69544
   296
lemma finite_ball_include:
immler@69544
   297
  fixes a :: "'a::metric_space"
immler@69544
   298
  assumes "finite S" 
immler@69544
   299
  shows "\<exists>e>0. S \<subseteq> ball a e"
immler@69544
   300
  using assms
immler@69544
   301
proof induction
immler@69544
   302
  case (insert x S)
immler@69544
   303
  then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto
immler@69544
   304
  define e where "e = max e0 (2 * dist a x)"
immler@69544
   305
  have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
immler@69544
   306
  moreover have "insert x S \<subseteq> ball a e"
immler@69544
   307
    using e0 \<open>e>0\<close> unfolding e_def by auto
immler@69544
   308
  ultimately show ?case by auto
immler@69544
   309
qed (auto intro: zero_less_one)
immler@69544
   310
immler@69544
   311
lemma finite_set_avoid:
immler@69544
   312
  fixes a :: "'a::metric_space"
immler@69544
   313
  assumes "finite S"
immler@69544
   314
  shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
immler@69544
   315
  using assms
immler@69544
   316
proof induction
immler@69544
   317
  case (insert x S)
immler@69544
   318
  then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
immler@69544
   319
    by blast
immler@69544
   320
  show ?case
immler@69544
   321
  proof (cases "x = a")
immler@69544
   322
    case True
immler@69544
   323
    with \<open>d > 0 \<close>d show ?thesis by auto
immler@69544
   324
  next
immler@69544
   325
    case False
immler@69544
   326
    let ?d = "min d (dist a x)"
immler@69544
   327
    from False \<open>d > 0\<close> have dp: "?d > 0"
immler@69544
   328
      by auto
immler@69544
   329
    from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
immler@69544
   330
      by auto
immler@69544
   331
    with dp False show ?thesis
immler@69544
   332
      by (metis insert_iff le_less min_less_iff_conj not_less)
immler@69544
   333
  qed
immler@69544
   334
qed (auto intro: zero_less_one)
immler@69544
   335
immler@69544
   336
lemma discrete_imp_closed:
immler@69544
   337
  fixes S :: "'a::metric_space set"
immler@69544
   338
  assumes e: "0 < e"
immler@69544
   339
    and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
immler@69544
   340
  shows "closed S"
immler@69544
   341
proof -
immler@69544
   342
  have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
immler@69544
   343
  proof -
immler@69544
   344
    from e have e2: "e/2 > 0" by arith
immler@69544
   345
    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
immler@69544
   346
      by blast
immler@69544
   347
    let ?m = "min (e/2) (dist x y) "
immler@69544
   348
    from e2 y(2) have mp: "?m > 0"
immler@69544
   349
      by simp
immler@69544
   350
    from C[OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
immler@69544
   351
      by blast
immler@69544
   352
    from z y have "dist z y < e"
immler@69544
   353
      by (intro dist_triangle_lt [where z=x]) simp
immler@69544
   354
    from d[rule_format, OF y(1) z(1) this] y z show ?thesis
immler@69544
   355
      by (auto simp: dist_commute)
immler@69544
   356
  qed
immler@69544
   357
  then show ?thesis
immler@69544
   358
    by (metis islimpt_approachable closed_limpt [where 'a='a])
immler@69544
   359
qed
immler@69544
   360
immler@69544
   361
immler@69544
   362
subsection \<open>Interior\<close>
immler@69544
   363
immler@69544
   364
lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
immler@69544
   365
  using open_contains_ball_eq [where S="interior S"]
immler@69544
   366
  by (simp add: open_subset_interior)
immler@69544
   367
immler@69611
   368
lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
immler@69611
   369
  by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior
immler@69611
   370
      subset_trans)
immler@69611
   371
immler@69544
   372
immler@69544
   373
subsection \<open>Frontier\<close>
immler@69544
   374
immler@69544
   375
lemma frontier_straddle:
immler@69544
   376
  fixes a :: "'a::metric_space"
immler@69544
   377
  shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
immler@69544
   378
  unfolding frontier_def closure_interior
immler@69544
   379
  by (auto simp: mem_interior subset_eq ball_def)
immler@69544
   380
immler@69544
   381
immler@69544
   382
subsection \<open>Limits\<close>
immler@69544
   383
immler@69544
   384
proposition Lim: "(f \<longlongrightarrow> l) net \<longleftrightarrow> trivial_limit net \<or> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
immler@69544
   385
  by (auto simp: tendsto_iff trivial_limit_eq)
immler@69544
   386
immler@69544
   387
text \<open>Show that they yield usual definitions in the various cases.\<close>
immler@69544
   388
immler@69544
   389
proposition Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
immler@69544
   390
    (\<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)"
immler@69544
   391
  by (auto simp: tendsto_iff eventually_at_le)
immler@69544
   392
immler@69544
   393
proposition Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
immler@69544
   394
    (\<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)"
immler@69544
   395
  by (auto simp: tendsto_iff eventually_at)
immler@69544
   396
immler@69544
   397
corollary Lim_withinI [intro?]:
immler@69544
   398
  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e"
immler@69544
   399
  shows "(f \<longlongrightarrow> l) (at a within S)"
immler@69544
   400
  apply (simp add: Lim_within, clarify)
immler@69544
   401
  apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
immler@69544
   402
  done
immler@69544
   403
immler@69544
   404
proposition Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
immler@69544
   405
    (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
immler@69544
   406
  by (auto simp: tendsto_iff eventually_at)
immler@69544
   407
immler@69544
   408
lemma Lim_transform_within_set:
immler@69544
   409
  fixes a :: "'a::metric_space" and l :: "'b::metric_space"
immler@69544
   410
  shows "\<lbrakk>(f \<longlongrightarrow> l) (at a within S); eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)\<rbrakk>
immler@69544
   411
         \<Longrightarrow> (f \<longlongrightarrow> l) (at a within T)"
immler@69544
   412
apply (clarsimp simp: eventually_at Lim_within)
immler@69544
   413
apply (drule_tac x=e in spec, clarify)
immler@69544
   414
apply (rename_tac k)
immler@69544
   415
apply (rule_tac x="min d k" in exI, simp)
immler@69544
   416
done
immler@69544
   417
immler@69544
   418
text \<open>Another limit point characterization.\<close>
immler@69544
   419
immler@69544
   420
lemma limpt_sequential_inj:
immler@69544
   421
  fixes x :: "'a::metric_space"
immler@69544
   422
  shows "x islimpt S \<longleftrightarrow>
immler@69544
   423
         (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> inj f \<and> (f \<longlongrightarrow> x) sequentially)"
immler@69544
   424
         (is "?lhs = ?rhs")
immler@69544
   425
proof
immler@69544
   426
  assume ?lhs
immler@69544
   427
  then have "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
immler@69544
   428
    by (force simp: islimpt_approachable)
immler@69544
   429
  then obtain y where y: "\<And>e. e>0 \<Longrightarrow> y e \<in> S \<and> y e \<noteq> x \<and> dist (y e) x < e"
immler@69544
   430
    by metis
immler@69544
   431
  define f where "f \<equiv> rec_nat (y 1) (\<lambda>n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"
immler@69544
   432
  have [simp]: "f 0 = y 1"
immler@69544
   433
               "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n
immler@69544
   434
    by (simp_all add: f_def)
immler@69544
   435
  have f: "f n \<in> S \<and> (f n \<noteq> x) \<and> dist (f n) x < inverse(2 ^ n)" for n
immler@69544
   436
  proof (induction n)
immler@69544
   437
    case 0 show ?case
immler@69544
   438
      by (simp add: y)
immler@69544
   439
  next
immler@69544
   440
    case (Suc n) then show ?case
immler@69544
   441
      apply (auto simp: y)
immler@69544
   442
      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)
immler@69544
   443
  qed
immler@69544
   444
  show ?rhs
immler@69544
   445
  proof (rule_tac x=f in exI, intro conjI allI)
immler@69544
   446
    show "\<And>n. f n \<in> S - {x}"
immler@69544
   447
      using f by blast
immler@69544
   448
    have "dist (f n) x < dist (f m) x" if "m < n" for m n
immler@69544
   449
    using that
immler@69544
   450
    proof (induction n)
immler@69544
   451
      case 0 then show ?case by simp
immler@69544
   452
    next
immler@69544
   453
      case (Suc n)
immler@69544
   454
      then consider "m < n" | "m = n" using less_Suc_eq by blast
immler@69544
   455
      then show ?case
immler@69544
   456
      proof cases
immler@69544
   457
        assume "m < n"
immler@69544
   458
        have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
immler@69544
   459
          by simp
immler@69544
   460
        also have "\<dots> < dist (f n) x"
immler@69544
   461
          by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
immler@69544
   462
        also have "\<dots> < dist (f m) x"
immler@69544
   463
          using Suc.IH \<open>m < n\<close> by blast
immler@69544
   464
        finally show ?thesis .
immler@69544
   465
      next
immler@69544
   466
        assume "m = n" then show ?case
immler@69544
   467
          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)
immler@69544
   468
      qed
immler@69544
   469
    qed
immler@69544
   470
    then show "inj f"
immler@69544
   471
      by (metis less_irrefl linorder_injI)
immler@69544
   472
    show "f \<longlonglongrightarrow> x"
immler@69544
   473
      apply (rule tendstoI)
immler@69544
   474
      apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)
immler@69544
   475
      apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])
immler@69544
   476
      apply (simp add: field_simps)
immler@69544
   477
      by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)
immler@69544
   478
  qed
immler@69544
   479
next
immler@69544
   480
  assume ?rhs
immler@69544
   481
  then show ?lhs
immler@69544
   482
    by (fastforce simp add: islimpt_approachable lim_sequentially)
immler@69544
   483
qed
immler@69544
   484
immler@69544
   485
lemma Lim_dist_ubound:
immler@69544
   486
  assumes "\<not>(trivial_limit net)"
immler@69544
   487
    and "(f \<longlongrightarrow> l) net"
immler@69544
   488
    and "eventually (\<lambda>x. dist a (f x) \<le> e) net"
immler@69544
   489
  shows "dist a l \<le> e"
immler@69544
   490
  using assms by (fast intro: tendsto_le tendsto_intros)
immler@69544
   491
immler@69544
   492
immler@69613
   493
subsection \<open>Continuity\<close>
immler@69613
   494
immler@69613
   495
text\<open>Derive the epsilon-delta forms, which we often use as "definitions"\<close>
immler@69613
   496
immler@69613
   497
proposition continuous_within_eps_delta:
immler@69613
   498
  "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
immler@69613
   499
  unfolding continuous_within and Lim_within  by fastforce
immler@69613
   500
immler@69613
   501
corollary continuous_at_eps_delta:
immler@69613
   502
  "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
immler@69613
   503
  using continuous_within_eps_delta [of x UNIV f] by simp
immler@69613
   504
immler@69613
   505
lemma continuous_at_right_real_increasing:
immler@69613
   506
  fixes f :: "real \<Rightarrow> real"
immler@69613
   507
  assumes nondecF: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y"
immler@69613
   508
  shows "continuous (at_right a) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f (a + d) - f a < e)"
immler@69613
   509
  apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
immler@69613
   510
  apply (intro all_cong ex_cong, safe)
immler@69613
   511
  apply (erule_tac x="a + d" in allE, simp)
immler@69613
   512
  apply (simp add: nondecF field_simps)
immler@69613
   513
  apply (drule nondecF, simp)
immler@69613
   514
  done
immler@69613
   515
immler@69613
   516
lemma continuous_at_left_real_increasing:
immler@69613
   517
  assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
immler@69613
   518
  shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
immler@69613
   519
  apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
immler@69613
   520
  apply (intro all_cong ex_cong, safe)
immler@69613
   521
  apply (erule_tac x="a - d" in allE, simp)
immler@69613
   522
  apply (simp add: nondecF field_simps)
immler@69613
   523
  apply (cut_tac x="a - d" and y=x in nondecF, simp_all)
immler@69613
   524
  done
immler@69613
   525
immler@69613
   526
text\<open>Versions in terms of open balls.\<close>
immler@69613
   527
immler@69613
   528
lemma continuous_within_ball:
immler@69613
   529
  "continuous (at x within s) f \<longleftrightarrow>
immler@69613
   530
    (\<forall>e > 0. \<exists>d > 0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e)"
immler@69613
   531
  (is "?lhs = ?rhs")
immler@69613
   532
proof
immler@69613
   533
  assume ?lhs
immler@69613
   534
  {
immler@69613
   535
    fix e :: real
immler@69613
   536
    assume "e > 0"
immler@69613
   537
    then obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"
immler@69613
   538
      using \<open>?lhs\<close>[unfolded continuous_within Lim_within] by auto
immler@69613
   539
    {
immler@69613
   540
      fix y
immler@69613
   541
      assume "y \<in> f ` (ball x d \<inter> s)"
immler@69613
   542
      then have "y \<in> ball (f x) e"
immler@69613
   543
        using d(2)
immler@69613
   544
        apply (auto simp: dist_commute)
immler@69613
   545
        apply (erule_tac x=xa in ballE, auto)
immler@69613
   546
        using \<open>e > 0\<close>
immler@69613
   547
        apply auto
immler@69613
   548
        done
immler@69613
   549
    }
immler@69613
   550
    then have "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e"
immler@69613
   551
      using \<open>d > 0\<close>
immler@69613
   552
      unfolding subset_eq ball_def by (auto simp: dist_commute)
immler@69613
   553
  }
immler@69613
   554
  then show ?rhs by auto
immler@69613
   555
next
immler@69613
   556
  assume ?rhs
immler@69613
   557
  then show ?lhs
immler@69613
   558
    unfolding continuous_within Lim_within ball_def subset_eq
immler@69613
   559
    apply (auto simp: dist_commute)
immler@69613
   560
    apply (erule_tac x=e in allE, auto)
immler@69613
   561
    done
immler@69613
   562
qed
immler@69613
   563
immler@69613
   564
lemma continuous_at_ball:
immler@69613
   565
  "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
immler@69613
   566
proof
immler@69613
   567
  assume ?lhs
immler@69613
   568
  then show ?rhs
immler@69613
   569
    unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
immler@69613
   570
    apply auto
immler@69613
   571
    apply (erule_tac x=e in allE, auto)
immler@69613
   572
    apply (rule_tac x=d in exI, auto)
immler@69613
   573
    apply (erule_tac x=xa in allE)
immler@69613
   574
    apply (auto simp: dist_commute)
immler@69613
   575
    done
immler@69613
   576
next
immler@69613
   577
  assume ?rhs
immler@69613
   578
  then show ?lhs
immler@69613
   579
    unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
immler@69613
   580
    apply auto
immler@69613
   581
    apply (erule_tac x=e in allE, auto)
immler@69613
   582
    apply (rule_tac x=d in exI, auto)
immler@69613
   583
    apply (erule_tac x="f xa" in allE)
immler@69613
   584
    apply (auto simp: dist_commute)
immler@69613
   585
    done
immler@69613
   586
qed
immler@69613
   587
immler@69613
   588
text\<open>Define setwise continuity in terms of limits within the set.\<close>
immler@69613
   589
immler@69613
   590
lemma continuous_on_iff:
immler@69613
   591
  "continuous_on s f \<longleftrightarrow>
immler@69613
   592
    (\<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)"
immler@69613
   593
  unfolding continuous_on_def Lim_within
immler@69613
   594
  by (metis dist_pos_lt dist_self)
immler@69613
   595
immler@69613
   596
lemma continuous_within_E:
immler@69613
   597
  assumes "continuous (at x within s) f" "e>0"
immler@69613
   598
  obtains d where "d>0"  "\<And>x'. \<lbrakk>x'\<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
immler@69613
   599
  using assms apply (simp add: continuous_within_eps_delta)
immler@69613
   600
  apply (drule spec [of _ e], clarify)
immler@69613
   601
  apply (rule_tac d="d/2" in that, auto)
immler@69613
   602
  done
immler@69613
   603
immler@69613
   604
lemma continuous_onI [intro?]:
immler@69613
   605
  assumes "\<And>x e. \<lbrakk>e > 0; x \<in> s\<rbrakk> \<Longrightarrow> \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
immler@69613
   606
  shows "continuous_on s f"
immler@69613
   607
apply (simp add: continuous_on_iff, clarify)
immler@69613
   608
apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
immler@69613
   609
done
immler@69613
   610
immler@69613
   611
text\<open>Some simple consequential lemmas.\<close>
immler@69613
   612
immler@69613
   613
lemma continuous_onE:
immler@69613
   614
    assumes "continuous_on s f" "x\<in>s" "e>0"
immler@69613
   615
    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
immler@69613
   616
  using assms
immler@69613
   617
  apply (simp add: continuous_on_iff)
immler@69613
   618
  apply (elim ballE allE)
immler@69613
   619
  apply (auto intro: that [where d="d/2" for d])
immler@69613
   620
  done
immler@69613
   621
immler@69613
   622
text\<open>The usual transformation theorems.\<close>
immler@69613
   623
immler@69613
   624
lemma continuous_transform_within:
immler@69613
   625
  fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
immler@69613
   626
  assumes "continuous (at x within s) f"
immler@69613
   627
    and "0 < d"
immler@69613
   628
    and "x \<in> s"
immler@69613
   629
    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
immler@69613
   630
  shows "continuous (at x within s) g"
immler@69613
   631
  using assms
immler@69613
   632
  unfolding continuous_within
immler@69613
   633
  by (force intro: Lim_transform_within)
immler@69613
   634
immler@69613
   635
immler@69544
   636
subsection \<open>Closure and Limit Characterization\<close>
immler@69544
   637
immler@69544
   638
lemma closure_approachable:
immler@69544
   639
  fixes S :: "'a::metric_space set"
immler@69544
   640
  shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
immler@69544
   641
  apply (auto simp: closure_def islimpt_approachable)
immler@69544
   642
  apply (metis dist_self)
immler@69544
   643
  done
immler@69544
   644
immler@69544
   645
lemma closure_approachable_le:
immler@69544
   646
  fixes S :: "'a::metric_space set"
immler@69544
   647
  shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x \<le> e)"
immler@69544
   648
  unfolding closure_approachable
immler@69544
   649
  using dense by force
immler@69544
   650
immler@69544
   651
lemma closure_approachableD:
immler@69544
   652
  assumes "x \<in> closure S" "e>0"
immler@69544
   653
  shows "\<exists>y\<in>S. dist x y < e"
immler@69544
   654
  using assms unfolding closure_approachable by (auto simp: dist_commute)
immler@69544
   655
immler@69544
   656
lemma closed_approachable:
immler@69544
   657
  fixes S :: "'a::metric_space set"
immler@69544
   658
  shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
immler@69544
   659
  by (metis closure_closed closure_approachable)
immler@69544
   660
immler@69544
   661
lemma closure_contains_Inf:
immler@69544
   662
  fixes S :: "real set"
immler@69544
   663
  assumes "S \<noteq> {}" "bdd_below S"
immler@69544
   664
  shows "Inf S \<in> closure S"
immler@69544
   665
proof -
immler@69544
   666
  have *: "\<forall>x\<in>S. Inf S \<le> x"
immler@69544
   667
    using cInf_lower[of _ S] assms by metis
immler@69544
   668
  {
immler@69544
   669
    fix e :: real
immler@69544
   670
    assume "e > 0"
immler@69544
   671
    then have "Inf S < Inf S + e" by simp
immler@69544
   672
    with assms obtain x where "x \<in> S" "x < Inf S + e"
immler@69544
   673
      by (subst (asm) cInf_less_iff) auto
immler@69544
   674
    with * have "\<exists>x\<in>S. dist x (Inf S) < e"
immler@69544
   675
      by (intro bexI[of _ x]) (auto simp: dist_real_def)
immler@69544
   676
  }
immler@69544
   677
  then show ?thesis unfolding closure_approachable by auto
immler@69544
   678
qed
immler@69544
   679
immler@69544
   680
lemma not_trivial_limit_within_ball:
immler@69544
   681
  "\<not> trivial_limit (at x within S) \<longleftrightarrow> (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
immler@69544
   682
  (is "?lhs \<longleftrightarrow> ?rhs")
immler@69544
   683
proof
immler@69544
   684
  show ?rhs if ?lhs
immler@69544
   685
  proof -
immler@69544
   686
    {
immler@69544
   687
      fix e :: real
immler@69544
   688
      assume "e > 0"
immler@69544
   689
      then obtain y where "y \<in> S - {x}" and "dist y x < e"
immler@69544
   690
        using \<open>?lhs\<close> not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
immler@69544
   691
        by auto
immler@69544
   692
      then have "y \<in> S \<inter> ball x e - {x}"
immler@69544
   693
        unfolding ball_def by (simp add: dist_commute)
immler@69544
   694
      then have "S \<inter> ball x e - {x} \<noteq> {}" by blast
immler@69544
   695
    }
immler@69544
   696
    then show ?thesis by auto
immler@69544
   697
  qed
immler@69544
   698
  show ?lhs if ?rhs
immler@69544
   699
  proof -
immler@69544
   700
    {
immler@69544
   701
      fix e :: real
immler@69544
   702
      assume "e > 0"
immler@69544
   703
      then obtain y where "y \<in> S \<inter> ball x e - {x}"
immler@69544
   704
        using \<open>?rhs\<close> by blast
immler@69544
   705
      then have "y \<in> S - {x}" and "dist y x < e"
immler@69544
   706
        unfolding ball_def by (simp_all add: dist_commute)
immler@69544
   707
      then have "\<exists>y \<in> S - {x}. dist y x < e"
immler@69544
   708
        by auto
immler@69544
   709
    }
immler@69544
   710
    then show ?thesis
immler@69544
   711
      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
immler@69544
   712
      by auto
immler@69544
   713
  qed
immler@69544
   714
qed
immler@69544
   715
immler@69613
   716
immler@69544
   717
subsection \<open>Boundedness\<close>
immler@69544
   718
immler@69544
   719
  (* FIXME: This has to be unified with BSEQ!! *)
immler@69544
   720
definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool"
immler@69544
   721
  where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
immler@69544
   722
immler@69544
   723
lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
immler@69544
   724
  unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)
immler@69544
   725
immler@69544
   726
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
immler@69544
   727
  unfolding bounded_def
immler@69544
   728
  by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)
immler@69544
   729
immler@69544
   730
lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
immler@69544
   731
  unfolding bounded_any_center [where a=0]
immler@69544
   732
  by (simp add: dist_norm)
immler@69544
   733
immler@69544
   734
lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
immler@69544
   735
  by (simp add: bounded_iff bdd_above_def)
immler@69544
   736
immler@69544
   737
lemma bounded_norm_comp: "bounded ((\<lambda>x. norm (f x)) ` S) = bounded (f ` S)"
immler@69544
   738
  by (simp add: bounded_iff)
immler@69544
   739
immler@69544
   740
lemma boundedI:
immler@69544
   741
  assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
immler@69544
   742
  shows "bounded S"
immler@69544
   743
  using assms bounded_iff by blast
immler@69544
   744
immler@69544
   745
lemma bounded_empty [simp]: "bounded {}"
immler@69544
   746
  by (simp add: bounded_def)
immler@69544
   747
immler@69544
   748
lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> bounded S"
immler@69544
   749
  by (metis bounded_def subset_eq)
immler@69544
   750
immler@69544
   751
lemma bounded_interior[intro]: "bounded S \<Longrightarrow> bounded(interior S)"
immler@69544
   752
  by (metis bounded_subset interior_subset)
immler@69544
   753
immler@69544
   754
lemma bounded_closure[intro]:
immler@69544
   755
  assumes "bounded S"
immler@69544
   756
  shows "bounded (closure S)"
immler@69544
   757
proof -
immler@69544
   758
  from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a"
immler@69544
   759
    unfolding bounded_def by auto
immler@69544
   760
  {
immler@69544
   761
    fix y
immler@69544
   762
    assume "y \<in> closure S"
immler@69544
   763
    then obtain f where f: "\<forall>n. f n \<in> S"  "(f \<longlongrightarrow> y) sequentially"
immler@69544
   764
      unfolding closure_sequential by auto
immler@69544
   765
    have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
immler@69544
   766
    then have "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
immler@69544
   767
      by (simp add: f(1))
immler@69544
   768
    have "dist x y \<le> a"
immler@69544
   769
      apply (rule Lim_dist_ubound [of sequentially f])
immler@69544
   770
      apply (rule trivial_limit_sequentially)
immler@69544
   771
      apply (rule f(2))
immler@69544
   772
      apply fact
immler@69544
   773
      done
immler@69544
   774
  }
immler@69544
   775
  then show ?thesis
immler@69544
   776
    unfolding bounded_def by auto
immler@69544
   777
qed
immler@69544
   778
immler@69544
   779
lemma bounded_closure_image: "bounded (f ` closure S) \<Longrightarrow> bounded (f ` S)"
immler@69544
   780
  by (simp add: bounded_subset closure_subset image_mono)
immler@69544
   781
immler@69544
   782
lemma bounded_cball[simp,intro]: "bounded (cball x e)"
immler@69544
   783
  apply (simp add: bounded_def)
immler@69544
   784
  apply (rule_tac x=x in exI)
immler@69544
   785
  apply (rule_tac x=e in exI, auto)
immler@69544
   786
  done
immler@69544
   787
immler@69544
   788
lemma bounded_ball[simp,intro]: "bounded (ball x e)"
immler@69544
   789
  by (metis ball_subset_cball bounded_cball bounded_subset)
immler@69544
   790
immler@69544
   791
lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
immler@69544
   792
  by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)
immler@69544
   793
immler@69544
   794
lemma bounded_Union[intro]: "finite F \<Longrightarrow> \<forall>S\<in>F. bounded S \<Longrightarrow> bounded (\<Union>F)"
immler@69544
   795
  by (induct rule: finite_induct[of F]) auto
immler@69544
   796
immler@69544
   797
lemma bounded_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. bounded (B x) \<Longrightarrow> bounded (\<Union>x\<in>A. B x)"
immler@69544
   798
  by (induct set: finite) auto
immler@69544
   799
immler@69544
   800
lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"
immler@69544
   801
proof -
immler@69544
   802
  have "\<forall>y\<in>{x}. dist x y \<le> 0"
immler@69544
   803
    by simp
immler@69544
   804
  then have "bounded {x}"
immler@69544
   805
    unfolding bounded_def by fast
immler@69544
   806
  then show ?thesis
immler@69544
   807
    by (metis insert_is_Un bounded_Un)
immler@69544
   808
qed
immler@69544
   809
immler@69544
   810
lemma bounded_subset_ballI: "S \<subseteq> ball x r \<Longrightarrow> bounded S"
immler@69544
   811
  by (meson bounded_ball bounded_subset)
immler@69544
   812
immler@69544
   813
lemma bounded_subset_ballD:
immler@69544
   814
  assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
immler@69544
   815
proof -
immler@69544
   816
  obtain e::real and y where "S \<subseteq> cball y e"  "0 \<le> e"
immler@69544
   817
    using assms by (auto simp: bounded_subset_cball)
immler@69544
   818
  then show ?thesis
immler@69544
   819
    apply (rule_tac x="dist x y + e + 1" in exI)
immler@69544
   820
    apply (simp add: add.commute add_pos_nonneg)
immler@69544
   821
    apply (erule subset_trans)
immler@69544
   822
    apply (clarsimp simp add: cball_def)
immler@69544
   823
    by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
immler@69544
   824
qed
immler@69544
   825
immler@69544
   826
lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
immler@69544
   827
  by (induct set: finite) simp_all
immler@69544
   828
immler@69544
   829
lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
immler@69544
   830
  by (metis Int_lower1 Int_lower2 bounded_subset)
immler@69544
   831
immler@69544
   832
lemma bounded_diff[intro]: "bounded S \<Longrightarrow> bounded (S - T)"
immler@69544
   833
  by (metis Diff_subset bounded_subset)
immler@69544
   834
immler@69544
   835
lemma bounded_dist_comp:
immler@69544
   836
  assumes "bounded (f ` S)" "bounded (g ` S)"
immler@69544
   837
  shows "bounded ((\<lambda>x. dist (f x) (g x)) ` S)"
immler@69544
   838
proof -
immler@69544
   839
  from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x
immler@69544
   840
    by (auto simp: bounded_any_center[of _ undefined] dist_commute)
immler@69544
   841
  have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x
immler@69544
   842
    using *[OF that]
immler@69544
   843
    by (rule order_trans[OF dist_triangle add_mono])
immler@69544
   844
  then show ?thesis
immler@69544
   845
    by (auto intro!: boundedI)
immler@69544
   846
qed
immler@69544
   847
immler@69613
   848
lemma bounded_Times:
immler@69613
   849
  assumes "bounded s" "bounded t"
immler@69613
   850
  shows "bounded (s \<times> t)"
immler@69613
   851
proof -
immler@69613
   852
  obtain x y a b where "\<forall>z\<in>s. dist x z \<le> a" "\<forall>z\<in>t. dist y z \<le> b"
immler@69613
   853
    using assms [unfolded bounded_def] by auto
immler@69613
   854
  then have "\<forall>z\<in>s \<times> t. dist (x, y) z \<le> sqrt (a\<^sup>2 + b\<^sup>2)"
immler@69613
   855
    by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
immler@69613
   856
  then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
immler@69613
   857
qed
immler@69611
   858
immler@69611
   859
immler@69544
   860
subsection \<open>Compactness\<close>
immler@69544
   861
immler@69544
   862
lemma compact_imp_bounded:
immler@69544
   863
  assumes "compact U"
immler@69544
   864
  shows "bounded U"
immler@69544
   865
proof -
immler@69544
   866
  have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)"
immler@69544
   867
    using assms by auto
immler@69544
   868
  then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
immler@69544
   869
    by (metis compactE_image)
immler@69544
   870
  from \<open>finite D\<close> have "bounded (\<Union>x\<in>D. ball x 1)"
immler@69544
   871
    by (simp add: bounded_UN)
immler@69544
   872
  then show "bounded U" using \<open>U \<subseteq> (\<Union>x\<in>D. ball x 1)\<close>
immler@69544
   873
    by (rule bounded_subset)
immler@69544
   874
qed
immler@69544
   875
immler@69544
   876
lemma closure_Int_ball_not_empty:
immler@69544
   877
  assumes "S \<subseteq> closure T" "x \<in> S" "r > 0"
immler@69544
   878
  shows "T \<inter> ball x r \<noteq> {}"
immler@69544
   879
  using assms centre_in_ball closure_iff_nhds_not_empty by blast
immler@69544
   880
immler@69613
   881
lemma compact_sup_maxdistance:
immler@69613
   882
  fixes s :: "'a::metric_space set"
immler@69613
   883
  assumes "compact s"
immler@69613
   884
    and "s \<noteq> {}"
immler@69613
   885
  shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
immler@69613
   886
proof -
immler@69613
   887
  have "compact (s \<times> s)"
immler@69613
   888
    using \<open>compact s\<close> by (intro compact_Times)
immler@69613
   889
  moreover have "s \<times> s \<noteq> {}"
immler@69613
   890
    using \<open>s \<noteq> {}\<close> by auto
immler@69613
   891
  moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"
immler@69613
   892
    by (intro continuous_at_imp_continuous_on ballI continuous_intros)
immler@69613
   893
  ultimately show ?thesis
immler@69613
   894
    using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
immler@69613
   895
qed
immler@69613
   896
immler@69613
   897
immler@69544
   898
subsubsection\<open>Totally bounded\<close>
immler@69544
   899
immler@69544
   900
lemma cauchy_def: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N \<longrightarrow> dist (s m) (s n) < e)"
immler@69544
   901
  unfolding Cauchy_def by metis
immler@69544
   902
immler@69544
   903
proposition seq_compact_imp_totally_bounded:
immler@69544
   904
  assumes "seq_compact s"
immler@69544
   905
  shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>k. ball x e)"
immler@69544
   906
proof -
immler@69544
   907
  { fix e::real assume "e > 0" assume *: "\<And>k. finite k \<Longrightarrow> k \<subseteq> s \<Longrightarrow> \<not> s \<subseteq> (\<Union>x\<in>k. ball x e)"
immler@69544
   908
    let ?Q = "\<lambda>x n r. r \<in> s \<and> (\<forall>m < (n::nat). \<not> (dist (x m) r < e))"
immler@69544
   909
    have "\<exists>x. \<forall>n::nat. ?Q x n (x n)"
immler@69544
   910
    proof (rule dependent_wellorder_choice)
immler@69544
   911
      fix n x assume "\<And>y. y < n \<Longrightarrow> ?Q x y (x y)"
immler@69544
   912
      then have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
immler@69544
   913
        using *[of "x ` {0 ..< n}"] by (auto simp: subset_eq)
immler@69544
   914
      then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
immler@69544
   915
        unfolding subset_eq by auto
immler@69544
   916
      show "\<exists>r. ?Q x n r"
immler@69544
   917
        using z by auto
immler@69544
   918
    qed simp
immler@69544
   919
    then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
immler@69544
   920
      by blast
immler@69544
   921
    then obtain l r where "l \<in> s" and r:"strict_mono  r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69544
   922
      using assms by (metis seq_compact_def)
immler@69544
   923
    from this(3) have "Cauchy (x \<circ> r)"
immler@69544
   924
      using LIMSEQ_imp_Cauchy by auto
immler@69544
   925
    then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
immler@69544
   926
      unfolding cauchy_def using \<open>e > 0\<close> by blast
immler@69544
   927
    then have False
immler@69544
   928
      using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
immler@69544
   929
  then show ?thesis
immler@69544
   930
    by metis
immler@69544
   931
qed
immler@69544
   932
immler@69544
   933
subsubsection\<open>Heine-Borel theorem\<close>
immler@69544
   934
immler@69544
   935
proposition seq_compact_imp_Heine_Borel:
immler@69544
   936
  fixes s :: "'a :: metric_space set"
immler@69544
   937
  assumes "seq_compact s"
immler@69544
   938
  shows "compact s"
immler@69544
   939
proof -
immler@69544
   940
  from seq_compact_imp_totally_bounded[OF \<open>seq_compact s\<close>]
immler@69544
   941
  obtain f where f: "\<forall>e>0. finite (f e) \<and> f e \<subseteq> s \<and> s \<subseteq> (\<Union>x\<in>f e. ball x e)"
immler@69544
   942
    unfolding choice_iff' ..
immler@69544
   943
  define K where "K = (\<lambda>(x, r). ball x r) ` ((\<Union>e \<in> \<rat> \<inter> {0 <..}. f e) \<times> \<rat>)"
immler@69544
   944
  have "countably_compact s"
immler@69544
   945
    using \<open>seq_compact s\<close> by (rule seq_compact_imp_countably_compact)
immler@69544
   946
  then show "compact s"
immler@69544
   947
  proof (rule countably_compact_imp_compact)
immler@69544
   948
    show "countable K"
immler@69544
   949
      unfolding K_def using f
immler@69544
   950
      by (auto intro: countable_finite countable_subset countable_rat
immler@69544
   951
               intro!: countable_image countable_SIGMA countable_UN)
immler@69544
   952
    show "\<forall>b\<in>K. open b" by (auto simp: K_def)
immler@69544
   953
  next
immler@69544
   954
    fix T x
immler@69544
   955
    assume T: "open T" "x \<in> T" and x: "x \<in> s"
immler@69544
   956
    from openE[OF T] obtain e where "0 < e" "ball x e \<subseteq> T"
immler@69544
   957
      by auto
immler@69544
   958
    then have "0 < e / 2" "ball x (e / 2) \<subseteq> T"
immler@69544
   959
      by auto
immler@69544
   960
    from Rats_dense_in_real[OF \<open>0 < e / 2\<close>] obtain r where "r \<in> \<rat>" "0 < r" "r < e / 2"
immler@69544
   961
      by auto
immler@69544
   962
    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"
immler@69544
   963
      by auto
immler@69544
   964
    from \<open>r \<in> \<rat>\<close> \<open>0 < r\<close> \<open>k \<in> f r\<close> have "ball k r \<in> K"
immler@69544
   965
      by (auto simp: K_def)
immler@69544
   966
    then show "\<exists>b\<in>K. x \<in> b \<and> b \<inter> s \<subseteq> T"
immler@69544
   967
    proof (rule bexI[rotated], safe)
immler@69544
   968
      fix y
immler@69544
   969
      assume "y \<in> ball k r"
immler@69544
   970
      with \<open>r < e / 2\<close> \<open>x \<in> ball k r\<close> have "dist x y < e"
immler@69544
   971
        by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)
immler@69544
   972
      with \<open>ball x e \<subseteq> T\<close> show "y \<in> T"
immler@69544
   973
        by auto
immler@69544
   974
    next
immler@69544
   975
      show "x \<in> ball k r" by fact
immler@69544
   976
    qed
immler@69544
   977
  qed
immler@69544
   978
qed
immler@69544
   979
immler@69544
   980
proposition compact_eq_seq_compact_metric:
immler@69544
   981
  "compact (s :: 'a::metric_space set) \<longleftrightarrow> seq_compact s"
immler@69544
   982
  using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast
immler@69544
   983
immler@69544
   984
proposition compact_def: \<comment> \<open>this is the definition of compactness in HOL Light\<close>
immler@69544
   985
  "compact (S :: 'a::metric_space set) \<longleftrightarrow>
immler@69544
   986
   (\<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))"
immler@69544
   987
  unfolding compact_eq_seq_compact_metric seq_compact_def by auto
immler@69544
   988
immler@69544
   989
subsubsection \<open>Complete the chain of compactness variants\<close>
immler@69544
   990
immler@69544
   991
proposition compact_eq_Bolzano_Weierstrass:
immler@69544
   992
  fixes s :: "'a::metric_space set"
immler@69544
   993
  shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))"
immler@69544
   994
  (is "?lhs = ?rhs")
immler@69544
   995
proof
immler@69544
   996
  assume ?lhs
immler@69544
   997
  then show ?rhs
immler@69544
   998
    using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto
immler@69544
   999
next
immler@69544
  1000
  assume ?rhs
immler@69544
  1001
  then show ?lhs
immler@69544
  1002
    unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact)
immler@69544
  1003
qed
immler@69544
  1004
immler@69544
  1005
proposition Bolzano_Weierstrass_imp_bounded:
immler@69544
  1006
  "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> bounded s"
immler@69544
  1007
  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass .
immler@69544
  1008
immler@69544
  1009
immler@69613
  1010
subsection \<open>Banach fixed point theorem\<close>
immler@69613
  1011
  
immler@69613
  1012
theorem banach_fix:\<comment> \<open>TODO: rename to \<open>Banach_fix\<close>\<close>
immler@69613
  1013
  assumes s: "complete s" "s \<noteq> {}"
immler@69613
  1014
    and c: "0 \<le> c" "c < 1"
immler@69613
  1015
    and f: "f ` s \<subseteq> s"
immler@69613
  1016
    and lipschitz: "\<forall>x\<in>s. \<forall>y\<in>s. dist (f x) (f y) \<le> c * dist x y"
immler@69613
  1017
  shows "\<exists>!x\<in>s. f x = x"
immler@69613
  1018
proof -
immler@69613
  1019
  from c have "1 - c > 0" by simp
immler@69613
  1020
immler@69613
  1021
  from s(2) obtain z0 where z0: "z0 \<in> s" by blast
immler@69613
  1022
  define z where "z n = (f ^^ n) z0" for n
immler@69613
  1023
  with f z0 have z_in_s: "z n \<in> s" for n :: nat
immler@69613
  1024
    by (induct n) auto
immler@69613
  1025
  define d where "d = dist (z 0) (z 1)"
immler@69613
  1026
immler@69613
  1027
  have fzn: "f (z n) = z (Suc n)" for n
immler@69613
  1028
    by (simp add: z_def)
immler@69613
  1029
  have cf_z: "dist (z n) (z (Suc n)) \<le> (c ^ n) * d" for n :: nat
immler@69613
  1030
  proof (induct n)
immler@69613
  1031
    case 0
immler@69613
  1032
    then show ?case
immler@69613
  1033
      by (simp add: d_def)
immler@69613
  1034
  next
immler@69613
  1035
    case (Suc m)
immler@69613
  1036
    with \<open>0 \<le> c\<close> have "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
immler@69613
  1037
      using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp
immler@69613
  1038
    then show ?case
immler@69613
  1039
      using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
immler@69613
  1040
      by (simp add: fzn mult_le_cancel_left)
immler@69613
  1041
  qed
immler@69613
  1042
immler@69613
  1043
  have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \<le> (c ^ m) * d * (1 - c ^ n)" for n m :: nat
immler@69613
  1044
  proof (induct n)
immler@69613
  1045
    case 0
immler@69613
  1046
    show ?case by simp
immler@69613
  1047
  next
immler@69613
  1048
    case (Suc k)
immler@69613
  1049
    from c have "(1 - c) * dist (z m) (z (m + Suc k)) \<le>
immler@69613
  1050
        (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"
immler@69613
  1051
      by (simp add: dist_triangle)
immler@69613
  1052
    also from c cf_z[of "m + k"] have "\<dots> \<le> (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"
immler@69613
  1053
      by simp
immler@69613
  1054
    also from Suc have "\<dots> \<le> c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"
immler@69613
  1055
      by (simp add: field_simps)
immler@69613
  1056
    also have "\<dots> = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"
immler@69613
  1057
      by (simp add: power_add field_simps)
immler@69613
  1058
    also from c have "\<dots> \<le> (c ^ m) * d * (1 - c ^ Suc k)"
immler@69613
  1059
      by (simp add: field_simps)
immler@69613
  1060
    finally show ?case by simp
immler@69613
  1061
  qed
immler@69613
  1062
immler@69613
  1063
  have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e" if "e > 0" for e
immler@69613
  1064
  proof (cases "d = 0")
immler@69613
  1065
    case True
immler@69613
  1066
    from \<open>1 - c > 0\<close> have "(1 - c) * x \<le> 0 \<longleftrightarrow> x \<le> 0" for x
immler@69613
  1067
      by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1)
immler@69613
  1068
    with c cf_z2[of 0] True have "z n = z0" for n
immler@69613
  1069
      by (simp add: z_def)
immler@69613
  1070
    with \<open>e > 0\<close> show ?thesis by simp
immler@69613
  1071
  next
immler@69613
  1072
    case False
immler@69613
  1073
    with zero_le_dist[of "z 0" "z 1"] have "d > 0"
immler@69613
  1074
      by (metis d_def less_le)
immler@69613
  1075
    with \<open>1 - c > 0\<close> \<open>e > 0\<close> have "0 < e * (1 - c) / d"
immler@69613
  1076
      by simp
immler@69613
  1077
    with c obtain N where N: "c ^ N < e * (1 - c) / d"
immler@69613
  1078
      using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto
immler@69613
  1079
    have *: "dist (z m) (z n) < e" if "m > n" and as: "m \<ge> N" "n \<ge> N" for m n :: nat
immler@69613
  1080
    proof -
immler@69613
  1081
      from c \<open>n \<ge> N\<close> have *: "c ^ n \<le> c ^ N"
immler@69613
  1082
        using power_decreasing[OF \<open>n\<ge>N\<close>, of c] by simp
immler@69613
  1083
      from c \<open>m > n\<close> have "1 - c ^ (m - n) > 0"
immler@69613
  1084
        using power_strict_mono[of c 1 "m - n"] by simp
immler@69613
  1085
      with \<open>d > 0\<close> \<open>0 < 1 - c\<close> have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
immler@69613
  1086
        by simp
immler@69613
  1087
      from cf_z2[of n "m - n"] \<open>m > n\<close>
immler@69613
  1088
      have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
immler@69613
  1089
        by (simp add: pos_le_divide_eq[OF \<open>1 - c > 0\<close>] mult.commute dist_commute)
immler@69613
  1090
      also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
immler@69613
  1091
        using mult_right_mono[OF * order_less_imp_le[OF **]]
immler@69613
  1092
        by (simp add: mult.assoc)
immler@69613
  1093
      also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
immler@69613
  1094
        using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)
immler@69613
  1095
      also from c \<open>d > 0\<close> \<open>1 - c > 0\<close> have "\<dots> = e * (1 - c ^ (m - n))"
immler@69613
  1096
        by simp
immler@69613
  1097
      also from c \<open>1 - c ^ (m - n) > 0\<close> \<open>e > 0\<close> have "\<dots> \<le> e"
immler@69613
  1098
        using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
immler@69613
  1099
      finally show ?thesis by simp
immler@69613
  1100
    qed
immler@69613
  1101
    have "dist (z n) (z m) < e" if "N \<le> m" "N \<le> n" for m n :: nat
immler@69613
  1102
    proof (cases "n = m")
immler@69613
  1103
      case True
immler@69613
  1104
      with \<open>e > 0\<close> show ?thesis by simp
immler@69613
  1105
    next
immler@69613
  1106
      case False
immler@69613
  1107
      with *[of n m] *[of m n] and that show ?thesis
immler@69613
  1108
        by (auto simp: dist_commute nat_neq_iff)
immler@69613
  1109
    qed
immler@69613
  1110
    then show ?thesis by auto
immler@69613
  1111
  qed
immler@69613
  1112
  then have "Cauchy z"
immler@69613
  1113
    by (simp add: cauchy_def)
immler@69613
  1114
  then obtain x where "x\<in>s" and x:"(z \<longlongrightarrow> x) sequentially"
immler@69613
  1115
    using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
immler@69613
  1116
immler@69613
  1117
  define e where "e = dist (f x) x"
immler@69613
  1118
  have "e = 0"
immler@69613
  1119
  proof (rule ccontr)
immler@69613
  1120
    assume "e \<noteq> 0"
immler@69613
  1121
    then have "e > 0"
immler@69613
  1122
      unfolding e_def using zero_le_dist[of "f x" x]
immler@69613
  1123
      by (metis dist_eq_0_iff dist_nz e_def)
immler@69613
  1124
    then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
immler@69613
  1125
      using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
immler@69613
  1126
    then have N':"dist (z N) x < e / 2" by auto
immler@69613
  1127
    have *: "c * dist (z N) x \<le> dist (z N) x"
immler@69613
  1128
      unfolding mult_le_cancel_right2
immler@69613
  1129
      using zero_le_dist[of "z N" x] and c
immler@69613
  1130
      by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
immler@69613
  1131
    have "dist (f (z N)) (f x) \<le> c * dist (z N) x"
immler@69613
  1132
      using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
immler@69613
  1133
      using z_in_s[of N] \<open>x\<in>s\<close>
immler@69613
  1134
      using c
immler@69613
  1135
      by auto
immler@69613
  1136
    also have "\<dots> < e / 2"
immler@69613
  1137
      using N' and c using * by auto
immler@69613
  1138
    finally show False
immler@69613
  1139
      unfolding fzn
immler@69613
  1140
      using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]
immler@69613
  1141
      unfolding e_def
immler@69613
  1142
      by auto
immler@69613
  1143
  qed
immler@69613
  1144
  then have "f x = x" by (auto simp: e_def)
immler@69613
  1145
  moreover have "y = x" if "f y = y" "y \<in> s" for y
immler@69613
  1146
  proof -
immler@69613
  1147
    from \<open>x \<in> s\<close> \<open>f x = x\<close> that have "dist x y \<le> c * dist x y"
immler@69613
  1148
      using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp
immler@69613
  1149
    with c and zero_le_dist[of x y] have "dist x y = 0"
immler@69613
  1150
      by (simp add: mult_le_cancel_right1)
immler@69613
  1151
    then show ?thesis by simp
immler@69613
  1152
  qed
immler@69613
  1153
  ultimately show ?thesis
immler@69613
  1154
    using \<open>x\<in>s\<close> by blast
immler@69613
  1155
qed
immler@69613
  1156
immler@69613
  1157
immler@69613
  1158
subsection \<open>Edelstein fixed point theorem\<close>
immler@69613
  1159
immler@69613
  1160
theorem edelstein_fix:\<comment> \<open>TODO: rename to \<open>Edelstein_fix\<close>\<close>
immler@69613
  1161
  fixes s :: "'a::metric_space set"
immler@69613
  1162
  assumes s: "compact s" "s \<noteq> {}"
immler@69613
  1163
    and gs: "(g ` s) \<subseteq> s"
immler@69613
  1164
    and dist: "\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
immler@69613
  1165
  shows "\<exists>!x\<in>s. g x = x"
immler@69613
  1166
proof -
immler@69613
  1167
  let ?D = "(\<lambda>x. (x, x)) ` s"
immler@69613
  1168
  have D: "compact ?D" "?D \<noteq> {}"
immler@69613
  1169
    by (rule compact_continuous_image)
immler@69613
  1170
       (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)
immler@69613
  1171
immler@69613
  1172
  have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
immler@69613
  1173
    using dist by fastforce
immler@69613
  1174
  then have "continuous_on s g"
immler@69613
  1175
    by (auto simp: continuous_on_iff)
immler@69613
  1176
  then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
immler@69613
  1177
    unfolding continuous_on_eq_continuous_within
immler@69613
  1178
    by (intro continuous_dist ballI continuous_within_compose)
immler@69613
  1179
       (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)
immler@69613
  1180
immler@69613
  1181
  obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
immler@69613
  1182
    using continuous_attains_inf[OF D cont] by auto
immler@69613
  1183
immler@69613
  1184
  have "g a = a"
immler@69613
  1185
  proof (rule ccontr)
immler@69613
  1186
    assume "g a \<noteq> a"
immler@69613
  1187
    with \<open>a \<in> s\<close> gs have "dist (g (g a)) (g a) < dist (g a) a"
immler@69613
  1188
      by (intro dist[rule_format]) auto
immler@69613
  1189
    moreover have "dist (g a) a \<le> dist (g (g a)) (g a)"
immler@69613
  1190
      using \<open>a \<in> s\<close> gs by (intro le) auto
immler@69613
  1191
    ultimately show False by auto
immler@69613
  1192
  qed
immler@69613
  1193
  moreover have "\<And>x. x \<in> s \<Longrightarrow> g x = x \<Longrightarrow> x = a"
immler@69613
  1194
    using dist[THEN bspec[where x=a]] \<open>g a = a\<close> and \<open>a\<in>s\<close> by auto
immler@69613
  1195
  ultimately show "\<exists>!x\<in>s. g x = x"
immler@69613
  1196
    using \<open>a \<in> s\<close> by blast
immler@69613
  1197
qed
immler@69613
  1198
immler@69613
  1199
subsection \<open>The diameter of a set\<close>
immler@69613
  1200
immler@69613
  1201
definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
immler@69613
  1202
  "diameter S = (if S = {} then 0 else SUP (x,y)\<in>S\<times>S. dist x y)"
immler@69613
  1203
immler@69613
  1204
lemma diameter_empty [simp]: "diameter{} = 0"
immler@69613
  1205
  by (auto simp: diameter_def)
immler@69613
  1206
immler@69613
  1207
lemma diameter_singleton [simp]: "diameter{x} = 0"
immler@69613
  1208
  by (auto simp: diameter_def)
immler@69613
  1209
immler@69613
  1210
lemma diameter_le:
immler@69613
  1211
  assumes "S \<noteq> {} \<or> 0 \<le> d"
immler@69613
  1212
      and no: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> norm(x - y) \<le> d"
immler@69613
  1213
    shows "diameter S \<le> d"
immler@69613
  1214
using assms
immler@69613
  1215
  by (auto simp: dist_norm diameter_def intro: cSUP_least)
immler@69613
  1216
immler@69613
  1217
lemma diameter_bounded_bound:
immler@69613
  1218
  fixes s :: "'a :: metric_space set"
immler@69613
  1219
  assumes s: "bounded s" "x \<in> s" "y \<in> s"
immler@69613
  1220
  shows "dist x y \<le> diameter s"
immler@69613
  1221
proof -
immler@69613
  1222
  from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
immler@69613
  1223
    unfolding bounded_def by auto
immler@69613
  1224
  have "bdd_above (case_prod dist ` (s\<times>s))"
immler@69613
  1225
  proof (intro bdd_aboveI, safe)
immler@69613
  1226
    fix a b
immler@69613
  1227
    assume "a \<in> s" "b \<in> s"
immler@69613
  1228
    with z[of a] z[of b] dist_triangle[of a b z]
immler@69613
  1229
    show "dist a b \<le> 2 * d"
immler@69613
  1230
      by (simp add: dist_commute)
immler@69613
  1231
  qed
immler@69613
  1232
  moreover have "(x,y) \<in> s\<times>s" using s by auto
immler@69613
  1233
  ultimately have "dist x y \<le> (SUP (x,y)\<in>s\<times>s. dist x y)"
immler@69613
  1234
    by (rule cSUP_upper2) simp
immler@69613
  1235
  with \<open>x \<in> s\<close> show ?thesis
immler@69613
  1236
    by (auto simp: diameter_def)
immler@69613
  1237
qed
immler@69613
  1238
immler@69613
  1239
lemma diameter_lower_bounded:
immler@69613
  1240
  fixes s :: "'a :: metric_space set"
immler@69613
  1241
  assumes s: "bounded s"
immler@69613
  1242
    and d: "0 < d" "d < diameter s"
immler@69613
  1243
  shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
immler@69613
  1244
proof (rule ccontr)
immler@69613
  1245
  assume contr: "\<not> ?thesis"
immler@69613
  1246
  moreover have "s \<noteq> {}"
immler@69613
  1247
    using d by (auto simp: diameter_def)
immler@69613
  1248
  ultimately have "diameter s \<le> d"
immler@69613
  1249
    by (auto simp: not_less diameter_def intro!: cSUP_least)
immler@69613
  1250
  with \<open>d < diameter s\<close> show False by auto
immler@69613
  1251
qed
immler@69613
  1252
immler@69613
  1253
lemma diameter_bounded:
immler@69613
  1254
  assumes "bounded s"
immler@69613
  1255
  shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
immler@69613
  1256
    and "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
immler@69613
  1257
  using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
immler@69613
  1258
  by auto
immler@69613
  1259
immler@69613
  1260
lemma bounded_two_points:
immler@69613
  1261
  "bounded S \<longleftrightarrow> (\<exists>e. \<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> e)"
immler@69613
  1262
  apply (rule iffI)
immler@69613
  1263
  subgoal using diameter_bounded(1) by auto
immler@69613
  1264
  subgoal using bounded_any_center[of S] by meson
immler@69613
  1265
  done
immler@69613
  1266
immler@69613
  1267
lemma diameter_compact_attained:
immler@69613
  1268
  assumes "compact s"
immler@69613
  1269
    and "s \<noteq> {}"
immler@69613
  1270
  shows "\<exists>x\<in>s. \<exists>y\<in>s. dist x y = diameter s"
immler@69613
  1271
proof -
immler@69613
  1272
  have b: "bounded s" using assms(1)
immler@69613
  1273
    by (rule compact_imp_bounded)
immler@69613
  1274
  then obtain x y where xys: "x\<in>s" "y\<in>s"
immler@69613
  1275
    and xy: "\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
immler@69613
  1276
    using compact_sup_maxdistance[OF assms] by auto
immler@69613
  1277
  then have "diameter s \<le> dist x y"
immler@69613
  1278
    unfolding diameter_def
immler@69613
  1279
    apply clarsimp
immler@69613
  1280
    apply (rule cSUP_least, fast+)
immler@69613
  1281
    done
immler@69613
  1282
  then show ?thesis
immler@69613
  1283
    by (metis b diameter_bounded_bound order_antisym xys)
immler@69613
  1284
qed
immler@69613
  1285
immler@69613
  1286
lemma diameter_ge_0:
immler@69613
  1287
  assumes "bounded S"  shows "0 \<le> diameter S"
immler@69613
  1288
  by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)
immler@69613
  1289
immler@69613
  1290
lemma diameter_subset:
immler@69613
  1291
  assumes "S \<subseteq> T" "bounded T"
immler@69613
  1292
  shows "diameter S \<le> diameter T"
immler@69613
  1293
proof (cases "S = {} \<or> T = {}")
immler@69613
  1294
  case True
immler@69613
  1295
  with assms show ?thesis
immler@69613
  1296
    by (force simp: diameter_ge_0)
immler@69613
  1297
next
immler@69613
  1298
  case False
immler@69613
  1299
  then have "bdd_above ((\<lambda>x. case x of (x, xa) \<Rightarrow> dist x xa) ` (T \<times> T))"
immler@69613
  1300
    using \<open>bounded T\<close> diameter_bounded_bound by (force simp: bdd_above_def)
immler@69613
  1301
  with False \<open>S \<subseteq> T\<close> show ?thesis
immler@69613
  1302
    apply (simp add: diameter_def)
immler@69613
  1303
    apply (rule cSUP_subset_mono, auto)
immler@69613
  1304
    done
immler@69613
  1305
qed
immler@69613
  1306
immler@69613
  1307
lemma diameter_closure:
immler@69613
  1308
  assumes "bounded S"
immler@69613
  1309
  shows "diameter(closure S) = diameter S"
immler@69613
  1310
proof (rule order_antisym)
immler@69613
  1311
  have "False" if "diameter S < diameter (closure S)"
immler@69613
  1312
  proof -
immler@69613
  1313
    define d where "d = diameter(closure S) - diameter(S)"
immler@69613
  1314
    have "d > 0"
immler@69613
  1315
      using that by (simp add: d_def)
immler@69613
  1316
    then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"
immler@69613
  1317
      by simp
immler@69613
  1318
    have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"
immler@69613
  1319
      by (simp add: d_def divide_simps)
immler@69613
  1320
     have bocl: "bounded (closure S)"
immler@69613
  1321
      using assms by blast
immler@69613
  1322
    moreover have "0 \<le> diameter S"
immler@69613
  1323
      using assms diameter_ge_0 by blast
immler@69613
  1324
    ultimately obtain x y where "x \<in> closure S" "y \<in> closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"
immler@69613
  1325
      using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \<open>d > 0\<close> d_def by auto
immler@69613
  1326
    then obtain x' y' where x'y': "x' \<in> S" "dist x' x < d/4" "y' \<in> S" "dist y' y < d/4"
immler@69613
  1327
      using closure_approachable
immler@69613
  1328
      by (metis \<open>0 < d\<close> zero_less_divide_iff zero_less_numeral)
immler@69613
  1329
    then have "dist x' y' \<le> diameter S"
immler@69613
  1330
      using assms diameter_bounded_bound by blast
immler@69613
  1331
    with x'y' have "dist x y \<le> d / 4 + diameter S + d / 4"
immler@69613
  1332
      by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)
immler@69613
  1333
    then show ?thesis
immler@69613
  1334
      using xy d_def by linarith
immler@69613
  1335
  qed
immler@69613
  1336
  then show "diameter (closure S) \<le> diameter S"
immler@69613
  1337
    by fastforce
immler@69613
  1338
  next
immler@69613
  1339
    show "diameter S \<le> diameter (closure S)"
immler@69613
  1340
      by (simp add: assms bounded_closure closure_subset diameter_subset)
immler@69613
  1341
qed
immler@69613
  1342
immler@69613
  1343
proposition Lebesgue_number_lemma:
immler@69613
  1344
  assumes "compact S" "\<C> \<noteq> {}" "S \<subseteq> \<Union>\<C>" and ope: "\<And>B. B \<in> \<C> \<Longrightarrow> open B"
immler@69613
  1345
  obtains \<delta> where "0 < \<delta>" "\<And>T. \<lbrakk>T \<subseteq> S; diameter T < \<delta>\<rbrakk> \<Longrightarrow> \<exists>B \<in> \<C>. T \<subseteq> B"
immler@69613
  1346
proof (cases "S = {}")
immler@69613
  1347
  case True
immler@69613
  1348
  then show ?thesis
immler@69613
  1349
    by (metis \<open>\<C> \<noteq> {}\<close> zero_less_one empty_subsetI equals0I subset_trans that)
immler@69613
  1350
next
immler@69613
  1351
  case False
immler@69613
  1352
  { fix x assume "x \<in> S"
immler@69613
  1353
    then obtain C where C: "x \<in> C" "C \<in> \<C>"
immler@69613
  1354
      using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
immler@69613
  1355
    then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"
immler@69613
  1356
      by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)
immler@69613
  1357
    then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"
immler@69613
  1358
      using C by blast
immler@69613
  1359
  }
immler@69613
  1360
  then obtain r where r: "\<And>x. x \<in> S \<Longrightarrow> r x > 0 \<and> (\<exists>C \<in> \<C>. ball x (2*r x) \<subseteq> C)"
immler@69613
  1361
    by metis
immler@69613
  1362
  then have "S \<subseteq> (\<Union>x \<in> S. ball x (r x))"
immler@69613
  1363
    by auto
immler@69613
  1364
  then obtain \<T> where "finite \<T>" "S \<subseteq> \<Union>\<T>" and \<T>: "\<T> \<subseteq> (\<lambda>x. ball x (r x)) ` S"
immler@69613
  1365
    by (rule compactE [OF \<open>compact S\<close>]) auto
immler@69613
  1366
  then obtain S0 where "S0 \<subseteq> S" "finite S0" and S0: "\<T> = (\<lambda>x. ball x (r x)) ` S0"
immler@69613
  1367
    by (meson finite_subset_image)
immler@69613
  1368
  then have "S0 \<noteq> {}"
immler@69613
  1369
    using False \<open>S \<subseteq> \<Union>\<T>\<close> by auto
immler@69613
  1370
  define \<delta> where "\<delta> = Inf (r ` S0)"
immler@69613
  1371
  have "\<delta> > 0"
immler@69613
  1372
    using \<open>finite S0\<close> \<open>S0 \<subseteq> S\<close> \<open>S0 \<noteq> {}\<close> r by (auto simp: \<delta>_def finite_less_Inf_iff)
immler@69613
  1373
  show ?thesis
immler@69613
  1374
  proof
immler@69613
  1375
    show "0 < \<delta>"
immler@69613
  1376
      by (simp add: \<open>0 < \<delta>\<close>)
immler@69613
  1377
    show "\<exists>B \<in> \<C>. T \<subseteq> B" if "T \<subseteq> S" and dia: "diameter T < \<delta>" for T
immler@69613
  1378
    proof (cases "T = {}")
immler@69613
  1379
      case True
immler@69613
  1380
      then show ?thesis
immler@69613
  1381
        using \<open>\<C> \<noteq> {}\<close> by blast
immler@69613
  1382
    next
immler@69613
  1383
      case False
immler@69613
  1384
      then obtain y where "y \<in> T" by blast
immler@69613
  1385
      then have "y \<in> S"
immler@69613
  1386
        using \<open>T \<subseteq> S\<close> by auto
immler@69613
  1387
      then obtain x where "x \<in> S0" and x: "y \<in> ball x (r x)"
immler@69613
  1388
        using \<open>S \<subseteq> \<Union>\<T>\<close> S0 that by blast
immler@69613
  1389
      have "ball y \<delta> \<subseteq> ball y (r x)"
immler@69613
  1390
        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)
immler@69613
  1391
      also have "... \<subseteq> ball x (2*r x)"
immler@69613
  1392
        by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)
immler@69613
  1393
      finally obtain C where "C \<in> \<C>" "ball y \<delta> \<subseteq> C"
immler@69613
  1394
        by (meson r \<open>S0 \<subseteq> S\<close> \<open>x \<in> S0\<close> dual_order.trans subsetCE)
immler@69613
  1395
      have "bounded T"
immler@69613
  1396
        using \<open>compact S\<close> bounded_subset compact_imp_bounded \<open>T \<subseteq> S\<close> by blast
immler@69613
  1397
      then have "T \<subseteq> ball y \<delta>"
immler@69613
  1398
        using \<open>y \<in> T\<close> dia diameter_bounded_bound by fastforce
immler@69613
  1399
      then show ?thesis
immler@69613
  1400
        apply (rule_tac x=C in bexI)
immler@69613
  1401
        using \<open>ball y \<delta> \<subseteq> C\<close> \<open>C \<in> \<C>\<close> by auto
immler@69613
  1402
    qed
immler@69613
  1403
  qed
immler@69613
  1404
qed
immler@69613
  1405
immler@69613
  1406
immler@69544
  1407
subsection \<open>Metric spaces with the Heine-Borel property\<close>
immler@69544
  1408
immler@69544
  1409
text \<open>
immler@69544
  1410
  A metric space (or topological vector space) is said to have the
immler@69544
  1411
  Heine-Borel property if every closed and bounded subset is compact.
immler@69544
  1412
\<close>
immler@69544
  1413
immler@69544
  1414
class heine_borel = metric_space +
immler@69544
  1415
  assumes bounded_imp_convergent_subsequence:
immler@69544
  1416
    "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69544
  1417
immler@69544
  1418
proposition bounded_closed_imp_seq_compact:
immler@69544
  1419
  fixes s::"'a::heine_borel set"
immler@69544
  1420
  assumes "bounded s"
immler@69544
  1421
    and "closed s"
immler@69544
  1422
  shows "seq_compact s"
immler@69544
  1423
proof (unfold seq_compact_def, clarify)
immler@69544
  1424
  fix f :: "nat \<Rightarrow> 'a"
immler@69544
  1425
  assume f: "\<forall>n. f n \<in> s"
immler@69544
  1426
  with \<open>bounded s\<close> have "bounded (range f)"
immler@69544
  1427
    by (auto intro: bounded_subset)
immler@69544
  1428
  obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69544
  1429
    using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
immler@69544
  1430
  from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
immler@69544
  1431
    by simp
immler@69544
  1432
  have "l \<in> s" using \<open>closed s\<close> fr l
immler@69544
  1433
    by (rule closed_sequentially)
immler@69544
  1434
  show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69544
  1435
    using \<open>l \<in> s\<close> r l by blast
immler@69544
  1436
qed
immler@69544
  1437
immler@69544
  1438
lemma compact_eq_bounded_closed:
immler@69544
  1439
  fixes s :: "'a::heine_borel set"
immler@69544
  1440
  shows "compact s \<longleftrightarrow> bounded s \<and> closed s"
immler@69544
  1441
  (is "?lhs = ?rhs")
immler@69544
  1442
proof
immler@69544
  1443
  assume ?lhs
immler@69544
  1444
  then show ?rhs
immler@69544
  1445
    using compact_imp_closed compact_imp_bounded
immler@69544
  1446
    by blast
immler@69544
  1447
next
immler@69544
  1448
  assume ?rhs
immler@69544
  1449
  then show ?lhs
immler@69544
  1450
    using bounded_closed_imp_seq_compact[of s]
immler@69544
  1451
    unfolding compact_eq_seq_compact_metric
immler@69544
  1452
    by auto
immler@69544
  1453
qed
immler@69544
  1454
immler@69544
  1455
lemma compact_Inter:
immler@69544
  1456
  fixes \<F> :: "'a :: heine_borel set set"
immler@69544
  1457
  assumes com: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S" and "\<F> \<noteq> {}"
immler@69544
  1458
  shows "compact(\<Inter> \<F>)"
immler@69544
  1459
  using assms
immler@69544
  1460
  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)
immler@69544
  1461
immler@69544
  1462
lemma compact_closure [simp]:
immler@69544
  1463
  fixes S :: "'a::heine_borel set"
immler@69544
  1464
  shows "compact(closure S) \<longleftrightarrow> bounded S"
immler@69544
  1465
by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
immler@69544
  1466
immler@69544
  1467
instance%important real :: heine_borel
immler@69544
  1468
proof%unimportant
immler@69544
  1469
  fix f :: "nat \<Rightarrow> real"
immler@69544
  1470
  assume f: "bounded (range f)"
immler@69544
  1471
  obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
immler@69544
  1472
    unfolding comp_def by (metis seq_monosub)
immler@69544
  1473
  then have "Bseq (f \<circ> r)"
immler@69544
  1474
    unfolding Bseq_eq_bounded using f
immler@69544
  1475
    by (metis BseqI' bounded_iff comp_apply rangeI)
immler@69544
  1476
  with r show "\<exists>l r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
immler@69544
  1477
    using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
immler@69544
  1478
qed
immler@69544
  1479
immler@69544
  1480
lemma compact_lemma_general:
immler@69544
  1481
  fixes f :: "nat \<Rightarrow> 'a"
immler@69544
  1482
  fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl "proj" 60)
immler@69544
  1483
  fixes unproj:: "('b \<Rightarrow> 'c) \<Rightarrow> 'a"
immler@69544
  1484
  assumes finite_basis: "finite basis"
immler@69544
  1485
  assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
immler@69544
  1486
  assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
immler@69544
  1487
  assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"
immler@69544
  1488
  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r::nat\<Rightarrow>nat.
immler@69544
  1489
    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)"
immler@69544
  1490
proof safe
immler@69544
  1491
  fix d :: "'b set"
immler@69544
  1492
  assume d: "d \<subseteq> basis"
immler@69544
  1493
  with finite_basis have "finite d"
immler@69544
  1494
    by (blast intro: finite_subset)
immler@69544
  1495
  from this d show "\<exists>l::'a. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and>
immler@69544
  1496
    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
immler@69544
  1497
  proof (induct d)
immler@69544
  1498
    case empty
immler@69544
  1499
    then show ?case
immler@69544
  1500
      unfolding strict_mono_def by auto
immler@69544
  1501
  next
immler@69544
  1502
    case (insert k d)
immler@69544
  1503
    have k[intro]: "k \<in> basis"
immler@69544
  1504
      using insert by auto
immler@69544
  1505
    have s': "bounded ((\<lambda>x. x proj k) ` range f)"
immler@69544
  1506
      using k
immler@69544
  1507
      by (rule bounded_proj)
immler@69544
  1508
    obtain l1::"'a" and r1 where r1: "strict_mono r1"
immler@69544
  1509
      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
immler@69544
  1510
      using insert(3) using insert(4) by auto
immler@69544
  1511
    have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
immler@69544
  1512
      by simp
immler@69544
  1513
    have "bounded (range (\<lambda>i. f (r1 i) proj k))"
immler@69544
  1514
      by (metis (lifting) bounded_subset f' image_subsetI s')
immler@69544
  1515
    then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
immler@69544
  1516
      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
immler@69544
  1517
      by (auto simp: o_def)
immler@69544
  1518
    define r where "r = r1 \<circ> r2"
immler@69544
  1519
    have r:"strict_mono r"
immler@69544
  1520
      using r1 and r2 unfolding r_def o_def strict_mono_def by auto
immler@69544
  1521
    moreover
immler@69544
  1522
    define l where "l = unproj (\<lambda>i. if i = k then l2 else l1 proj i)"
immler@69544
  1523
    {
immler@69544
  1524
      fix e::real
immler@69544
  1525
      assume "e > 0"
immler@69544
  1526
      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"
immler@69544
  1527
        by blast
immler@69544
  1528
      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"
immler@69544
  1529
        by (rule tendstoD)
immler@69544
  1530
      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"
immler@69544
  1531
        by (rule eventually_subseq)
immler@69544
  1532
      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"
immler@69544
  1533
        using N1' N2
immler@69544
  1534
        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)
immler@69544
  1535
    }
immler@69544
  1536
    ultimately show ?case by auto
immler@69544
  1537
  qed
immler@69544
  1538
qed
immler@69544
  1539
immler@69544
  1540
lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
immler@69544
  1541
  unfolding bounded_def
immler@69544
  1542
  by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)
immler@69544
  1543
immler@69544
  1544
lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
immler@69544
  1545
  unfolding bounded_def
immler@69544
  1546
  by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
immler@69544
  1547
immler@69544
  1548
instance%important prod :: (heine_borel, heine_borel) heine_borel
immler@69544
  1549
proof%unimportant
immler@69544
  1550
  fix f :: "nat \<Rightarrow> 'a \<times> 'b"
immler@69544
  1551
  assume f: "bounded (range f)"
immler@69544
  1552
  then have "bounded (fst ` range f)"
immler@69544
  1553
    by (rule bounded_fst)
immler@69544
  1554
  then have s1: "bounded (range (fst \<circ> f))"
immler@69544
  1555
    by (simp add: image_comp)
immler@69544
  1556
  obtain l1 r1 where r1: "strict_mono r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
immler@69544
  1557
    using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
immler@69544
  1558
  from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
immler@69544
  1559
    by (auto simp: image_comp intro: bounded_snd bounded_subset)
immler@69544
  1560
  obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
immler@69544
  1561
    using bounded_imp_convergent_subsequence [OF s2]
immler@69544
  1562
    unfolding o_def by fast
immler@69544
  1563
  have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"
immler@69544
  1564
    using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
immler@69544
  1565
  have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially"
immler@69544
  1566
    using tendsto_Pair [OF l1' l2] unfolding o_def by simp
immler@69544
  1567
  have r: "strict_mono (r1 \<circ> r2)"
immler@69544
  1568
    using r1 r2 unfolding strict_mono_def by simp
immler@69544
  1569
  show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69544
  1570
    using l r by fast
immler@69544
  1571
qed
immler@69544
  1572
immler@69611
  1573
immler@69613
  1574
subsection \<open>Completeness\<close>
immler@69544
  1575
immler@69544
  1576
proposition (in metric_space) completeI:
immler@69544
  1577
  assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
immler@69544
  1578
  shows "complete s"
immler@69544
  1579
  using assms unfolding complete_def by fast
immler@69544
  1580
immler@69544
  1581
proposition (in metric_space) completeE:
immler@69544
  1582
  assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
immler@69544
  1583
  obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
immler@69544
  1584
  using assms unfolding complete_def by fast
immler@69544
  1585
immler@69544
  1586
(* TODO: generalize to uniform spaces *)
immler@69544
  1587
lemma compact_imp_complete:
immler@69544
  1588
  fixes s :: "'a::metric_space set"
immler@69544
  1589
  assumes "compact s"
immler@69544
  1590
  shows "complete s"
immler@69544
  1591
proof -
immler@69544
  1592
  {
immler@69544
  1593
    fix f
immler@69544
  1594
    assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
immler@69544
  1595
    from as(1) obtain l r where lr: "l\<in>s" "strict_mono r" "(f \<circ> r) \<longlonglongrightarrow> l"
immler@69544
  1596
      using assms unfolding compact_def by blast
immler@69544
  1597
immler@69544
  1598
    note lr' = seq_suble [OF lr(2)]
immler@69544
  1599
    {
immler@69544
  1600
      fix e :: real
immler@69544
  1601
      assume "e > 0"
immler@69544
  1602
      from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2"
immler@69544
  1603
        unfolding cauchy_def
immler@69544
  1604
        using \<open>e > 0\<close>
immler@69544
  1605
        apply (erule_tac x="e/2" in allE, auto)
immler@69544
  1606
        done
immler@69544
  1607
      from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]
immler@69544
  1608
      obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
immler@69544
  1609
        using \<open>e > 0\<close> by auto
immler@69544
  1610
      {
immler@69544
  1611
        fix n :: nat
immler@69544
  1612
        assume n: "n \<ge> max N M"
immler@69544
  1613
        have "dist ((f \<circ> r) n) l < e/2"
immler@69544
  1614
          using n M by auto
immler@69544
  1615
        moreover have "r n \<ge> N"
immler@69544
  1616
          using lr'[of n] n by auto
immler@69544
  1617
        then have "dist (f n) ((f \<circ> r) n) < e / 2"
immler@69544
  1618
          using N and n by auto
immler@69544
  1619
        ultimately have "dist (f n) l < e"
immler@69544
  1620
          using dist_triangle_half_r[of "f (r n)" "f n" e l]
immler@69544
  1621
          by (auto simp: dist_commute)
immler@69544
  1622
      }
immler@69544
  1623
      then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
immler@69544
  1624
    }
immler@69544
  1625
    then have "\<exists>l\<in>s. (f \<longlongrightarrow> l) sequentially" using \<open>l\<in>s\<close>
immler@69544
  1626
      unfolding lim_sequentially by auto
immler@69544
  1627
  }
immler@69544
  1628
  then show ?thesis unfolding complete_def by auto
immler@69544
  1629
qed
immler@69544
  1630
immler@69544
  1631
proposition compact_eq_totally_bounded:
immler@69544
  1632
  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>x\<in>k. ball x e))"
immler@69544
  1633
    (is "_ \<longleftrightarrow> ?rhs")
immler@69544
  1634
proof
immler@69544
  1635
  assume assms: "?rhs"
immler@69544
  1636
  then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
immler@69544
  1637
    by (auto simp: choice_iff')
immler@69544
  1638
immler@69544
  1639
  show "compact s"
immler@69544
  1640
  proof cases
immler@69544
  1641
    assume "s = {}"
immler@69544
  1642
    then show "compact s" by (simp add: compact_def)
immler@69544
  1643
  next
immler@69544
  1644
    assume "s \<noteq> {}"
immler@69544
  1645
    show ?thesis
immler@69544
  1646
      unfolding compact_def
immler@69544
  1647
    proof safe
immler@69544
  1648
      fix f :: "nat \<Rightarrow> 'a"
immler@69544
  1649
      assume f: "\<forall>n. f n \<in> s"
immler@69544
  1650
immler@69544
  1651
      define e where "e n = 1 / (2 * Suc n)" for n
immler@69544
  1652
      then have [simp]: "\<And>n. 0 < e n" by auto
immler@69544
  1653
      define B where "B n U = (SOME b. infinite {n. f n \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U))" for n U
immler@69544
  1654
      {
immler@69544
  1655
        fix n U
immler@69544
  1656
        assume "infinite {n. f n \<in> U}"
immler@69544
  1657
        then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
immler@69544
  1658
          using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
immler@69544
  1659
        then obtain a where
immler@69544
  1660
          "a \<in> k (e n)"
immler@69544
  1661
          "infinite {i \<in> {n. f n \<in> U}. f i \<in> ball a (e n)}" ..
immler@69544
  1662
        then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
immler@69544
  1663
          by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
immler@69544
  1664
        from someI_ex[OF this]
immler@69544
  1665
        have "infinite {i. f i \<in> B n U}" "\<exists>x. B n U \<subseteq> ball x (e n) \<inter> U"
immler@69544
  1666
          unfolding B_def by auto
immler@69544
  1667
      }
immler@69544
  1668
      note B = this
immler@69544
  1669
immler@69544
  1670
      define F where "F = rec_nat (B 0 UNIV) B"
immler@69544
  1671
      {
immler@69544
  1672
        fix n
immler@69544
  1673
        have "infinite {i. f i \<in> F n}"
immler@69544
  1674
          by (induct n) (auto simp: F_def B)
immler@69544
  1675
      }
immler@69544
  1676
      then have F: "\<And>n. \<exists>x. F (Suc n) \<subseteq> ball x (e n) \<inter> F n"
immler@69544
  1677
        using B by (simp add: F_def)
immler@69544
  1678
      then have F_dec: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
immler@69544
  1679
        using decseq_SucI[of F] by (auto simp: decseq_def)
immler@69544
  1680
immler@69544
  1681
      obtain sel where sel: "\<And>k i. i < sel k i" "\<And>k i. f (sel k i) \<in> F k"
immler@69544
  1682
      proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)
immler@69544
  1683
        fix k i
immler@69544
  1684
        have "infinite ({n. f n \<in> F k} - {.. i})"
immler@69544
  1685
          using \<open>infinite {n. f n \<in> F k}\<close> by auto
immler@69544
  1686
        from infinite_imp_nonempty[OF this]
immler@69544
  1687
        show "\<exists>x>i. f x \<in> F k"
immler@69544
  1688
          by (simp add: set_eq_iff not_le conj_commute)
immler@69544
  1689
      qed
immler@69544
  1690
immler@69544
  1691
      define t where "t = rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
immler@69544
  1692
      have "strict_mono t"
immler@69544
  1693
        unfolding strict_mono_Suc_iff by (simp add: t_def sel)
immler@69544
  1694
      moreover have "\<forall>i. (f \<circ> t) i \<in> s"
immler@69544
  1695
        using f by auto
immler@69544
  1696
      moreover
immler@69544
  1697
      {
immler@69544
  1698
        fix n
immler@69544
  1699
        have "(f \<circ> t) n \<in> F n"
immler@69544
  1700
          by (cases n) (simp_all add: t_def sel)
immler@69544
  1701
      }
immler@69544
  1702
      note t = this
immler@69544
  1703
immler@69544
  1704
      have "Cauchy (f \<circ> t)"
immler@69544
  1705
      proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
immler@69544
  1706
        fix r :: real and N n m
immler@69544
  1707
        assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
immler@69544
  1708
        then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
immler@69544
  1709
          using F_dec t by (auto simp: e_def field_simps of_nat_Suc)
immler@69544
  1710
        with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
immler@69544
  1711
          by (auto simp: subset_eq)
immler@69544
  1712
        with dist_triangle[of "(f \<circ> t) m" "(f \<circ> t) n" x] \<open>2 * e N < r\<close>
immler@69544
  1713
        show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
immler@69544
  1714
          by (simp add: dist_commute)
immler@69544
  1715
      qed
immler@69544
  1716
immler@69544
  1717
      ultimately show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
immler@69544
  1718
        using assms unfolding complete_def by blast
immler@69544
  1719
    qed
immler@69544
  1720
  qed
immler@69544
  1721
qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
immler@69544
  1722
immler@69544
  1723
lemma cauchy_imp_bounded:
immler@69544
  1724
  assumes "Cauchy s"
immler@69544
  1725
  shows "bounded (range s)"
immler@69544
  1726
proof -
immler@69544
  1727
  from assms obtain N :: nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1"
immler@69544
  1728
    unfolding cauchy_def by force
immler@69544
  1729
  then have N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
immler@69544
  1730
  moreover
immler@69544
  1731
  have "bounded (s ` {0..N})"
immler@69544
  1732
    using finite_imp_bounded[of "s ` {1..N}"] by auto
immler@69544
  1733
  then obtain a where a:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> a"
immler@69544
  1734
    unfolding bounded_any_center [where a="s N"] by auto
immler@69544
  1735
  ultimately show "?thesis"
immler@69544
  1736
    unfolding bounded_any_center [where a="s N"]
immler@69544
  1737
    apply (rule_tac x="max a 1" in exI, auto)
immler@69544
  1738
    apply (erule_tac x=y in allE)
immler@69544
  1739
    apply (erule_tac x=y in ballE, auto)
immler@69544
  1740
    done
immler@69544
  1741
qed
immler@69544
  1742
immler@69544
  1743
instance heine_borel < complete_space
immler@69544
  1744
proof
immler@69544
  1745
  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
immler@69544
  1746
  then have "bounded (range f)"
immler@69544
  1747
    by (rule cauchy_imp_bounded)
immler@69544
  1748
  then have "compact (closure (range f))"
immler@69544
  1749
    unfolding compact_eq_bounded_closed by auto
immler@69544
  1750
  then have "complete (closure (range f))"
immler@69544
  1751
    by (rule compact_imp_complete)
immler@69544
  1752
  moreover have "\<forall>n. f n \<in> closure (range f)"
immler@69544
  1753
    using closure_subset [of "range f"] by auto
immler@69544
  1754
  ultimately have "\<exists>l\<in>closure (range f). (f \<longlongrightarrow> l) sequentially"
immler@69544
  1755
    using \<open>Cauchy f\<close> unfolding complete_def by auto
immler@69544
  1756
  then show "convergent f"
immler@69544
  1757
    unfolding convergent_def by auto
immler@69544
  1758
qed
immler@69544
  1759
immler@69544
  1760
lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"
immler@69544
  1761
proof (rule completeI)
immler@69544
  1762
  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
immler@69544
  1763
  then have "convergent f" by (rule Cauchy_convergent)
immler@69544
  1764
  then show "\<exists>l\<in>UNIV. f \<longlonglongrightarrow> l" unfolding convergent_def by simp
immler@69544
  1765
qed
immler@69544
  1766
immler@69544
  1767
lemma complete_imp_closed:
immler@69544
  1768
  fixes S :: "'a::metric_space set"
immler@69544
  1769
  assumes "complete S"
immler@69544
  1770
  shows "closed S"
immler@69544
  1771
proof (unfold closed_sequential_limits, clarify)
immler@69544
  1772
  fix f x assume "\<forall>n. f n \<in> S" and "f \<longlonglongrightarrow> x"
immler@69544
  1773
  from \<open>f \<longlonglongrightarrow> x\<close> have "Cauchy f"
immler@69544
  1774
    by (rule LIMSEQ_imp_Cauchy)
immler@69544
  1775
  with \<open>complete S\<close> and \<open>\<forall>n. f n \<in> S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
immler@69544
  1776
    by (rule completeE)
immler@69544
  1777
  from \<open>f \<longlonglongrightarrow> x\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "x = l"
immler@69544
  1778
    by (rule LIMSEQ_unique)
immler@69544
  1779
  with \<open>l \<in> S\<close> show "x \<in> S"
immler@69544
  1780
    by simp
immler@69544
  1781
qed
immler@69544
  1782
immler@69544
  1783
lemma complete_Int_closed:
immler@69544
  1784
  fixes S :: "'a::metric_space set"
immler@69544
  1785
  assumes "complete S" and "closed t"
immler@69544
  1786
  shows "complete (S \<inter> t)"
immler@69544
  1787
proof (rule completeI)
immler@69544
  1788
  fix f assume "\<forall>n. f n \<in> S \<inter> t" and "Cauchy f"
immler@69544
  1789
  then have "\<forall>n. f n \<in> S" and "\<forall>n. f n \<in> t"
immler@69544
  1790
    by simp_all
immler@69544
  1791
  from \<open>complete S\<close> obtain l where "l \<in> S" and "f \<longlonglongrightarrow> l"
immler@69544
  1792
    using \<open>\<forall>n. f n \<in> S\<close> and \<open>Cauchy f\<close> by (rule completeE)
immler@69544
  1793
  from \<open>closed t\<close> and \<open>\<forall>n. f n \<in> t\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "l \<in> t"
immler@69544
  1794
    by (rule closed_sequentially)
immler@69544
  1795
  with \<open>l \<in> S\<close> and \<open>f \<longlonglongrightarrow> l\<close> show "\<exists>l\<in>S \<inter> t. f \<longlonglongrightarrow> l"
immler@69544
  1796
    by fast
immler@69544
  1797
qed
immler@69544
  1798
immler@69544
  1799
lemma complete_closed_subset:
immler@69544
  1800
  fixes S :: "'a::metric_space set"
immler@69544
  1801
  assumes "closed S" and "S \<subseteq> t" and "complete t"
immler@69544
  1802
  shows "complete S"
immler@69544
  1803
  using assms complete_Int_closed [of t S] by (simp add: Int_absorb1)
immler@69544
  1804
immler@69544
  1805
lemma complete_eq_closed:
immler@69544
  1806
  fixes S :: "('a::complete_space) set"
immler@69544
  1807
  shows "complete S \<longleftrightarrow> closed S"
immler@69544
  1808
proof
immler@69544
  1809
  assume "closed S" then show "complete S"
immler@69544
  1810
    using subset_UNIV complete_UNIV by (rule complete_closed_subset)
immler@69544
  1811
next
immler@69544
  1812
  assume "complete S" then show "closed S"
immler@69544
  1813
    by (rule complete_imp_closed)
immler@69544
  1814
qed
immler@69544
  1815
immler@69544
  1816
lemma convergent_eq_Cauchy:
immler@69544
  1817
  fixes S :: "nat \<Rightarrow> 'a::complete_space"
immler@69544
  1818
  shows "(\<exists>l. (S \<longlongrightarrow> l) sequentially) \<longleftrightarrow> Cauchy S"
immler@69544
  1819
  unfolding Cauchy_convergent_iff convergent_def ..
immler@69544
  1820
immler@69544
  1821
lemma convergent_imp_bounded:
immler@69544
  1822
  fixes S :: "nat \<Rightarrow> 'a::metric_space"
immler@69544
  1823
  shows "(S \<longlongrightarrow> l) sequentially \<Longrightarrow> bounded (range S)"
immler@69544
  1824
  by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
immler@69544
  1825
immler@69544
  1826
lemma frontier_subset_compact:
immler@69544
  1827
  fixes S :: "'a::heine_borel set"
immler@69544
  1828
  shows "compact S \<Longrightarrow> frontier S \<subseteq> S"
immler@69544
  1829
  using frontier_subset_closed compact_eq_bounded_closed
immler@69544
  1830
  by blast
immler@69544
  1831
immler@69613
  1832
lemma continuous_closed_imp_Cauchy_continuous:
immler@69613
  1833
  fixes S :: "('a::complete_space) set"
immler@69613
  1834
  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
immler@69613
  1835
  apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
immler@69613
  1836
  by (meson LIMSEQ_imp_Cauchy complete_def)
immler@69613
  1837
immler@69613
  1838
lemma banach_fix_type:
immler@69613
  1839
  fixes f::"'a::complete_space\<Rightarrow>'a"
immler@69613
  1840
  assumes c:"0 \<le> c" "c < 1"
immler@69613
  1841
      and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
immler@69613
  1842
  shows "\<exists>!x. (f x = x)"
immler@69613
  1843
  using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
immler@69613
  1844
  by auto
immler@69613
  1845
immler@69613
  1846
immler@69615
  1847
subsection%unimportant\<open> Finite intersection property\<close>
immler@69615
  1848
immler@69615
  1849
text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
immler@69615
  1850
immler@69615
  1851
lemma closed_imp_fip:
immler@69615
  1852
  fixes S :: "'a::heine_borel set"
immler@69615
  1853
  assumes "closed S"
immler@69615
  1854
      and T: "T \<in> \<F>" "bounded T"
immler@69615
  1855
      and clof: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
immler@69615
  1856
      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}"
immler@69615
  1857
    shows "S \<inter> \<Inter>\<F> \<noteq> {}"
immler@69615
  1858
proof -
immler@69615
  1859
  have "compact (S \<inter> T)"
immler@69615
  1860
    using \<open>closed S\<close> clof compact_eq_bounded_closed T by blast
immler@69615
  1861
  then have "(S \<inter> T) \<inter> \<Inter>\<F> \<noteq> {}"
immler@69615
  1862
    apply (rule compact_imp_fip)
immler@69615
  1863
     apply (simp add: clof)
immler@69615
  1864
    by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \<open>T \<in> \<F>\<close>)
immler@69615
  1865
  then show ?thesis by blast
immler@69615
  1866
qed
immler@69615
  1867
immler@69615
  1868
lemma closed_imp_fip_compact:
immler@69615
  1869
  fixes S :: "'a::heine_borel set"
immler@69615
  1870
  shows
immler@69615
  1871
   "\<lbrakk>closed S; \<And>T. T \<in> \<F> \<Longrightarrow> compact T;
immler@69615
  1872
     \<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> S \<inter> \<Inter>\<F>' \<noteq> {}\<rbrakk>
immler@69615
  1873
        \<Longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}"
immler@69615
  1874
by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)
immler@69615
  1875
immler@69615
  1876
lemma closed_fip_Heine_Borel:
immler@69615
  1877
  fixes \<F> :: "'a::heine_borel set set"
immler@69615
  1878
  assumes "closed S" "T \<in> \<F>" "bounded T"
immler@69615
  1879
      and "\<And>T. T \<in> \<F> \<Longrightarrow> closed T"
immler@69615
  1880
      and "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
immler@69615
  1881
    shows "\<Inter>\<F> \<noteq> {}"
immler@69615
  1882
proof -
immler@69615
  1883
  have "UNIV \<inter> \<Inter>\<F> \<noteq> {}"
immler@69615
  1884
    using assms closed_imp_fip [OF closed_UNIV] by auto
immler@69615
  1885
  then show ?thesis by simp
immler@69615
  1886
qed
immler@69615
  1887
immler@69615
  1888
lemma compact_fip_Heine_Borel:
immler@69615
  1889
  fixes \<F> :: "'a::heine_borel set set"
immler@69615
  1890
  assumes clof: "\<And>T. T \<in> \<F> \<Longrightarrow> compact T"
immler@69615
  1891
      and none: "\<And>\<F>'. \<lbrakk>finite \<F>'; \<F>' \<subseteq> \<F>\<rbrakk> \<Longrightarrow> \<Inter>\<F>' \<noteq> {}"
immler@69615
  1892
    shows "\<Inter>\<F> \<noteq> {}"
immler@69615
  1893
by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)
immler@69615
  1894
immler@69615
  1895
lemma compact_sequence_with_limit:
immler@69615
  1896
  fixes f :: "nat \<Rightarrow> 'a::heine_borel"
immler@69615
  1897
  shows "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> compact (insert l (range f))"
immler@69615
  1898
apply (simp add: compact_eq_bounded_closed, auto)
immler@69615
  1899
apply (simp add: convergent_imp_bounded)
immler@69615
  1900
by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
immler@69615
  1901
immler@69615
  1902
immler@69613
  1903
subsection \<open>Properties of Balls and Spheres\<close>
immler@69611
  1904
immler@69611
  1905
lemma compact_cball[simp]:
immler@69611
  1906
  fixes x :: "'a::heine_borel"
immler@69611
  1907
  shows "compact (cball x e)"
immler@69611
  1908
  using compact_eq_bounded_closed bounded_cball closed_cball
immler@69611
  1909
  by blast
immler@69611
  1910
immler@69611
  1911
lemma compact_frontier_bounded[intro]:
immler@69611
  1912
  fixes S :: "'a::heine_borel set"
immler@69611
  1913
  shows "bounded S \<Longrightarrow> compact (frontier S)"
immler@69611
  1914
  unfolding frontier_def
immler@69611
  1915
  using compact_eq_bounded_closed
immler@69611
  1916
  by blast
immler@69611
  1917
immler@69611
  1918
lemma compact_frontier[intro]:
immler@69611
  1919
  fixes S :: "'a::heine_borel set"
immler@69611
  1920
  shows "compact S \<Longrightarrow> compact (frontier S)"
immler@69611
  1921
  using compact_eq_bounded_closed compact_frontier_bounded
immler@69611
  1922
  by blast
immler@69611
  1923
immler@69611
  1924
immler@69613
  1925
subsection \<open>Distance from a Set\<close>
immler@69611
  1926
immler@69611
  1927
lemma distance_attains_sup:
immler@69611
  1928
  assumes "compact s" "s \<noteq> {}"
immler@69611
  1929
  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
immler@69611
  1930
proof (rule continuous_attains_sup [OF assms])
immler@69611
  1931
  {
immler@69611
  1932
    fix x
immler@69611
  1933
    assume "x\<in>s"
immler@69611
  1934
    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
immler@69611
  1935
      by (intro tendsto_dist tendsto_const tendsto_ident_at)
immler@69611
  1936
  }
immler@69611
  1937
  then show "continuous_on s (dist a)"
immler@69611
  1938
    unfolding continuous_on ..
immler@69611
  1939
qed
immler@69611
  1940
immler@69611
  1941
text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
immler@69611
  1942
immler@69611
  1943
lemma distance_attains_inf:
immler@69611
  1944
  fixes a :: "'a::heine_borel"
immler@69611
  1945
  assumes "closed s" and "s \<noteq> {}"
immler@69611
  1946
  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
immler@69611
  1947
proof -
immler@69611
  1948
  from assms obtain b where "b \<in> s" by auto
immler@69611
  1949
  let ?B = "s \<inter> cball a (dist b a)"
immler@69611
  1950
  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
immler@69611
  1951
    by (auto simp: dist_commute)
immler@69611
  1952
  moreover have "continuous_on ?B (dist a)"
immler@69611
  1953
    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
immler@69611
  1954
  moreover have "compact ?B"
immler@69611
  1955
    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
immler@69611
  1956
  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
immler@69611
  1957
    by (metis continuous_attains_inf)
immler@69611
  1958
  with that show ?thesis by fastforce
immler@69611
  1959
qed
immler@69611
  1960
immler@69613
  1961
immler@69611
  1962
subsection \<open>Infimum Distance\<close>
immler@69611
  1963
immler@69611
  1964
definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
immler@69611
  1965
immler@69611
  1966
lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
immler@69611
  1967
  by (auto intro!: zero_le_dist)
immler@69611
  1968
immler@69611
  1969
lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"
immler@69611
  1970
  by (simp add: infdist_def)
immler@69611
  1971
immler@69611
  1972
lemma infdist_nonneg: "0 \<le> infdist x A"
immler@69611
  1973
  by (auto simp: infdist_def intro: cINF_greatest)
immler@69611
  1974
immler@69611
  1975
lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
immler@69611
  1976
  by (auto intro: cINF_lower simp add: infdist_def)
immler@69611
  1977
immler@69611
  1978
lemma infdist_le2: "a \<in> A \<Longrightarrow> dist x a \<le> d \<Longrightarrow> infdist x A \<le> d"
immler@69611
  1979
  by (auto intro!: cINF_lower2 simp add: infdist_def)
immler@69611
  1980
immler@69611
  1981
lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
immler@69611
  1982
  by (auto intro!: antisym infdist_nonneg infdist_le2)
immler@69611
  1983
immler@69611
  1984
lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
immler@69611
  1985
proof (cases "A = {}")
immler@69611
  1986
  case True
immler@69611
  1987
  then show ?thesis by (simp add: infdist_def)
immler@69611
  1988
next
immler@69611
  1989
  case False
immler@69611
  1990
  then obtain a where "a \<in> A" by auto
immler@69611
  1991
  have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
immler@69611
  1992
  proof (rule cInf_greatest)
immler@69611
  1993
    from \<open>A \<noteq> {}\<close> show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}"
immler@69611
  1994
      by simp
immler@69611
  1995
    fix d
immler@69611
  1996
    assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
immler@69611
  1997
    then obtain a where d: "d = dist x y + dist y a" "a \<in> A"
immler@69611
  1998
      by auto
immler@69611
  1999
    show "infdist x A \<le> d"
immler@69611
  2000
      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>]
immler@69611
  2001
    proof (rule cINF_lower2)
immler@69611
  2002
      show "a \<in> A" by fact
immler@69611
  2003
      show "dist x a \<le> d"
immler@69611
  2004
        unfolding d by (rule dist_triangle)
immler@69611
  2005
    qed simp
immler@69611
  2006
  qed
immler@69611
  2007
  also have "\<dots> = dist x y + infdist y A"
immler@69611
  2008
  proof (rule cInf_eq, safe)
immler@69611
  2009
    fix a
immler@69611
  2010
    assume "a \<in> A"
immler@69611
  2011
    then show "dist x y + infdist y A \<le> dist x y + dist y a"
immler@69611
  2012
      by (auto intro: infdist_le)
immler@69611
  2013
  next
immler@69611
  2014
    fix i
immler@69611
  2015
    assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
immler@69611
  2016
    then have "i - dist x y \<le> infdist y A"
immler@69611
  2017
      unfolding infdist_notempty[OF \<open>A \<noteq> {}\<close>] using \<open>a \<in> A\<close>
immler@69611
  2018
      by (intro cINF_greatest) (auto simp: field_simps)
immler@69611
  2019
    then show "i \<le> dist x y + infdist y A"
immler@69611
  2020
      by simp
immler@69611
  2021
  qed
immler@69611
  2022
  finally show ?thesis by simp
immler@69611
  2023
qed
immler@69611
  2024
immler@69611
  2025
lemma in_closure_iff_infdist_zero:
immler@69611
  2026
  assumes "A \<noteq> {}"
immler@69611
  2027
  shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
immler@69611
  2028
proof
immler@69611
  2029
  assume "x \<in> closure A"
immler@69611
  2030
  show "infdist x A = 0"
immler@69611
  2031
  proof (rule ccontr)
immler@69611
  2032
    assume "infdist x A \<noteq> 0"
immler@69611
  2033
    with infdist_nonneg[of x A] have "infdist x A > 0"
immler@69611
  2034
      by auto
immler@69611
  2035
    then have "ball x (infdist x A) \<inter> closure A = {}"
immler@69611
  2036
      apply auto
immler@69611
  2037
      apply (metis \<open>x \<in> closure A\<close> closure_approachable dist_commute infdist_le not_less)
immler@69611
  2038
      done
immler@69611
  2039
    then have "x \<notin> closure A"
immler@69611
  2040
      by (metis \<open>0 < infdist x A\<close> centre_in_ball disjoint_iff_not_equal)
immler@69611
  2041
    then show False using \<open>x \<in> closure A\<close> by simp
immler@69611
  2042
  qed
immler@69611
  2043
next
immler@69611
  2044
  assume x: "infdist x A = 0"
immler@69611
  2045
  then obtain a where "a \<in> A"
immler@69611
  2046
    by atomize_elim (metis all_not_in_conv assms)
immler@69611
  2047
  show "x \<in> closure A"
immler@69611
  2048
    unfolding closure_approachable
immler@69611
  2049
    apply safe
immler@69611
  2050
  proof (rule ccontr)
immler@69611
  2051
    fix e :: real
immler@69611
  2052
    assume "e > 0"
immler@69611
  2053
    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
immler@69611
  2054
    then have "infdist x A \<ge> e" using \<open>a \<in> A\<close>
immler@69611
  2055
      unfolding infdist_def
immler@69611
  2056
      by (force simp: dist_commute intro: cINF_greatest)
immler@69611
  2057
    with x \<open>e > 0\<close> show False by auto
immler@69611
  2058
  qed
immler@69611
  2059
qed
immler@69611
  2060
immler@69611
  2061
lemma in_closed_iff_infdist_zero:
immler@69611
  2062
  assumes "closed A" "A \<noteq> {}"
immler@69611
  2063
  shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
immler@69611
  2064
proof -
immler@69611
  2065
  have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
immler@69611
  2066
    by (rule in_closure_iff_infdist_zero) fact
immler@69611
  2067
  with assms show ?thesis by simp
immler@69611
  2068
qed
immler@69611
  2069
immler@69611
  2070
lemma infdist_pos_not_in_closed:
immler@69611
  2071
  assumes "closed S" "S \<noteq> {}" "x \<notin> S"
immler@69611
  2072
  shows "infdist x S > 0"
immler@69611
  2073
using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
immler@69611
  2074
immler@69611
  2075
lemma
immler@69611
  2076
  infdist_attains_inf:
immler@69611
  2077
  fixes X::"'a::heine_borel set"
immler@69611
  2078
  assumes "closed X"
immler@69611
  2079
  assumes "X \<noteq> {}"
immler@69611
  2080
  obtains x where "x \<in> X" "infdist y X = dist y x"
immler@69611
  2081
proof -
immler@69611
  2082
  have "bdd_below (dist y ` X)"
immler@69611
  2083
    by auto
immler@69611
  2084
  from distance_attains_inf[OF assms, of y]
immler@69611
  2085
  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
immler@69611
  2086
  have "infdist y X = dist y x"
immler@69611
  2087
    by (auto simp: infdist_def assms
immler@69611
  2088
      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
immler@69611
  2089
  with \<open>x \<in> X\<close> show ?thesis ..
immler@69611
  2090
qed
immler@69611
  2091
immler@69611
  2092
immler@69611
  2093
text \<open>Every metric space is a T4 space:\<close>
immler@69611
  2094
immler@69611
  2095
instance metric_space \<subseteq> t4_space
immler@69611
  2096
proof
immler@69611
  2097
  fix S T::"'a set" assume H: "closed S" "closed T" "S \<inter> T = {}"
immler@69611
  2098
  consider "S = {}" | "T = {}" | "S \<noteq> {} \<and> T \<noteq> {}" by auto
immler@69611
  2099
  then show "\<exists>U V. open U \<and> open V \<and> S \<subseteq> U \<and> T \<subseteq> V \<and> U \<inter> V = {}"
immler@69611
  2100
  proof (cases)
immler@69611
  2101
    case 1
immler@69611
  2102
    show ?thesis
immler@69611
  2103
      apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto
immler@69611
  2104
  next
immler@69611
  2105
    case 2
immler@69611
  2106
    show ?thesis
immler@69611
  2107
      apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto
immler@69611
  2108
  next
immler@69611
  2109
    case 3
immler@69611
  2110
    define U where "U = (\<Union>x\<in>S. ball x ((infdist x T)/2))"
immler@69611
  2111
    have A: "open U" unfolding U_def by auto
immler@69611
  2112
    have "infdist x T > 0" if "x \<in> S" for x
immler@69611
  2113
      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
immler@69611
  2114
    then have B: "S \<subseteq> U" unfolding U_def by auto
immler@69611
  2115
    define V where "V = (\<Union>x\<in>T. ball x ((infdist x S)/2))"
immler@69611
  2116
    have C: "open V" unfolding V_def by auto
immler@69611
  2117
    have "infdist x S > 0" if "x \<in> T" for x
immler@69611
  2118
      using H that 3 by (auto intro!: infdist_pos_not_in_closed)
immler@69611
  2119
    then have D: "T \<subseteq> V" unfolding V_def by auto
immler@69611
  2120
immler@69611
  2121
    have "(ball x ((infdist x T)/2)) \<inter> (ball y ((infdist y S)/2)) = {}" if "x \<in> S" "y \<in> T" for x y
immler@69611
  2122
    proof (auto)
immler@69611
  2123
      fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"
immler@69611
  2124
      have "2 * dist x y \<le> 2 * dist x z + 2 * dist y z"
immler@69611
  2125
        using dist_triangle[of x y z] by (auto simp add: dist_commute)
immler@69611
  2126
      also have "... < infdist x T + infdist y S"
immler@69611
  2127
        using H by auto
immler@69611
  2128
      finally have "dist x y < infdist x T \<or> dist x y < infdist y S"
immler@69611
  2129
        by auto
immler@69611
  2130
      then show False
immler@69611
  2131
        using infdist_le[OF \<open>x \<in> S\<close>, of y] infdist_le[OF \<open>y \<in> T\<close>, of x] by (auto simp add: dist_commute)
immler@69611
  2132
    qed
immler@69611
  2133
    then have E: "U \<inter> V = {}"
immler@69611
  2134
      unfolding U_def V_def by auto
immler@69611
  2135
    show ?thesis
immler@69611
  2136
      apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto
immler@69611
  2137
  qed
immler@69611
  2138
qed
immler@69611
  2139
immler@69611
  2140
lemma tendsto_infdist [tendsto_intros]:
immler@69611
  2141
  assumes f: "(f \<longlongrightarrow> l) F"
immler@69611
  2142
  shows "((\<lambda>x. infdist (f x) A) \<longlongrightarrow> infdist l A) F"
immler@69611
  2143
proof (rule tendstoI)
immler@69611
  2144
  fix e ::real
immler@69611
  2145
  assume "e > 0"
immler@69611
  2146
  from tendstoD[OF f this]
immler@69611
  2147
  show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
immler@69611
  2148
  proof (eventually_elim)
immler@69611
  2149
    fix x
immler@69611
  2150
    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
immler@69611
  2151
    have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
immler@69611
  2152
      by (simp add: dist_commute dist_real_def)
immler@69611
  2153
    also assume "dist (f x) l < e"
immler@69611
  2154
    finally show "dist (infdist (f x) A) (infdist l A) < e" .
immler@69611
  2155
  qed
immler@69611
  2156
qed
immler@69611
  2157
immler@69611
  2158
lemma continuous_infdist[continuous_intros]:
immler@69611
  2159
  assumes "continuous F f"
immler@69611
  2160
  shows "continuous F (\<lambda>x. infdist (f x) A)"
immler@69611
  2161
  using assms unfolding continuous_def by (rule tendsto_infdist)
immler@69611
  2162
immler@69611
  2163
lemma compact_infdist_le:
immler@69611
  2164
  fixes A::"'a::heine_borel set"
immler@69611
  2165
  assumes "A \<noteq> {}"
immler@69611
  2166
  assumes "compact A"
immler@69611
  2167
  assumes "e > 0"
immler@69611
  2168
  shows "compact {x. infdist x A \<le> e}"
immler@69611
  2169
proof -
immler@69611
  2170
  from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
immler@69611
  2171
    continuous_infdist[OF continuous_ident, of _ UNIV A]
immler@69611
  2172
  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
immler@69611
  2173
  moreover
immler@69611
  2174
  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
immler@69611
  2175
    by (auto simp: compact_eq_bounded_closed bounded_def)
immler@69611
  2176
  {
immler@69611
  2177
    fix y
immler@69611
  2178
    assume le: "infdist y A \<le> e"
immler@69611
  2179
    from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
immler@69611
  2180
    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
immler@69611
  2181
    have "dist x0 y \<le> dist y z + dist x0 z"
immler@69611
  2182
      by (metis dist_commute dist_triangle)
immler@69611
  2183
    also have "dist y z \<le> e" using le z by simp
immler@69611
  2184
    also have "dist x0 z \<le> b" using b z by simp
immler@69611
  2185
    finally have "dist x0 y \<le> b + e" by arith
immler@69611
  2186
  } then
immler@69611
  2187
  have "bounded {x. infdist x A \<le> e}"
immler@69611
  2188
    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
immler@69611
  2189
  ultimately show "compact {x. infdist x A \<le> e}"
immler@69611
  2190
    by (simp add: compact_eq_bounded_closed)
immler@69611
  2191
qed
immler@69611
  2192
immler@69611
  2193
immler@69613
  2194
subsection \<open>Separation between Points and Sets\<close>
immler@69613
  2195
immler@69613
  2196
proposition separate_point_closed:
immler@69613
  2197
  fixes s :: "'a::heine_borel set"
immler@69613
  2198
  assumes "closed s" and "a \<notin> s"
immler@69613
  2199
  shows "\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x"
immler@69613
  2200
proof (cases "s = {}")
immler@69613
  2201
  case True
immler@69613
  2202
  then show ?thesis by(auto intro!: exI[where x=1])
immler@69544
  2203
next
immler@69613
  2204
  case False
immler@69613
  2205
  from assms obtain x where "x\<in>s" "\<forall>y\<in>s. dist a x \<le> dist a y"
immler@69613
  2206
    using \<open>s \<noteq> {}\<close> by (blast intro: distance_attains_inf [of s a])
immler@69613
  2207
  with \<open>x\<in>s\<close> show ?thesis using dist_pos_lt[of a x] and\<open>a \<notin> s\<close>
immler@69613
  2208
    by blast
immler@69544
  2209
qed
immler@69544
  2210
immler@69613
  2211
proposition separate_compact_closed:
immler@69613
  2212
  fixes s t :: "'a::heine_borel set"
immler@69613
  2213
  assumes "compact s"
immler@69613
  2214
    and t: "closed t" "s \<inter> t = {}"
immler@69613
  2215
  shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
immler@69613
  2216
proof cases
immler@69613
  2217
  assume "s \<noteq> {} \<and> t \<noteq> {}"
immler@69613
  2218
  then have "s \<noteq> {}" "t \<noteq> {}" by auto
immler@69613
  2219
  let ?inf = "\<lambda>x. infdist x t"
immler@69613
  2220
  have "continuous_on s ?inf"
immler@69613
  2221
    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)
immler@69613
  2222
  then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"
immler@69613
  2223
    using continuous_attains_inf[OF \<open>compact s\<close> \<open>s \<noteq> {}\<close>] by auto
immler@69613
  2224
  then have "0 < ?inf x"
immler@69613
  2225
    using t \<open>t \<noteq> {}\<close> in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)
immler@69613
  2226
  moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y"
immler@69613
  2227
    using x by (auto intro: order_trans infdist_le)
immler@69613
  2228
  ultimately show ?thesis by auto
immler@69613
  2229
qed (auto intro!: exI[of _ 1])
immler@69613
  2230
immler@69613
  2231
proposition separate_closed_compact:
immler@69613
  2232
  fixes s t :: "'a::heine_borel set"
immler@69613
  2233
  assumes "closed s"
immler@69613
  2234
    and "compact t"
immler@69613
  2235
    and "s \<inter> t = {}"
immler@69613
  2236
  shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
immler@69613
  2237
proof -
immler@69613
  2238
  have *: "t \<inter> s = {}"
immler@69613
  2239
    using assms(3) by auto
immler@69613
  2240
  show ?thesis
immler@69613
  2241
    using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
immler@69613
  2242
qed
immler@69613
  2243
immler@69613
  2244
proposition compact_in_open_separated:
immler@69613
  2245
  fixes A::"'a::heine_borel set"
immler@69613
  2246
  assumes "A \<noteq> {}"
immler@69613
  2247
  assumes "compact A"
immler@69613
  2248
  assumes "open B"
immler@69613
  2249
  assumes "A \<subseteq> B"
immler@69613
  2250
  obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
immler@69613
  2251
proof atomize_elim
immler@696