Quelle  Abstract_Limits.thy   Sprache: Isabelle

theory Abstract_Limits
  imports
    Abstract_Topology
begin

subsection‹nhdsin and atin›

definition nhdsin :: "'a topology \ 'a \ 'a filter"
  where "nhdsin X a =
           (if a ∈ topspace X then (INF S∈{S. openin X S ∧ a ∈ S}. principal S) else bot)"

definition atin_within :: "['a topology, 'a, 'a set] \ 'a filter"
  where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \ S - {a}))"

abbreviation atin :: "'a topology \ 'a \ 'a filter"
  where "atin X a \ atin_within X a UNIV"

lemma atin_def: "atin X a = inf (nhdsin X a) (principal (topspace X - {a}))"
  by (simp add: atin_within_def)

lemma nhdsin_degenerate [simp]: "a \ topspace X \ nhdsin X a = bot"
  and atin_degenerate [simp]: "a \ topspace X \ atin X a = bot"
  by (simp_all add: nhdsin_def atin_def)

lemma eventually_nhdsin:
  "eventually P (nhdsin X a) \ a \ topspace X \ (\S. openin X S \ a \ S \ (\x\S. P x))"
proof (cases "a \ topspace X")
  case True
  hence "nhdsin X a = (INF S\{S. openin X S \ a \ S}. principal S)"
    by (simp add: nhdsin_def)
  also have "eventually P \ \ (\S. openin X S \ a \ S \ (\x\S. P x))"
    using True by (subst eventually_INF_base) (auto simp: eventually_principal)
  finally show ?thesis using True by simp
qed auto

lemma eventually_atin_within:
  "eventually P (atin_within X a S) \ a \ topspace X \ (\T. openin X T \ a \ T \ (\x\T. x \ S \ x \ a \ P x))"
proof (cases "a \ topspace X")
  case True
  hence "eventually P (atin_within X a S) \
         (∃T. openin X T ∧ a ∈ T ∧
          (∀x∈T. x ∈ topspace X ∧ x ∈ S ∧ x ≠ a ⟶ P x))"
    by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
  also have "\ \ (\T. openin X T \ a \ T \ (\x\T. x \ S \ x \ a \ P x))"
    using openin_subset by (intro ex_cong) auto
  finally show ?thesis by (simp add: True)
qed (simp add: atin_within_def)

lemma eventually_atin:
  "eventually P (atin X a) \ a \ topspace X \
             (∃U. openin X U ∧ a ∈ U ∧ (∀x ∈ U - {a}. P x))"
  by (auto simp add: eventually_atin_within)

lemma nontrivial_limit_atin:
   "atin X a \ bot \ a \ X derived_set_of topspace X"
proof 
  assume L: "atin X a \ bot"
  then have "a \ topspace X"
    by (meson atin_degenerate)
  moreover have "\ openin X {a}"
    using L by (auto simp: eventually_atin trivial_limit_eq)
  ultimately
  show "a \ X derived_set_of topspace X"
    by (auto simp: derived_set_of_topspace)
next
  assume a: "a \ X derived_set_of topspace X"
  show "atin X a \ bot"
  proof
    assume "atin X a = bot"
    then have "eventually (\_. False) (atin X a)"
      by simp
    then show False
      by (metis a eventually_atin in_derived_set_of insertE insert_Diff)
  qed
qed

lemma eventually_atin_subtopology:
  assumes "a \ topspace X"
  shows "eventually P (atin (subtopology X S) a) \
    (a ∈ S ⟶ (∃U. openin (subtopology X S) U ∧ a ∈ U ∧ (∀x∈U - {a}. P x)))"
  using assms by (simp add: eventually_atin)

lemma eventually_within_imp:
   "eventually P (atin_within X a S) \ eventually (\x. x \ S \ P x) (atin X a)"
  by (auto simp add: eventually_atin_within eventually_atin)

lemma atin_subtopology_within:
  assumes "a \ S"
  shows "atin (subtopology X S) a = atin_within X a S"
