# Theory Going_To_Filter

theory Going_To_Filter
imports Complex_Main
(*
File:    Going_To_Filter.thy
Author:  Manuel Eberl, TU München

A filter describing the points x such that f(x) tends to some other filter.
*)
section ‹The going\_to' filter›
theory Going_To_Filter
imports Complex_Main
begin

definition going_to_within :: "('a ⇒ 'b) ⇒ 'b filter ⇒ 'a set ⇒ 'a filter"
("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where
"f going_to F within A = inf (filtercomap f F) (principal A)"

abbreviation going_to :: "('a ⇒ 'b) ⇒ 'b filter ⇒ 'a filter"
(infix "going'_to" 60)
where "f going_to F ≡ f going_to F within UNIV"

text ‹
The going\_to' filter is, in a sense, the opposite of @{term filtermap}.
It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the
range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be
written as @{term "f going_to F"}.

A classic example is the @{term "at_infinity"} filter, which describes the neigbourhood
of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written
as @{term "norm going_to at_top"}.

Additionally, the going\_to' filter can be restricted with an optional within' parameter.
For instance, if one would would want to consider the filter of complex numbers near infinity
that do not lie on the negative real line, one could write
@{term "norm going_to at_top within - complex_of_real  {..0}"}.

A third, less mathematical example lies in the complexity analysis of algorithms.
Suppose we wanted to say that an algorithm on lists takes $O(n^2)$ time where $n$ is
the length of the input list. We can write this using the Landau symbols from the AFP,
where the underlying filter is @{term "length going_to at_top"}. If, on the other hand,
we want to look the complexity of the algorithm on sorted lists, we could use the filter
@{term "length going_to at_top within {xs. sorted xs}"}.
›

lemma going_to_def: "f going_to F = filtercomap f F"
by (simp add: going_to_within_def)

lemma eventually_going_toI [intro]:
assumes "eventually P F"
shows   "eventually (λx. P (f x)) (f going_to F)"
using assms by (auto simp: going_to_def)

lemma filterlim_going_toI_weak [intro]: "filterlim f F (f going_to F within A)"
unfolding going_to_within_def
by (meson filterlim_filtercomap filterlim_iff inf_le1 le_filter_def)

lemma going_to_mono: "F ≤ G ⟹ A ⊆ B ⟹ f going_to F within A ≤ f going_to G within B"
unfolding going_to_within_def by (intro inf_mono filtercomap_mono) simp_all

lemma going_to_inf:
"f going_to (inf F G) within A = inf (f going_to F within A) (f going_to G within A)"
by (simp add: going_to_within_def filtercomap_inf inf_assoc inf_commute inf_left_commute)

lemma going_to_sup:
"f going_to (sup F G) within A ≥ sup (f going_to F within A) (f going_to G within A)"
by (auto simp: going_to_within_def intro!: inf.coboundedI1 filtercomap_sup filtercomap_mono)

lemma going_to_top [simp]: "f going_to top within A = principal A"
by (simp add: going_to_within_def)

lemma going_to_bot [simp]: "f going_to bot within A = bot"
by (simp add: going_to_within_def)

lemma going_to_principal:
"f going_to principal A within B = principal (f - A ∩ B)"
by (simp add: going_to_within_def)

lemma going_to_within_empty [simp]: "f going_to F within {} = bot"
by (simp add: going_to_within_def)

lemma going_to_within_union [simp]:
"f going_to F within (A ∪ B) = sup (f going_to F within A) (f going_to F within B)"
by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])

lemma eventually_going_to_at_top_linorder:
fixes f :: "'a ⇒ 'b :: linorder"
shows "eventually P (f going_to at_top within A) ⟷ (∃C. ∀x∈A. f x ≥ C ⟶ P x)"
unfolding going_to_within_def eventually_filtercomap
eventually_inf_principal eventually_at_top_linorder by fast

lemma eventually_going_to_at_bot_linorder:
fixes f :: "'a ⇒ 'b :: linorder"
shows "eventually P (f going_to at_bot within A) ⟷ (∃C. ∀x∈A. f x ≤ C ⟶ P x)"
unfolding going_to_within_def eventually_filtercomap
eventually_inf_principal eventually_at_bot_linorder by fast

lemma eventually_going_to_at_top_dense:
fixes f :: "'a ⇒ 'b :: {linorder,no_top}"
shows "eventually P (f going_to at_top within A) ⟷ (∃C. ∀x∈A. f x > C ⟶ P x)"
unfolding going_to_within_def eventually_filtercomap
eventually_inf_principal eventually_at_top_dense by fast

lemma eventually_going_to_at_bot_dense:
fixes f :: "'a ⇒ 'b :: {linorder,no_bot}"
shows "eventually P (f going_to at_bot within A) ⟷ (∃C. ∀x∈A. f x < C ⟶ P x)"
unfolding going_to_within_def eventually_filtercomap
eventually_inf_principal eventually_at_bot_dense by fast

lemma eventually_going_to_nhds:
"eventually P (f going_to nhds a within A) ⟷
(∃S. open S ∧ a ∈ S ∧ (∀x∈A. f x ∈ S ⟶ P x))"
unfolding going_to_within_def eventually_filtercomap eventually_inf_principal
eventually_nhds by fast

lemma eventually_going_to_at:
"eventually P (f going_to (at a within B) within A) ⟷
(∃S. open S ∧ a ∈ S ∧ (∀x∈A. f x ∈ B ∩ S - {a} ⟶ P x))"
unfolding at_within_def going_to_inf eventually_inf_principal
eventually_going_to_nhds going_to_principal by fast

lemma norm_going_to_at_top_eq: "norm going_to at_top = at_infinity"
by (simp add: eventually_at_infinity eventually_going_to_at_top_linorder filter_eq_iff)

lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric]

end