|
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 |