summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Going_To_Filter.thy

author | wenzelm |

Tue May 15 13:57:39 2018 +0200 (16 months ago) | |

changeset 68189 | 6163c90694ef |

parent 67409 | 060efe532189 |

child 68406 | 6beb45f6cf67 |

permissions | -rw-r--r-- |

tuned headers;

1 (*

2 File: Going_To_Filter.thy

3 Author: Manuel Eberl, TU München

5 A filter describing the points x such that f(x) tends to some other filter.

6 *)

8 section \<open>The \<open>going_to\<close> filter\<close>

10 theory Going_To_Filter

11 imports Complex_Main

12 begin

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

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"

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"}.

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"}.

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}"}.

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>

45 lemma going_to_def: "f going_to F = filtercomap f F"

46 by (simp add: going_to_within_def)

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)

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)

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

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)

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)

68 lemma going_to_top [simp]: "f going_to top within A = principal A"

69 by (simp add: going_to_within_def)

71 lemma going_to_bot [simp]: "f going_to bot within A = bot"

72 by (simp add: going_to_within_def)

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)

78 lemma going_to_within_empty [simp]: "f going_to F within {} = bot"

79 by (simp add: going_to_within_def)

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 inf_sup_distrib1 [symmetric])

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

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

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

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

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

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

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)

124 lemmas at_infinity_altdef = norm_going_to_at_top_eq [symmetric]

126 end