# Theory 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}))"

lemma nhdsin_degenerate [simp]: "a ∉ topspace X ⟹ nhdsin X a = bot"
and atin_degenerate [simp]: "a ∉ topspace X ⟹ atin X a = bot"

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)"
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)

lemma eventually_atin:
"eventually P (atin X a) ⟷ a ∉ topspace X ∨
(∃U. openin X U ∧ a ∈ U ∧ (∀x ∈ U - {a}. P x))"

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)"

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)"

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"

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"

lemma limitin_const_iff [simp]: "limitin X (λa. l) l F ⟷ l ∈ topspace X"

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))"

lemma limitin_sequentially_offset:
"limitin X f l sequentially ⟹ limitin X (λi. f (i + k)) l sequentially"
unfolding limitin_sequentially

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"
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"

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

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)"

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)"

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"])
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)"

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)"

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

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)"

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)"

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))"

lemma continuous_map_real_abs [continuous_intros]:
"continuous_map X euclideanreal f ⟹ continuous_map X euclideanreal (λx. abs(f x))"

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))"

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))"

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)"

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)"