proof -
  have "eventually P (atin (subtopology X S) a) \ eventually P (atin_within X a S)" for P
    unfolding eventually_atin eventually_atin_within openin_subtopology
    using assms by auto
  then show ?thesis
    by (meson le_filter_def order.eq_iff)
qed

lemma atin_subtopology_within_if:
  shows "atin (subtopology X S) a = (if a \ S then atin_within X a S else bot)"
  by (simp add: atin_subtopology_within)

lemma trivial_limit_atpointof_within:
   "trivial_limit(atin_within X a S) \
        (a ∉ X derived_set_of S)"
  by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)

lemma derived_set_of_trivial_limit:
   "a \ X derived_set_of S \ \ trivial_limit(atin_within X a S)"
  by (simp add: trivial_limit_atpointof_within)


subsection‹Limits in a topological space›

definition limitin :: "'a topology \ ('b \ 'a) \ 'a \ 'b filter \ bool" where
  "limitin X f l F \ l \ topspace X \ (\U. openin X U \ l \ U \ eventually (\x. f x \ U) F)"

lemma limit_within_subset:
   "\limitin X f l (atin_within Y a S); T \ S\ \ limitin X f l (atin_within Y a T)"
  by (smt (verit) eventually_atin_within limitin_def subset_eq)

lemma limitinD: "\limitin X f l F; openin X U; l \ U\ \ eventually (\x. f x \ U) F"
  by (simp add: limitin_def)

lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \ (f \ l) F"
  by (auto simp: limitin_def tendsto_def)

lemma limitin_topspace: "limitin X f l F \ l \ topspace X"
  by (simp add: limitin_def)

lemma limitin_const_iff [simp]: "limitin X (\a. l) l F \ l \ topspace X"
  by (simp add: limitin_def)

lemma limitin_const: "limitin euclidean (\a. l) l F"
  by simp

lemma limitin_eventually:
   "\l \ topspace X; eventually (\x. f x = l) F\ \ limitin X f l F"
  by (auto simp: limitin_def eventually_mono)

lemma limitin_subsequence:
   "\strict_mono r; limitin X f l sequentially\ \ limitin X (f \ r) l sequentially"
  unfolding limitin_def using eventually_subseq by fastforce

lemma limitin_subtopology:
  "limitin (subtopology X S) f l F
   ⟷ l ∈ S ∧ eventually (λa. f a ∈ S) F ∧ limitin X f l F" (is "?lhs = ?rhs")
proof (cases "l \ S \ topspace X")
  case True
  show ?thesis
  proof
    assume L: ?lhs
    with True
    have "\\<^sub>F b in F. f b \ topspace X \ S"
      by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
    moreover have "\U. \openin X U; l \ U\ \ \\<^sub>F x in F. f x \ S \ U"
      using limitinD [OF L] True openin_subtopology_Int2 by force
    ultimately show ?rhs
      using True by (auto simp: limitin_def eventually_conj_iff)
  next
    assume ?rhs
    then show ?lhs
      using eventually_elim2
      by (fastforce simp add: limitin_def openin_subtopology_alt)
  qed
qed (auto simp: limitin_def)


lemma limitin_canonical_iff_gen [simp]:
  assumes "open S"
  shows "limitin (top_of_set S) f l F \ (f \ l) F \ l \ S"
  using assms by (auto simp: limitin_subtopology tendsto_def)

lemma limitin_sequentially:
   "limitin X S l sequentially \
     l ∈ topspace X ∧ (∀U. openin X U ∧ l ∈ U ⟶ (∃N. ∀n. N ≤ n ⟶ S n ∈ U))"
  by (simp add: limitin_def eventually_sequentially)

lemma limitin_sequentially_offset:
   "limitin X f l sequentially \ limitin X (\i. f (i + k)) l sequentially"
  unfolding limitin_sequentially
  by (metis add.commute le_add2 order_trans)

lemma limitin_sequentially_offset_rev:
  assumes "limitin X (\i. f (i + k)) l sequentially"
  shows "limitin X f l sequentially"
