Theory Going_To_Filter

(*
  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 termfiltermap. 
  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 termf going_to F.
  
  A classic example is the termat_infinity filter, which describes the neigbourhood
  of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written
  as termnorm 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 
  termnorm 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 termlength 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
  termlength 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 flip: inf_sup_distrib1)

lemma eventually_going_to_at_top_linorder:
  fixes f :: "'a  'b :: linorder"
  shows "eventually P (f going_to at_top within A)  (C. xA. 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. xA. 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. xA. 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. xA. 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  (xA. 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  (xA. 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