src/HOL/Library/Going_To_Filter.thy
author wenzelm
Fri Jan 04 23:22:53 2019 +0100 (7 months ago)
changeset 69593 3dda49e08b9d
parent 68406 6beb45f6cf67
child 69597 ff784d5a5bfb
permissions -rw-r--r--
isabelle update -u control_cartouches;
     1 (*
     2   File:    Going_To_Filter.thy
     3   Author:  Manuel Eberl, TU M√ľnchen
     4 
     5   A filter describing the points x such that f(x) tends to some other filter.
     6 *)
     7 
     8 section \<open>The \<open>going_to\<close> filter\<close>
     9 
    10 theory Going_To_Filter
    11   imports Complex_Main
    12 begin
    13 
    14 definition going_to_within :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a set \<Rightarrow> 'a filter"
    15   ("(_)/ going'_to (_)/ within (_)" [1000,60,60] 60) where
    16   "f going_to F within A = inf (filtercomap f F) (principal A)"
    17 
    18 abbreviation going_to :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter"
    19     (infix "going'_to" 60)
    20     where "f going_to F \<equiv> f going_to F within UNIV"
    21 
    22 text \<open>
    23   The \<open>going_to\<close> filter is, in a sense, the opposite of \<^term>\<open>filtermap\<close>. 
    24   It corresponds to the intuition of, given a function $f: A \to B$ and a filter $F$ on the 
    25   range of $B$, looking at such values of $x$ that $f(x)$ approaches $F$. This can be 
    26   written as \<^term>\<open>f going_to F\<close>.
    27   
    28   A classic example is the \<^term>\<open>at_infinity\<close> filter, which describes the neigbourhood
    29   of infinity (i.\,e.\ all values sufficiently far away from the zero). This can also be written
    30   as \<^term>\<open>norm going_to at_top\<close>.
    31 
    32   Additionally, the \<open>going_to\<close> filter can be restricted with an optional `within' parameter.
    33   For instance, if one would would want to consider the filter of complex numbers near infinity
    34   that do not lie on the negative real line, one could write 
    35   \<^term>\<open>norm going_to at_top within - complex_of_real ` {..0}\<close>.
    36 
    37   A third, less mathematical example lies in the complexity analysis of algorithms.
    38   Suppose we wanted to say that an algorithm on lists takes $O(n^2)$ time where $n$ is 
    39   the length of the input list. We can write this using the Landau symbols from the AFP,
    40   where the underlying filter is \<^term>\<open>length going_to at_top\<close>. If, on the other hand,
    41   we want to look the complexity of the algorithm on sorted lists, we could use the filter
    42   \<^term>\<open>length going_to at_top within {xs. sorted xs}\<close>.
    43 \<close>
    44 
    45 lemma going_to_def: "f going_to F = filtercomap f F"
    46   by (simp add: going_to_within_def)
    47 
    48 lemma eventually_going_toI [intro]: 
    49   assumes "eventually P F"
    50   shows   "eventually (\<lambda>x. P (f x)) (f going_to F)"
    51   using assms by (auto simp: going_to_def)
    52 
    53 lemma filterlim_going_toI_weak [intro]: "filterlim f F (f going_to F within A)"
    54   unfolding going_to_within_def
    55   by (meson filterlim_filtercomap filterlim_iff inf_le1 le_filter_def)
    56 
    57 lemma going_to_mono: "F \<le> G \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f going_to F within A \<le> f going_to G within B"
    58   unfolding going_to_within_def by (intro inf_mono filtercomap_mono) simp_all
    59 
    60 lemma going_to_inf: 
    61   "f going_to (inf F G) within A = inf (f going_to F within A) (f going_to G within A)"
    62   by (simp add: going_to_within_def filtercomap_inf inf_assoc inf_commute inf_left_commute)
    63 
    64 lemma going_to_sup: 
    65   "f going_to (sup F G) within A \<ge> sup (f going_to F within A) (f going_to G within A)"
    66   by (auto simp: going_to_within_def intro!: inf.coboundedI1 filtercomap_sup filtercomap_mono)
    67 
    68 lemma going_to_top [simp]: "f going_to top within A = principal A"
    69   by (simp add: going_to_within_def)
    70     
    71 lemma going_to_bot [simp]: "f going_to bot within A = bot"
    72   by (simp add: going_to_within_def)
    73     
    74 lemma going_to_principal: 
    75   "f going_to principal A within B = principal (f -` A \<inter> B)"
    76   by (simp add: going_to_within_def)
    77     
    78 lemma going_to_within_empty [simp]: "f going_to F within {} = bot"
    79   by (simp add: going_to_within_def)
    80 
    81 lemma going_to_within_union [simp]: 
    82   "f going_to F within (A \<union> B) = sup (f going_to F within A) (f going_to F within B)"
    83   by (simp add: going_to_within_def flip: inf_sup_distrib1)
    84 
    85 lemma eventually_going_to_at_top_linorder:
    86   fixes f :: "'a \<Rightarrow> 'b :: linorder"
    87   shows "eventually P (f going_to at_top within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x \<ge> C \<longrightarrow> P x)"
    88   unfolding going_to_within_def eventually_filtercomap 
    89     eventually_inf_principal eventually_at_top_linorder by fast
    90 
    91 lemma eventually_going_to_at_bot_linorder:
    92   fixes f :: "'a \<Rightarrow> 'b :: linorder"
    93   shows "eventually P (f going_to at_bot within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x \<le> C \<longrightarrow> P x)"
    94   unfolding going_to_within_def eventually_filtercomap 
    95     eventually_inf_principal eventually_at_bot_linorder by fast
    96 
    97 lemma eventually_going_to_at_top_dense:
    98   fixes f :: "'a \<Rightarrow> 'b :: {linorder,no_top}"
    99   shows "eventually P (f going_to at_top within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x > C \<longrightarrow> P x)"
   100   unfolding going_to_within_def eventually_filtercomap 
   101     eventually_inf_principal eventually_at_top_dense by fast
   102 
   103 lemma eventually_going_to_at_bot_dense:
   104   fixes f :: "'a \<Rightarrow> 'b :: {linorder,no_bot}"
   105   shows "eventually P (f going_to at_bot within A) \<longleftrightarrow> (\<exists>C. \<forall>x\<in>A. f x < C \<longrightarrow> P x)"
   106   unfolding going_to_within_def eventually_filtercomap 
   107     eventually_inf_principal eventually_at_bot_dense by fast
   108                
   109 lemma eventually_going_to_nhds:
   110   "eventually P (f going_to nhds a within A) \<longleftrightarrow> 
   111      (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>A. f x \<in> S \<longrightarrow> P x))"
   112   unfolding going_to_within_def eventually_filtercomap eventually_inf_principal
   113     eventually_nhds by fast
   114 
   115 lemma eventually_going_to_at:
   116   "eventually P (f going_to (at a within B) within A) \<longleftrightarrow> 
   117      (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>A. f x \<in> B \<inter> S - {a} \<longrightarrow> P x))"
   118   unfolding at_within_def going_to_inf eventually_inf_principal
   119             eventually_going_to_nhds going_to_principal by fast
   120 
   121 lemma norm_going_to_at_top_eq: "norm going_to at_top = at_infinity"
   122   by (simp add: eventually_at_infinity eventually_going_to_at_top_linorder filter_eq_iff)
   123 
   124 lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric]
   125 
   126 end