proof -
  have "\N. \n\N. f n \ U" if U: "openin X U" "l \ U" for U
  proof -
    obtain N where "\n. n\N \ f (n + k) \ U"
      using assms U unfolding limitin_sequentially by blast
    then have "\n\N+k. f n \ U"
      by (metis add_leD2 add_le_imp_le_diff le_add_diff_inverse2)
    then show ?thesis ..
  qed
  with assms show ?thesis
    unfolding limitin_sequentially
    by simp
qed

lemma limitin_atin:
   "limitin Y f y (atin X x) \
        y ∈ topspace Y ∧
        (x ∈ topspace X
        ⟶ (∀V. openin Y V ∧ y ∈ V
                 ⟶ (∃U. openin X U ∧ x ∈ U ∧ f ` (U - {x}) ⊆ V)))"
  by (auto simp: limitin_def eventually_atin image_subset_iff)

lemma limitin_atin_self:
   "limitin Y f (f a) (atin X a) \
        f a ∈ topspace Y ∧
        (a ∈ topspace X
         ⟶ (∀V. openin Y V ∧ f a ∈ V
                  ⟶ (∃U. openin X U ∧ a ∈ U ∧ f ` U ⊆ V)))"
  unfolding limitin_atin by fastforce

lemma limitin_trivial:
   "\trivial_limit F; y \ topspace X\ \ limitin X f y F"
  by (simp add: limitin_def)

lemma limitin_transform_eventually:
   "\eventually (\x. f x = g x) F; limitin X f l F\ \ limitin X g l F"
  unfolding limitin_def using eventually_elim2 by fastforce

lemma continuous_map_limit:
  assumes "continuous_map X Y g" and f: "limitin X f l F"
  shows "limitin Y (g \ f) (g l) F"
proof -
  have "g l \ topspace Y"
    by (meson assms continuous_map f image_eqI in_mono limitin_def)
  moreover
  have "\U. \\V. openin X V \ l \ V \ (\\<^sub>F x in F. f x \ V); openin Y U; g l \ U\
            ==> ∀🚫F x in F. g (f x) ∈ U"
    using assms eventually_mono
    by (fastforce simp: limitin_def dest!: openin_continuous_map_preimage)
  ultimately show ?thesis
    using f by (fastforce simp add: limitin_def)
qed


subsection‹Pointwise continuity in topological spaces›

definition topcontinuous_at where
  "topcontinuous_at X Y f x \
     x ∈ topspace X ∧
     f ∈ topspace X → topspace Y ∧
     (∀V. openin Y V ∧ f x ∈ V
          ⟶ (∃U. openin X U ∧ x ∈ U ∧ (∀y ∈ U. f y ∈ V)))"

lemma topcontinuous_at_atin:
   "topcontinuous_at X Y f x \
        x ∈ topspace X ∧
        f ∈ topspace X → topspace Y ∧
        limitin Y f (f x) (atin X x)"
  unfolding topcontinuous_at_def
  by (fastforce simp add: limitin_atin)+

lemma continuous_map_eq_topcontinuous_at:
   "continuous_map X Y f \ (\x \ topspace X. topcontinuous_at X Y f x)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: continuous_map_def topcontinuous_at_def)
next
  assume R: ?rhs
  then show ?lhs
    unfolding continuous_map_def topcontinuous_at_def Pi_iff
    by (smt (verit, ccfv_threshold)  mem_Collect_eq openin_subopen openin_subset subset_eq)
qed

lemma continuous_map_atin:
   "continuous_map X Y f \ (\x \ topspace X. limitin Y f (f x) (atin X x))"
  by (auto simp: limitin_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)

lemma limitin_continuous_map:
   "\continuous_map X Y f; a \ topspace X; f a = b\ \ limitin Y f b (atin X a)"
  by (auto simp: continuous_map_atin)

lemma limit_continuous_map_within:
   "\continuous_map (subtopology X S) Y f; a \ S; a \ topspace X\
    ==> limitin Y f (f a) (atin_within X a S)"
  by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)


