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 ∧ (∀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 (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 ∧ (∀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 "∀⇩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. ∀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 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