66488
|
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 |
*)
|
67409
|
7 |
|
|
8 |
section \<open>The \<open>going_to\<close> filter\<close>
|
|
9 |
|
66488
|
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>
|
67409
|
23 |
The \<open>going_to\<close> filter is, in a sense, the opposite of @{term filtermap}.
|
66488
|
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 |
|
67409
|
32 |
Additionally, the \<open>going_to\<close> filter can be restricted with an optional `within' parameter.
|
66488
|
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)"
|
68406
|
83 |
by (simp add: going_to_within_def flip: inf_sup_distrib1)
|
66488
|
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
|