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

eberlm@66488

83 
by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])

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
