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