Quelle  Sparse_In.thy

theory Sparse_In 
  imports Homotopy

begin

(*TODO: can we remove the definition isolated_points_of from 
  HOL-Complex_Analysis.Complex_Singularities?*)
(*TODO: more lemmas between sparse_in and discrete?*)

subsection ‹A set of points sparse in another set›

definition sparse_in:: "'a :: topological_space set ==> 'a set ==> bool"
    (infixl ‹(sparse'_in)› 50)
  where
  "pts sparse_in A = (∀x∈A. ∃B. x∈B ∧ open B ∧ (∀y∈B. ¬ y islimpt pts))"

lemma sparse_in_empty[simp]: "{} sparse_in A"
  by (meson UNIV_I empty_iff islimpt_def open_UNIV sparse_in_def)

lemma finite_imp_sparse:
  fixes pts::"'a:: t1_space set"
  shows "finite pts ==> pts sparse_in S"
  by (meson UNIV_I islimpt_finite open_UNIV sparse_in_def)

lemma sparse_in_singleton[simp]: "{x} sparse_in (A::'a:: t1_space set)"
  by (rule finite_imp_sparse) auto

lemma sparse_in_ball_def:
  "pts sparse_in D ⟷ (∀x∈D. ∃e>0. ∀y∈ball x e. ¬ y islimpt pts)"
  unfolding sparse_in_def
  by (meson Elementary_Metric_Spaces.open_ball open_contains_ball_eq subset_eq)

lemma get_sparse_in_cover:
  assumes "pts sparse_in A"
  obtains B where "open B" "A ⊆ B" "∀y∈B. ¬ y islimpt pts"
proof -
  obtain getB where getB:"x∈getB x" "open (getB x)" "∀y∈getB x. ¬ y islimpt pts"
    if "x∈A" for x
    using assms(1) unfolding sparse_in_def by metis
  define B where "B = Union (getB ` A)"
  have "open B" unfolding B_def using getB(2) by blast
  moreover have "A ⊆ B" unfolding B_def using getB(1) by auto
  moreover have "∀y∈B. ¬ y islimpt pts" unfolding B_def by (meson UN_iff getB(3))
  ultimately show ?thesis using that by blast
qed

lemma sparse_in_open:
  assumes "open A"
  shows "pts sparse_in A ⟷ (∀y∈A. ¬y islimpt pts)"
  using assms unfolding sparse_in_def by auto

lemma sparse_in_not_in:
  assumes "pts sparse_in A" "x∈A"
  obtains B where "open B" "x∈B" "∀y∈B. y≠x ⟶ y∉pts"
  using assms unfolding sparse_in_def
  by (metis islimptI)

lemma sparse_in_subset:
  assumes "pts sparse_in A" "B ⊆ A"
  shows "pts sparse_in B"
  using assms unfolding sparse_in_def  by auto

lemma sparse_in_subset2:
  assumes "pts1 sparse_in D" "pts2 ⊆ pts1"
  shows "pts2 sparse_in D"
  by (meson assms(1) assms(2) islimpt_subset sparse_in_def)

lemma sparse_in_union:
  assumes "pts1 sparse_in D1" "pts2 sparse_in D1" 
  shows "(pts1 ∪ pts2) sparse_in (D1 ∩ D2)" 
  using assms unfolding sparse_in_def islimpt_Un
  by (metis Int_iff open_Int)

lemma sparse_in_union': "A sparse_in C ==> B sparse_in C ==> A ∪ B sparse_in C"
  using sparse_in_union[of A C B C] by simp

lemma sparse_in_Union_finite:
  assumes "(∧A'. A' ∈ A ==> A' sparse_in B)" "finite A"
  shows   "∪A sparse_in B"
  using assms(2,1) by (induction rule: finite_induct) (auto intro!: sparse_in_union')

lemma sparse_in_UN_finite:
  assumes "(∧x. x ∈ A ==> f x sparse_in B)" "finite A"
  shows   "(∪x∈A. f x) sparse_in B"
  by (rule sparse_in_Union_finite) (use assms in auto)

lemma sparse_in_compact_finite:
  assumes "pts sparse_in A" "compact A"
  shows "finite (A ∩ pts)"
  apply (rule finite_not_islimpt_in_compact[OF ‹compact A›])
  using assms unfolding sparse_in_def by blast

lemma sparse_imp_closedin_pts:
  assumes "pts sparse_in D" 
  shows "closedin (top_of_set D) (D ∩ pts)"
  using assms islimpt_subset unfolding closedin_limpt sparse_in_def 
  by fastforce

lemma open_diff_sparse_pts:
  assumes "open D" "pts sparse_in D" 
  shows "open (D - pts)"
  using assms sparse_imp_closedin_pts
  by (metis Diff_Diff_Int Diff_cancel Diff_eq_empty_iff Diff_subset 
      closedin_def double_diff openin_open_eq topspace_euclidean_subtopology)

lemma sparse_in_UNIV_imp_closed: "X sparse_in UNIV ==> closed X"
  by (simp add: Compl_eq_Diff_UNIV closed_open open_diff_sparse_pts)


lemma sparse_imp_countable:
  fixes D::"'a ::euclidean_space set"
  assumes  "open D" "pts sparse_in D"
  shows "countable (D ∩ pts)"
proof -
  obtain K :: "nat ==> 'a ::euclidean_space set"
      where K: "D = (∪n. K n)" "∧n. compact (K n)"
    using assms  by (metis open_Union_compact_subsets)
  then have "D∩ pts = (∪n. K n ∩ pts)"
    by blast
  moreover have "∧n. finite (K n ∩ pts)"
    by (metis K(1) K(2) Union_iff assms(2) rangeI 
        sparse_in_compact_finite sparse_in_subset subsetI)
  ultimately show ?thesis
    by (metis countableI_type countable_UN countable_finite)
qed

lemma sparse_imp_connected:
  fixes D::"'a ::euclidean_space set"
  assumes  "2 ≤ DIM ('a)"  "connected D" "open D" "pts sparse_in D"
  shows "connected (D - pts)"
  using assms
  by (metis Diff_Compl Diff_Diff_Int Diff_eq connected_open_diff_countable 
      sparse_imp_countable)

lemma sparse_in_eventually_iff:
  assumes "open A"
  shows "pts sparse_in A ⟷ (∀y∈A. (∀🪙F y in at y. y ∉ pts))"
  unfolding sparse_in_open[OF ‹open A›] islimpt_iff_eventually
  by simp

lemma get_sparse_from_eventually:
  fixes A::"'a::topological_space set"
  assumes "∀x∈A. ∀🪙F z in at x. P z" "open A"
  obtains pts where "pts sparse_in A" "∀x∈A - pts. P x"
proof -
  define pts::"'a set" where "pts={x. ¬P x}"
  have "pts sparse_in A" "∀x∈A - pts. P x"
    unfolding sparse_in_eventually_iff[OF ‹open A›] pts_def
    using assms(1) by simp_all
  then show ?thesis using that by blast
qed

lemma sparse_disjoint:
  assumes "pts ∩ A = {}" "open A"
  shows "pts sparse_in A"
  using assms unfolding sparse_in_eventually_iff[OF ‹open A›]
      eventually_at_topological
  by blast

lemma sparse_in_translate:
  fixes A B :: "'a :: real_normed_vector set"
  assumes "A sparse_in B"
  shows   "(+) c ` A sparse_in (+) c ` B"
  unfolding sparse_in_def
proof safe
  fix x assume "x ∈ B"
  from get_sparse_in_cover[OF assms] obtain B' where B': "open B'" "B ⊆ B'" "∀y∈B'. ¬y islimpt A"
    by blast
  have "c + x ∈ (+) c ` B'" "open ((+) c ` B')"
    using B' ‹x ∈ B› by (auto intro: open_translation)
  moreover have "∀y∈(+) c ` B'. ¬y islimpt ((+) c ` A)"
  proof safe
    fix y assume y: "y ∈ B'" "c + y islimpt (+) c ` A"
    have "(-c) + (c + y) islimpt (+) (-c) ` (+) c ` A"
      by (intro islimpt_isCont_image[OF y(2)] continuous_intros)
         (auto simp: algebra_simps eventually_at_topological)
    hence "y islimpt A"
      by (simp add: image_image)
    with y(1) B' show False
      by blast
  qed
  ultimately show "∃B. c + x ∈ B ∧ open B ∧ (∀y∈B. ¬ y islimpt (+) c ` A)"
    by metis
qed

lemma sparse_in_translate':
  fixes A B :: "'a :: real_normed_vector set"
  assumes "A sparse_in B" "C ⊆ (+) c ` B"
  shows   "(+) c ` A sparse_in C"
  using sparse_in_translate[OF assms(1)] assms(2) by (rule sparse_in_subset)

lemma sparse_in_translate_UNIV:
  fixes A B :: "'a :: real_normed_vector set"
  assumes "A sparse_in UNIV"
  shows   "(+) c ` A sparse_in UNIV"
  using assms by (rule sparse_in_translate') auto


subsection ‹Co-sparseness filter›

text ‹
  The co-sparseness filter allows us to talk about properties that hold on a given set except
  for an ``insignificant'' number of points that are sparse in that set.
 ›
lemma is_filter_cosparse: "is_filter (λP. {x. ¬P x} sparse_in A)"
proof (standard, goal_cases)
  case 1
  thus ?case by auto
next
  case (2 P Q)
  from sparse_in_union[OF this, of UNIV] show ?case
    by (auto simp: Un_def)
next
  case (3 P Q)
  from 3(2) show ?case
    by (rule sparse_in_subset2) (use 3(1) in auto)
qed  

definition cosparse :: "'a set ==> 'a :: topological_space filter" where
 "cosparse A = Abs_filter (λP. {x. ¬P x} sparse_in A)"

syntax
  "_eventually_cosparse" :: "pttrn => 'a set => bool => bool"  (‹(‹indent=3 notation=‹binder ∀≈›\›\🪙≈_∈_./ _)› [0, 0, 10] 10)
syntax_consts
  "_eventually_cosparse" == eventually
translations
  "∀🪙≈x∈A. P" == "CONST eventually (λx. P) (CONST cosparse A)"

syntax
  "_eventually_cosparse_UNIV" :: "pttrn => bool => bool"  (‹(‹indent=3 notation=‹binder ∀≈›\›\🪙≈_./ _)› [0, 10] 10)
syntax_consts
  "_eventually_cosparse_UNIV" == eventually
translations
  "∀🪙≈x. P" == "CONST eventually (λx. P) (CONST cosparse CONST UNIV)"

syntax
  "_qeventually_cosparse" :: "pttrn ==> bool ==> 'a ==> 'a"  (‹(‹indent=3 notation=‹binder ∀≈›\›\🪙≈_ | (_)./ _)› [0, 0, 10] 10)
syntax_consts
  "_qeventually_cosparse" == eventually
translations
  "∀🪙≈x|P. t" => "CONST eventually (λx. t) (CONST cosparse {x. P})"
print_translation ‹
  [(🍋‹eventually›,
›

lemma eventually_cosparse: "eventually P (cosparse A) ⟷ {x. ¬P x} sparse_in A"
  unfolding cosparse_def by (rule eventually_Abs_filter[OF is_filter_cosparse])

lemma eventually_not_in_cosparse:
  assumes "X sparse_in A"
  shows   "eventually (λx. x ∉ X) (cosparse A)"
  using assms by (auto simp: eventually_cosparse)

lemma eventually_cosparse_open_eq:
  "open A ==> eventually P (cosparse A) ⟷ (∀x∈A. eventually P (at x))"
  unfolding eventually_cosparse
  by (subst sparse_in_open) (auto simp: islimpt_conv_frequently_at frequently_def)

lemma eventually_cosparse_imp_eventually_at:
  "eventually P (cosparse A) ==> x ∈ A ==> eventually P (at x within B)"
  unfolding eventually_cosparse sparse_in_def islimpt_def eventually_at_topological 
  by fastforce

lemma eventually_in_cosparse:
  assumes "A ⊆ X" "open A"
  shows   "eventually (λx. x ∈ X) (cosparse A)"
proof -
  have "eventually (λx. x ∈ A) (cosparse A)"
    using assms by (auto simp: eventually_cosparse_open_eq intro: eventually_at_in_open')
  thus ?thesis
    by eventually_elim (use assms(1) in blast)
qed

lemma cosparse_eq_bot_iff: "cosparse A = bot ⟷ (∀x∈A. open {x})"
proof -
  have "cosparse A = bot ⟷ eventually (λ_. False) (cosparse A)"
    by (simp add: trivial_limit_def)
  also have "… ⟷ (∀x∈A. open {x})"
    unfolding eventually_cosparse sparse_in_def
    by (auto simp: islimpt_UNIV_iff)
  finally show ?thesis .
qed

lemma cosparse_empty [simp]: "cosparse {} = bot"
  by (rule filter_eqI) (auto simp: eventually_cosparse sparse_in_def)

lemma cosparse_eq_bot_iff' [simp]: "cosparse (A :: 'a :: perfect_space set) = bot ⟷ A = {}"
  by (auto simp: cosparse_eq_bot_iff not_open_singleton)

end