subsection‹Combining theorems for continuous functions into the reals›

lemma continuous_map_canonical_const [continuous_intros]:
   "continuous_map X euclidean (\x. c)"
  by simp

lemma continuous_map_real_mult [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g\
   ==> continuous_map X euclideanreal (λx. f x * g x)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_pow [continuous_intros]:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. f x ^ n)"
  by (induction n) (auto simp: continuous_map_real_mult)

lemma continuous_map_real_mult_left:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. c * f x)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_mult_left_eq:
   "continuous_map X euclideanreal (\x. c * f x) \ c = 0 \ continuous_map X euclideanreal f"
proof (cases "c = 0")
  case False
  { assume "continuous_map X euclideanreal (\x. c * f x)"
    then have "continuous_map X euclideanreal (\x. inverse c * (c * f x))"
      by (simp add: continuous_map_real_mult)
    then have "continuous_map X euclideanreal f"
      by (simp add: field_simps False) }
  with False show ?thesis
    using continuous_map_real_mult_left by blast
qed simp

lemma continuous_map_real_mult_right:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. f x * c)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_mult_right_eq:
   "continuous_map X euclideanreal (\x. f x * c) \ c = 0 \ continuous_map X euclideanreal f"
  by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)

lemma continuous_map_minus [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "continuous_map X euclidean f \ continuous_map X euclidean (\x. - f x)"
  by (simp add: continuous_map_atin tendsto_minus)

lemma continuous_map_minus_eq [simp]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "continuous_map X euclidean (\x. - f x) \ continuous_map X euclidean f"
  using continuous_map_minus add.inverse_inverse continuous_map_eq by fastforce

lemma continuous_map_add [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "\continuous_map X euclidean f; continuous_map X euclidean g\ \ continuous_map X euclidean (\x. f x + g x)"
  by (simp add: continuous_map_atin tendsto_add)

lemma continuous_map_diff [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "\continuous_map X euclidean f; continuous_map X euclidean g\ \ continuous_map X euclidean (\x. f x - g x)"
  by (simp add: continuous_map_atin tendsto_diff)

lemma continuous_map_norm [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "continuous_map X euclidean f \ continuous_map X euclidean (\x. norm(f x))"
  by (simp add: continuous_map_atin tendsto_norm)

lemma continuous_map_real_abs [continuous_intros]:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. abs(f x))"
  by (simp add: continuous_map_atin tendsto_rabs)

lemma continuous_map_real_max [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g\
   ==> continuous_map X euclideanreal (λx. max (f x) (g x))"
  by (simp add: continuous_map_atin tendsto_max)

lemma continuous_map_real_min [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g\
   ==> continuous_map X euclideanreal (λx. min (f x) (g x))"
  by (simp add: continuous_map_atin tendsto_min)

lemma continuous_map_sum [continuous_intros]:
  fixes f :: "'a\'b\'c::real_normed_vector"
  shows "\finite I; \i. i \ I \ continuous_map X euclidean (\x. f x i)\
         ==> continuous_map X euclidean (λx. sum (f x) I)"
  by (simp add: continuous_map_atin tendsto_sum)

lemma continuous_map_prod [continuous_intros]:
   "\finite I;
         ∧i. i ∈ I ==> continuous_map X euclideanreal (λx. f x i)]
        ==> continuous_map X euclideanreal (λx. prod (f x) I)"
  by (simp add: continuous_map_atin tendsto_prod)

lemma continuous_map_real_inverse [continuous_intros]:
   "\continuous_map X euclideanreal f; \x. x \ topspace X \ f x \ 0\
        ==> continuous_map X euclideanreal (λx. inverse(f x))"
  by (simp add: continuous_map_atin tendsto_inverse)

lemma continuous_map_real_divide [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g; \x. x \ topspace X \ g x \ 0\
   ==> continuous_map X euclideanreal (λx. f x / g x)"
  by (simp add: continuous_map_atin tendsto_divide)

end