author | blanchet |
Thu, 28 Aug 2014 07:30:16 +0200 | |
changeset 58066 | 96e987003a01 |
parent 56544 | b60d5d119489 |
child 58881 | b9556a055632 |
permissions | -rw-r--r-- |
31381 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
4 |
header {* Comparing growth of functions on natural numbers by a preorder relation *} |
|
5 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
6 |
theory Function_Growth |
51542 | 7 |
imports Main Preorder Discrete |
31381 | 8 |
begin |
9 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
10 |
subsection {* Motivation *} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
11 |
|
31381 | 12 |
text {* |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
13 |
When comparing growth of functions in computer science, it is common to adhere |
51264 | 14 |
on Landau Symbols (``O-Notation''). However these come at the cost of notational |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
15 |
oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
16 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
17 |
Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood, |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
18 |
Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225). |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
19 |
We establish a quasi order relation @{text "\<lesssim>"} on functions such that |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
20 |
@{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}. From a didactic point of view, this does not only |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
21 |
avoid the notational oddities mentioned above but also emphasizes the key insight |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
22 |
of a growth hierachy of functions: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
23 |
@{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}. |
31381 | 24 |
*} |
25 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
26 |
subsection {* Model *} |
31381 | 27 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
28 |
text {* |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
29 |
Our growth functions are of type @{text "\<nat> \<Rightarrow> \<nat>"}. This is different |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
30 |
to the usual conventions for Landau symbols for which @{text "\<real> \<Rightarrow> \<real>"} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
31 |
would be appropriate, but we argue that @{text "\<real> \<Rightarrow> \<real>"} is more |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
32 |
appropriate for analysis, whereas our setting is discrete. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
33 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
34 |
Note that we also restrict the additional coefficients to @{text \<nat>}, something |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
35 |
we discuss at the particular definitions. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
36 |
*} |
31381 | 37 |
|
38 |
subsection {* The @{text "\<lesssim>"} relation *} |
|
39 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
40 |
definition less_eq_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<lesssim>" 50) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
41 |
where |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
42 |
"f \<lesssim> g \<longleftrightarrow> (\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m)" |
31381 | 43 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
44 |
text {* |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
45 |
This yields @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}. Note that @{text c} is restricted to |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
46 |
@{text \<nat>}. This does not pose any problems since if @{text "f \<in> O(g)"} holds for |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
47 |
a @{text "c \<in> \<real>"}, it also holds for @{text "\<lceil>c\<rceil> \<in> \<nat>"} by transitivity. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
48 |
*} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
49 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
50 |
lemma less_eq_funI [intro?]: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
51 |
assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" |
31381 | 52 |
shows "f \<lesssim> g" |
53 |
unfolding less_eq_fun_def by (rule assms) |
|
54 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
55 |
lemma not_less_eq_funI: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
56 |
assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m" |
31381 | 57 |
shows "\<not> f \<lesssim> g" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
58 |
using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast |
31381 | 59 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
60 |
lemma less_eq_funE [elim?]: |
31381 | 61 |
assumes "f \<lesssim> g" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
62 |
obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m" |
31381 | 63 |
using assms unfolding less_eq_fun_def by blast |
64 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
65 |
lemma not_less_eq_funE: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
66 |
assumes "\<not> f \<lesssim> g" and "c > 0" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
67 |
obtains m where "m > n" and "c * g m < f m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
68 |
using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast |
31381 | 69 |
|
70 |
||
71 |
subsection {* The @{text "\<approx>"} relation, the equivalence relation induced by @{text "\<lesssim>"} *} |
|
72 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
73 |
definition equiv_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<cong>" 50) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
74 |
where |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
75 |
"f \<cong> g \<longleftrightarrow> |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
76 |
(\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m)" |
31381 | 77 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
78 |
text {* |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
79 |
This yields @{text "f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)"}. Concerning @{text "c\<^sub>1"} and @{text "c\<^sub>2"} |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
80 |
restricted to @{typ nat}, see note above on @{text "(\<lesssim>)"}. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
81 |
*} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
82 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
83 |
lemma equiv_funI [intro?]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
84 |
assumes "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. \<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
31381 | 85 |
shows "f \<cong> g" |
86 |
unfolding equiv_fun_def by (rule assms) |
|
87 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
88 |
lemma not_equiv_funI: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
89 |
assumes "\<And>c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \<Longrightarrow> c\<^sub>2 > 0 \<Longrightarrow> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
90 |
\<exists>m>n. c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m" |
31381 | 91 |
shows "\<not> f \<cong> g" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
92 |
using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast |
31381 | 93 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
94 |
lemma equiv_funE [elim?]: |
31381 | 95 |
assumes "f \<cong> g" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
96 |
obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
97 |
and "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
31381 | 98 |
using assms unfolding equiv_fun_def by blast |
99 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
100 |
lemma not_equiv_funE: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
101 |
fixes n c\<^sub>1 c\<^sub>2 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
102 |
assumes "\<not> f \<cong> g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
103 |
obtains m where "m > n" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
104 |
and "c\<^sub>1 * f m < g m \<or> c\<^sub>2 * g m < f m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
105 |
using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast |
31381 | 106 |
|
107 |
||
108 |
subsection {* The @{text "\<prec>"} relation, the strict part of @{text "\<lesssim>"} *} |
|
109 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
110 |
definition less_fun :: "(nat \<Rightarrow> nat) \<Rightarrow> (nat \<Rightarrow> nat) \<Rightarrow> bool" (infix "\<prec>" 50) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
111 |
where |
31381 | 112 |
"f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f" |
113 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
114 |
lemma less_funI: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
115 |
assumes "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
116 |
and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m" |
31381 | 117 |
shows "f \<prec> g" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
118 |
using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
119 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
120 |
lemma not_less_funI: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
121 |
assumes "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * g m < f m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
122 |
and "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
123 |
shows "\<not> f \<prec> g" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
124 |
using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
125 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
126 |
lemma less_funE [elim?]: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
127 |
assumes "f \<prec> g" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
128 |
obtains n c where "c > 0" and "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
129 |
and "\<And>c n. c > 0 \<Longrightarrow> \<exists>m>n. c * f m < g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
130 |
proof - |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
131 |
from assms have "f \<lesssim> g" and "\<not> g \<lesssim> f" by (simp_all add: less_fun_def) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
132 |
from `f \<lesssim> g` obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
133 |
by (rule less_eq_funE) blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
134 |
{ fix c n :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
135 |
assume "c > 0" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
136 |
with `\<not> g \<lesssim> f` obtain m where "m > n" "c * f m < g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
137 |
by (rule not_less_eq_funE) blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
138 |
then have **: "\<exists>m>n. c * f m < g m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
139 |
} note ** = this |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
140 |
from * ** show thesis by (rule that) |
31381 | 141 |
qed |
142 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
143 |
lemma not_less_funE: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
144 |
assumes "\<not> f \<prec> g" and "c > 0" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
145 |
obtains m where "m > n" and "c * g m < f m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
146 |
| d q where "\<And>m. d > 0 \<Longrightarrow> m > q \<Longrightarrow> g q \<le> d * f q" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
147 |
using assms unfolding less_fun_def linorder_not_less [symmetric] by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
148 |
|
31381 | 149 |
text {* |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
150 |
I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}. Maybe this only |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
151 |
holds if @{text f} and/or @{text g} are of a certain class of functions. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
152 |
However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
153 |
handy introduction rule. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
154 |
|
51264 | 155 |
Note that D. Knuth ignores @{text o} altogether. So what \dots |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
156 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
157 |
Something still has to be said about the coefficient @{text c} in |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
158 |
the definition of @{text "(\<prec>)"}. In the typical definition of @{text o}, |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
159 |
it occurs on the \emph{right} hand side of the @{text "(>)"}. The reason |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
160 |
is that the situation is dual to the definition of @{text O}: the definition |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
161 |
works since @{text c} may become arbitrary small. Since this is not possible |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
162 |
within @{term \<nat>}, we push the coefficient to the left hand side instead such |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
163 |
that it become arbitrary big instead. |
31381 | 164 |
*} |
165 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
166 |
lemma less_fun_strongI: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
167 |
assumes "\<And>c. c > 0 \<Longrightarrow> \<exists>n. \<forall>m>n. c * f m < g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
168 |
shows "f \<prec> g" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
169 |
proof (rule less_funI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
170 |
have "1 > (0::nat)" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
171 |
from assms `1 > 0` have "\<exists>n. \<forall>m>n. 1 * f m < g m" . |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
172 |
then obtain n where *: "\<And>m. m > n \<Longrightarrow> 1 * f m < g m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
173 |
have "\<forall>m>n. f m \<le> 1 * g m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
174 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
175 |
fix m |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
176 |
assume "m > n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
177 |
with * have "1 * f m < g m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
178 |
then show "f m \<le> 1 * g m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
179 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
180 |
with `1 > 0` show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
181 |
fix c n :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
182 |
assume "c > 0" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
183 |
with assms obtain q where "\<And>m. m > q \<Longrightarrow> c * f m < g m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
184 |
then have "c * f (Suc (q + n)) < g (Suc (q + n))" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
185 |
moreover have "Suc (q + n) > n" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
186 |
ultimately show "\<exists>m>n. c * f m < g m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
187 |
qed |
31381 | 188 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
189 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
190 |
subsection {* @{text "\<lesssim>"} is a preorder *} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
191 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
192 |
text {* This yields all lemmas relating @{text "\<lesssim>"}, @{text "\<prec>"} and @{text "\<cong>"}. *} |
31381 | 193 |
|
194 |
interpretation fun_order: preorder_equiv less_eq_fun less_fun |
|
195 |
where "preorder_equiv.equiv less_eq_fun = equiv_fun" |
|
196 |
proof - |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
197 |
interpret preorder: preorder_equiv less_eq_fun less_fun |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
198 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
199 |
fix f g h |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
200 |
show "f \<lesssim> f" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
201 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
202 |
have "\<exists>n. \<forall>m>n. f m \<le> 1 * f m" by auto |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
203 |
then show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * f m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
204 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
205 |
show "f \<prec> g \<longleftrightarrow> f \<lesssim> g \<and> \<not> g \<lesssim> f" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
206 |
by (fact less_fun_def) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
207 |
assume "f \<lesssim> g" and "g \<lesssim> h" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
208 |
show "f \<lesssim> h" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
209 |
proof |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
210 |
from `f \<lesssim> g` obtain n\<^sub>1 c\<^sub>1 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
211 |
where "c\<^sub>1 > 0" and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
212 |
by rule blast |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
213 |
from `g \<lesssim> h` obtain n\<^sub>2 c\<^sub>2 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
214 |
where "c\<^sub>2 > 0" and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * h m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
215 |
by rule blast |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
216 |
have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
217 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
218 |
fix m |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
219 |
assume Q: "m > max n\<^sub>1 n\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
220 |
from P\<^sub>1 Q have *: "f m \<le> c\<^sub>1 * g m" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
221 |
from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * h m" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
222 |
with `c\<^sub>1 > 0` have "c\<^sub>1 * g m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
223 |
with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans) |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
224 |
qed |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
225 |
then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule |
56544 | 226 |
moreover from `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "c\<^sub>1 * c\<^sub>2 > 0" by simp |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
227 |
ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
228 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
229 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
230 |
from preorder.preorder_equiv_axioms show "class.preorder_equiv less_eq_fun less_fun" . |
31381 | 231 |
show "preorder_equiv.equiv less_eq_fun = equiv_fun" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
232 |
proof (rule ext, rule ext, unfold preorder.equiv_def) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
233 |
fix f g |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
234 |
show "f \<lesssim> g \<and> g \<lesssim> f \<longleftrightarrow> f \<cong> g" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
235 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
236 |
assume "f \<cong> g" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
237 |
then obtain n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
238 |
and *: "\<And>m. m > n \<Longrightarrow> f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
239 |
by rule blast |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
240 |
have "\<forall>m>n. f m \<le> c\<^sub>1 * g m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
241 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
242 |
fix m |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
243 |
assume "m > n" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
244 |
with * show "f m \<le> c\<^sub>1 * g m" by simp |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
245 |
qed |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
246 |
with `c\<^sub>1 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * g m" by blast |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
247 |
then have "f \<lesssim> g" .. |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
248 |
have "\<forall>m>n. g m \<le> c\<^sub>2 * f m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
249 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
250 |
fix m |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
251 |
assume "m > n" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
252 |
with * show "g m \<le> c\<^sub>2 * f m" by simp |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
253 |
qed |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
254 |
with `c\<^sub>2 > 0` have "\<exists>c>0. \<exists>n. \<forall>m>n. g m \<le> c * f m" by blast |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
255 |
then have "g \<lesssim> f" .. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
256 |
from `f \<lesssim> g` and `g \<lesssim> f` show "f \<lesssim> g \<and> g \<lesssim> f" .. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
257 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
258 |
assume "f \<lesssim> g \<and> g \<lesssim> f" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
259 |
then have "f \<lesssim> g" and "g \<lesssim> f" by auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
260 |
from `f \<lesssim> g` obtain n\<^sub>1 c\<^sub>1 where "c\<^sub>1 > 0" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
261 |
and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
262 |
from `g \<lesssim> f` obtain n\<^sub>2 c\<^sub>2 where "c\<^sub>2 > 0" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
263 |
and P\<^sub>2: "\<And>m. m > n\<^sub>2 \<Longrightarrow> g m \<le> c\<^sub>2 * f m" by rule blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
264 |
have "\<forall>m>max n\<^sub>1 n\<^sub>2. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
265 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
266 |
fix m |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
267 |
assume Q: "m > max n\<^sub>1 n\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
268 |
from P\<^sub>1 Q have "f m \<le> c\<^sub>1 * g m" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
269 |
moreover from P\<^sub>2 Q have "g m \<le> c\<^sub>2 * f m" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
270 |
ultimately show "f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" .. |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
271 |
qed |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
272 |
with `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "\<exists>c\<^sub>1>0. \<exists>c\<^sub>2>0. \<exists>n. |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
273 |
\<forall>m>n. f m \<le> c\<^sub>1 * g m \<and> g m \<le> c\<^sub>2 * f m" by blast |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
274 |
then show "f \<cong> g" .. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
275 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
276 |
qed |
31381 | 277 |
qed |
278 |
||
279 |
||
280 |
subsection {* Simple examples *} |
|
281 |
||
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
282 |
text {* |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
283 |
Most of these are left as constructive exercises for the reader. Note that additional |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
284 |
preconditions to the functions may be necessary. The list here is by no means to be |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
285 |
intended as complete contruction set for typical functions, here surely something |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
286 |
has to be added yet. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
287 |
*} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
288 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
289 |
text {* @{prop "(\<lambda>n. f n + k) \<cong> f"} *} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
290 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
291 |
text {* @{prop "(\<lambda>n. Suc k * f n) \<cong> f"} *} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
292 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
293 |
lemma "f \<lesssim> (\<lambda>n. f n + g n)" |
51264 | 294 |
by rule auto |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
295 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
296 |
lemma "(\<lambda>_. 0) \<prec> (\<lambda>n. Suc k)" |
51264 | 297 |
by (rule less_fun_strongI) auto |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
298 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
299 |
lemma "(\<lambda>_. k) \<prec> Discrete.log" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
300 |
proof (rule less_fun_strongI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
301 |
fix c :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
302 |
have "\<forall>m>2 ^ (Suc (c * k)). c * k < Discrete.log m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
303 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
304 |
fix m :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
305 |
assume "2 ^ Suc (c * k) < m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
306 |
then have "2 ^ Suc (c * k) \<le> m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
307 |
with log_mono have "Discrete.log (2 ^ (Suc (c * k))) \<le> Discrete.log m" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
308 |
by (blast dest: monoD) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
309 |
moreover have "c * k < Discrete.log (2 ^ (Suc (c * k)))" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
310 |
ultimately show "c * k < Discrete.log m" by auto |
31381 | 311 |
qed |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
312 |
then show "\<exists>n. \<forall>m>n. c * k < Discrete.log m" .. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
313 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
314 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
315 |
text {* @{prop "Discrete.log \<prec> Discrete.sqrt"} *} |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
316 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
317 |
lemma "Discrete.sqrt \<prec> id" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
318 |
proof (rule less_fun_strongI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
319 |
fix c :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
320 |
assume "0 < c" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
321 |
have "\<forall>m>(Suc c)\<^sup>2. c * Discrete.sqrt m < id m" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
322 |
proof (rule allI, rule impI) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
323 |
fix m |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
324 |
assume "(Suc c)\<^sup>2 < m" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
325 |
then have "(Suc c)\<^sup>2 \<le> m" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
326 |
with mono_sqrt have "Discrete.sqrt ((Suc c)\<^sup>2) \<le> Discrete.sqrt m" by (rule monoE) |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
327 |
then have "Suc c \<le> Discrete.sqrt m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
328 |
then have "c < Discrete.sqrt m" by simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
329 |
moreover from `(Suc c)\<^sup>2 < m` have "Discrete.sqrt m > 0" by simp |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
330 |
ultimately have "c * Discrete.sqrt m < Discrete.sqrt m * Discrete.sqrt m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
331 |
also have "\<dots> \<le> m" by (simp add: power2_eq_square [symmetric]) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
332 |
finally show "c * Discrete.sqrt m < id m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
333 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
334 |
then show "\<exists>n. \<forall>m>n. c * Discrete.sqrt m < id m" .. |
31381 | 335 |
qed |
336 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51542
diff
changeset
|
337 |
lemma "id \<prec> (\<lambda>n. n\<^sup>2)" |
51264 | 338 |
by (rule less_fun_strongI) (auto simp add: power2_eq_square) |
31381 | 339 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
340 |
lemma "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. n ^ Suc k)" |
51264 | 341 |
by (rule less_fun_strongI) auto |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
342 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
343 |
text {* @{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"} *} |
31381 | 344 |
|
345 |
end |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
346 |