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