src/HOL/Library/Going_To_Filter.thy
 author Manuel Eberl 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