src/HOL/Library/Going_To_Filter.thy
 author haftmann Wed Jul 18 20:51:21 2018 +0200 (11 months ago) changeset 68658 16cc1161ad7f parent 68406 6beb45f6cf67 child 69593 3dda49e08b9d permissions -rw-r--r--
tuned equation
     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 filtermap}.

    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 "f going_to F"}.

    27

    28   A classic example is the @{term "at_infinity"} 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 "norm going_to at_top"}.

    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 "norm going_to at_top within - complex_of_real  {..0}"}.

    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 "length going_to at_top"}. 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 "length going_to at_top within {xs. sorted xs}"}.

    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
`