Quelle  Isolated.thy   Sprache: Isabelle

theory Isolated
  imports "Elementary_Metric_Spaces" "Sparse_In"

begin

subsection ‹Isolate and discrete›

definition (in topological_space) isolated_in:: "'a \ 'a set \ bool"  (infixr ‹isolated'_in\ 60)
  where "x isolated_in S \ (x\S \ (\T. open T \ T \ S = {x}))"

definition (in topological_space) discrete:: "'a set \ bool"
  where "discrete S \ (\x\S. x isolated_in S)"

definition (in metric_space) uniform_discrete :: "'a set \ bool" where
  "uniform_discrete S \ (\e>0. \x\S. \y\S. dist x y < e \ x = y)"

lemma discreteI: "(\x. x \ X \ x isolated_in X ) \ discrete X"
  unfolding discrete_def by auto

lemma discreteD: "discrete X \ x \ X \ x isolated_in X "
  unfolding discrete_def by auto
 
lemma uniformI1:
  assumes "e>0" "\x y. \x\S;y\S;dist x y \ x =y "
  shows "uniform_discrete S"
unfolding uniform_discrete_def using assms by auto

lemma uniformI2:
  assumes "e>0" "\x y. \x\S;y\S;x\y\ \ dist x y\e "
  shows "uniform_discrete S"
unfolding uniform_discrete_def using assms not_less by blast

lemma isolated_in_islimpt_iff:"(x isolated_in S) \ (\ (x islimpt S) \ x\S)"
  unfolding isolated_in_def islimpt_def by auto

lemma isolated_in_dist_Ex_iff:
  fixes x::"'a::metric_space"
  shows "x isolated_in S \ (x\S \ (\e>0. \y\S. dist x y < e \ y=x))"
unfolding isolated_in_islimpt_iff islimpt_approachable by (metis dist_commute)

lemma discrete_empty[simp]: "discrete {}"
  unfolding discrete_def by auto

lemma uniform_discrete_empty[simp]: "uniform_discrete {}"
  unfolding uniform_discrete_def by (simp add: gt_ex)

lemma isolated_in_insert:
  fixes x :: "'a::t1_space"
  shows "x isolated_in (insert a S) \ x isolated_in S \ (x=a \ \ (x islimpt S))"
by (meson insert_iff islimpt_insert isolated_in_islimpt_iff)

lemma isolated_inI:
  assumes "x\S" "open T" "T \ S = {x}"
  shows   "x isolated_in S"
  using assms unfolding isolated_in_def by auto

lemma isolated_inE:
  assumes "x isolated_in S"
  obtains T where "x \ S" "open T" "T \ S = {x}"
  using assms that unfolding isolated_in_def by force

lemma isolated_inE_dist:
  assumes "x isolated_in S"
  obtains d where "d > 0" "\y. y \ S \ dist x y < d \ y = x"
  by (meson assms isolated_in_dist_Ex_iff)

lemma isolated_in_altdef: 
  "x isolated_in S \ (x\S \ eventually (\y. y \ S) (at x))"
proof 
  assume "x isolated_in S"
  from isolated_inE[OF this] 
  obtain T where "x \ S" and T:"open T" "T \ S = {x}"
    by metis
  have "\\<^sub>F y in nhds x. y \ T"
    apply (rule eventually_nhds_in_open)
    using T by auto
  then have  "eventually (\y. y \ T - {x}) (at x)"
    unfolding eventually_at_filter by eventually_elim auto
  then have "eventually (\y. y \ S) (at x)"
    by eventually_elim (use T in auto)
  then show " x \ S \ (\\<^sub>F y in at x. y \ S)" using ‹x ∈ S› by auto
next
  assume "x \ S \ (\\<^sub>F y in at x. y \ S)" 
  then have "\\<^sub>F y in at x. y \ S" "x\S" by auto
  from this(1) have "eventually (\y. y \ S \ y = x) (nhds x)"
    unfolding eventually_at_filter by eventually_elim auto
  then obtain T where T:"open T" "x \ T" "(\y\T. y \ S \ y = x)" 
    unfolding eventually_nhds by auto
  with ‹x ∈ S› have "T \ S = {x}"  
    by fastforce
  with ‹x∈S› ‹open T›
  show "x isolated_in S"
    unfolding isolated_in_def by auto
qed

lemma discrete_altdef:
  "discrete S \ (\x\S. \\<^sub>F y in at x. y \ S)"
  unfolding discrete_def isolated_in_altdef by auto

(*
TODO.
Other than

  uniform_discrete S \<longrightarrow> discrete S
  uniform_discrete S \<longrightarrow> closed S

, we should be able to prove

  discrete S \<and> closed S \<longrightarrow> uniform_discrete S

but the proof (based on Tietze Extension Theorem) seems not very trivial to me. Informal proofs can be found in

http://topology.auburn.edu/tp/reprints/v30/tp30120.pdf
http://msp.org/pjm/1959/9-2/pjm-v9-n2-p19-s.pdf
*)

lemma uniform_discrete_imp_closed:
  "uniform_discrete S \ closed S"
  by (meson discrete_imp_closed uniform_discrete_def)

lemma uniform_discrete_imp_discrete:
  "uniform_discrete S \ discrete S"
  by (metis discrete_def isolated_in_dist_Ex_iff uniform_discrete_def)

lemma isolated_in_subset:"x isolated_in S \ T \ S \ x\T \ x isolated_in T"
  unfolding isolated_in_def by fastforce

lemma discrete_subset[elim]: "discrete S \ T \ S \ discrete T"
  unfolding discrete_def using islimpt_subset isolated_in_islimpt_iff by blast

lemma uniform_discrete_subset[elim]: "uniform_discrete S \ T \ S \ uniform_discrete T"
  by (meson subsetD uniform_discrete_def)

lemma continuous_on_discrete: "discrete S \ continuous_on S f"
  unfolding continuous_on_topological by (metis discrete_def islimptI isolated_in_islimpt_iff)

lemma uniform_discrete_insert: "uniform_discrete (insert a S) \ uniform_discrete S"
proof
  assume asm:"uniform_discrete S"
  let ?thesis = "uniform_discrete (insert a S)"
  have ?thesis when "a\S" using that asm by (simp add: insert_absorb)
  moreover have ?thesis when "S={}" using that asm by (simp add: uniform_discrete_def)
  moreover have ?thesis when "a\S" "S\{}"
  proof -
    obtain e1 where "e1>0" and e1_dist:"\x\S. \y\S. dist y x < e1 \ y = x"
      using asm unfolding uniform_discrete_def by auto
    define e2 where "e2 \ min (setdist {a} S) e1"
    have "closed S" using asm uniform_discrete_imp_closed by auto
    then have "e2>0"
      by (smt (verit) ‹0 < e1› e2_def infdist_eq_setdist infdist_pos_not_in_closed that)
    moreover have "x = y" if "x\insert a S" "y\insert a S" "dist x y < e2" for x y
    proof (cases "x=a \ y=a")
      case True then show ?thesis
        by (smt (verit, best) dist_commute e2_def infdist_eq_setdist infdist_le insertE that)
    next
      case False then show ?thesis
        using e1_dist e2_def that by force
    qed
    ultimately show ?thesis unfolding uniform_discrete_def by meson
  qed
  ultimately show ?thesis by auto
qed (simp add: subset_insertI uniform_discrete_subset)

lemma discrete_compact_finite_iff:
  fixes S :: "'a::t1_space set"
  shows "discrete S \ compact S \ finite S"
proof
  assume "finite S"
  then have "compact S" using finite_imp_compact by auto
  moreover have "discrete S"
    unfolding discrete_def using isolated_in_islimpt_iff islimpt_finite[OF ‹finite S›] by auto
  ultimately show "discrete S \ compact S" by auto
next
  assume "discrete S \ compact S"
  then show "finite S"
    by (meson discrete_def Heine_Borel_imp_Bolzano_Weierstrass isolated_in_islimpt_iff order_refl)
qed

lemma uniform_discrete_finite_iff:
  fixes S :: "'a::heine_borel set"
  shows "uniform_discrete S \ bounded S \ finite S"
proof
  assume "uniform_discrete S \ bounded S"
  then have "discrete S" "compact S"
    using uniform_discrete_imp_discrete uniform_discrete_imp_closed compact_eq_bounded_closed
    by auto
  then show "finite S" using discrete_compact_finite_iff by auto
next
  assume asm:"finite S"
  let ?thesis = "uniform_discrete S \ bounded S"
  have ?thesis when "S={}" using that by auto
  moreover have ?thesis when "S\{}"
  proof -
    have "\x. \d>0. \y\S. y \ x \ d \ dist x y"
      using finite_set_avoid[OF ‹finite S›] by auto
    then obtain f where f_pos:"f x>0"
        and f_dist: "\y\S. y \ x \ f x \ dist x y"
        if "x\S" for x
      by metis
    define f_min where "f_min \ Min (f ` S)"
    have "f_min > 0"
      unfolding f_min_def
      by (simp add: asm f_pos that)
    moreover have "\x\S. \y\S. f_min > dist x y \ x=y"
      using f_dist unfolding f_min_def
      by (metis Min_le asm finite_imageI imageI le_less_trans linorder_not_less)
    ultimately have "uniform_discrete S"
      unfolding uniform_discrete_def by auto
    moreover have "bounded S" using ‹finite S› by auto
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis by blast
qed

lemma uniform_discrete_image_scale:
  assumes "uniform_discrete S" and dist:"\x\S. \y\S. dist x y = c * dist (f x) (f y)"
  shows "uniform_discrete (f ` S)"
proof -
  have ?thesis when "S={}" using that by auto
  moreover have ?thesis when "S\{}" "c\0"
  proof -
    obtain x1 where "x1\S" using ‹S≠{}› by auto
    have ?thesis when "S-{x1} = {}"
      using ‹x1 ∈ S› subset_antisym that uniform_discrete_insert by fastforce
    moreover have ?thesis when "S-{x1} \ {}"
    proof -
      obtain x2 where "x2\S-{x1}" using ‹S-{x1} ≠ {}› by auto
      then have "x2\S" "x1\x2" by auto
      then have "dist x1 x2 > 0" by auto
      moreover have "dist x1 x2 = c * dist (f x1) (f x2)"
        by (simp add: ‹x1 ∈ S› ‹x2 ∈ S› dist)
      moreover have "dist (f x2) (f x2) \ 0" by auto
      ultimately have False using ‹c≤0› by (simp add: zero_less_mult_iff)
      then show ?thesis by auto
    qed
    ultimately show ?thesis by auto
  qed
  moreover have ?thesis when "S\{}" "c>0"
  proof -
    obtain e1 where "e1>0" and e1_dist:"\x\S. \y\S. dist y x < e1 \ y = x"
      using ‹uniform_discrete S› unfolding uniform_discrete_def by auto
    define e where "e \ e1/c"
    have "x1 = x2" when "x1 \ f ` S" "x2 \ f ` S" and d: "dist x1 x2 < e" for x1 x2
      by (smt (verit) ‹0 < c› d dist divide_right_mono e1_dist e_def imageE nonzero_mult_div_cancel_left that)
    moreover have "e>0" using ‹e1>0› ‹c>0› unfolding e_def by auto
    ultimately show ?thesis unfolding uniform_discrete_def by meson
  qed
  ultimately show ?thesis by fastforce
qed

definition sparse :: "real \ 'a :: metric_space set \ bool"
  where "sparse \ X \ (\x\X. \y\X-{x}. dist x y > \)"

lemma sparse_empty [simp, intro]: "sparse \ {}"
  by (auto simp: sparse_def)

lemma sparseI [intro?]:
  "(\x y. x \ X \ y \ X \ x \ y \ dist x y > \) \ sparse \ X"
  unfolding sparse_def by auto

lemma sparseD:
  "sparse \ X \ x \ X \ y \ X \ x \ y \ dist x y > \"
  unfolding sparse_def by auto

lemma sparseD':
  "sparse \ X \ x \ X \ y \ X \ dist x y \ \ \ x = y"
  unfolding sparse_def by force

lemma sparse_singleton [simp, intro]: "sparse \ {x}"
  by (auto simp: sparse_def)

definition setdist_gt where "setdist_gt \ X Y \ (\x\X. \y\Y. dist x y > \)"

lemma setdist_gt_empty [simp]: "setdist_gt \ {} Y" "setdist_gt \ X {}"
  by (auto simp: setdist_gt_def)

lemma setdist_gtI: "(\x y. x \ X \ y \ Y \ dist x y > \) \ setdist_gt \ X Y"
  unfolding setdist_gt_def by auto

lemma setdist_gtD: "setdist_gt \ X Y \ x \ X \ y \ Y \ dist x y > \"
  unfolding setdist_gt_def by auto 

lemma setdist_gt_setdist: "\ < setdist A B \ setdist_gt \ A B"
  unfolding setdist_gt_def using setdist_le_dist by fastforce

lemma setdist_gt_mono: "setdist_gt \' A B \ \ \ \' \ A' \ A \ B' \ B \ setdist_gt \ A' B'"
  by (force simp: setdist_gt_def)
  
lemma setdist_gt_Un_left: "setdist_gt \ (A \ B) C \ setdist_gt \ A C \ setdist_gt \ B C"
  by (auto simp: setdist_gt_def)

lemma setdist_gt_Un_right: "setdist_gt \ C (A \ B) \ setdist_gt \ C A \ setdist_gt \ C B"
  by (auto simp: setdist_gt_def)
  
lemma compact_closed_imp_eventually_setdist_gt_at_right_0:
  assumes "compact A" "closed B" "A \ B = {}"
  shows   "eventually (\\. setdist_gt \ A B) (at_right 0)"
proof (cases "A = {} \ B = {}")
  case False
  hence "setdist A B > 0"
    by (metis IntI assms empty_iff in_closed_iff_infdist_zero order_less_le setdist_attains_inf setdist_pos_le setdist_sym)
  hence "eventually (\\. \ < setdist A B) (at_right 0)"
    using eventually_at_right_field by blast
  thus ?thesis
    by eventually_elim (auto intro: setdist_gt_setdist)
qed auto 

lemma setdist_gt_symI: "setdist_gt \ A B \ setdist_gt \ B A"
  by (force simp: setdist_gt_def dist_commute)

lemma setdist_gt_sym: "setdist_gt \ A B \ setdist_gt \ B A"
  by (force simp: setdist_gt_def dist_commute)

lemma eventually_setdist_gt_at_right_0_mult_iff:
  assumes "c > 0"
  shows   "eventually (\\. setdist_gt (c * \) A B) (at_right 0) \
             eventually (λε. setdist_gt ε A B) (at_right 0)"
proof -
  have "eventually (\\. setdist_gt (c * \) A B) (at_right 0) \
        eventually (λε. setdist_gt ε A B) (filtermap ((*) c) (at_right 0))"
    by (simp add: eventually_filtermap)
  also have "filtermap ((*) c) (at_right 0) = at_right 0"
    by (subst filtermap_times_pos_at_right) (use assms in auto)
  finally show ?thesis .
qed

lemma uniform_discrete_imp_sparse:
  assumes "uniform_discrete X"
  shows   "X sparse_in A"
  using assms unfolding uniform_discrete_def sparse_in_ball_def
  by (auto simp: discrete_imp_not_islimpt)

end