Theory HOL-Analysis.Abstract_Limits

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  (xS. 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  (xS. 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  (xT. 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 
          (xT. 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  (xT. 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 (smt (verit, best) 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  (xU - {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 "F b in F. f b  topspace X  S"
      by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
    with L show ?rhs
      apply (clarsimp simp add: limitin_def eventually_mono openin_subtopology_alt)
      apply (drule_tac x="S  U" in spec, force simp: elim: eventually_mono)
      done
  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. nN. f n  U" if U: "openin X U" "l  U" for U
  proof -
    obtain N where "n. nN  f (n + k)  U"
      using assms U unfolding limitin_sequentially by blast
    then have "nN+k. f n  U"
      by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
    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  (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
    apply (auto simp: continuous_map_def topcontinuous_at_def)
    by (smt (verit, del_insts) 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
  have "continuous_map X euclideanreal (λx. c * f x)  continuous_map X euclideanreal f"
    apply (frule continuous_map_real_mult_left [where c="inverse c"])
    apply (simp add: field_simps False)
    done
  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