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