author | paulson <lp15@cam.ac.uk> |
Tue, 01 Dec 2015 14:09:10 +0000 | |
changeset 61762 | d50b993b4fb9 |
parent 61585 | a9599d3d7610 |
child 61831 | c43f87119d80 |
permissions | -rw-r--r-- |
31381 | 1 |
|
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 |
51542 | 7 |
imports Main Preorder Discrete |
31381 | 8 |
begin |
9 |
||
60500 | 10 |
subsection \<open>Motivation\<close> |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
11 |
|
60500 | 12 |
text \<open> |
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 |
61585 | 15 |
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
|
16 |
|
59113 | 17 |
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
|
18 |
Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225). |
61585 | 19 |
We establish a quasi order relation \<open>\<lesssim>\<close> on functions such that |
20 |
\<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
|
21 |
avoid the notational oddities mentioned above but also emphasizes the key insight |
59113 | 22 |
of a growth hierarchy of functions: |
61585 | 23 |
\<open>(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>\<close>. |
60500 | 24 |
\<close> |
31381 | 25 |
|
60500 | 26 |
subsection \<open>Model\<close> |
31381 | 27 |
|
60500 | 28 |
text \<open> |
61585 | 29 |
Our growth functions are of type \<open>\<nat> \<Rightarrow> \<nat>\<close>. This is different |
30 |
to the usual conventions for Landau symbols for which \<open>\<real> \<Rightarrow> \<real>\<close> |
|
31 |
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
|
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 |
|
61585 | 34 |
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
|
35 |
we discuss at the particular definitions. |
60500 | 36 |
\<close> |
31381 | 37 |
|
61585 | 38 |
subsection \<open>The \<open>\<lesssim>\<close> relation\<close> |
31381 | 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 |
|
60500 | 44 |
text \<open> |
61585 | 45 |
This yields \<open>f \<lesssim> g \<longleftrightarrow> f \<in> O(g)\<close>. Note that \<open>c\<close> is restricted to |
46 |
\<open>\<nat>\<close>. This does not pose any problems since if \<open>f \<in> O(g)\<close> holds for |
|
47 |
a \<open>c \<in> \<real>\<close>, it also holds for \<open>\<lceil>c\<rceil> \<in> \<nat>\<close> by transitivity. |
|
60500 | 48 |
\<close> |
51263
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 |
||
61585 | 71 |
subsection \<open>The \<open>\<approx>\<close> relation, the equivalence relation induced by \<open>\<lesssim>\<close>\<close> |
31381 | 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 |
|
60500 | 78 |
text \<open> |
61585 | 79 |
This yields \<open>f \<cong> g \<longleftrightarrow> f \<in> \<Theta>(g)\<close>. Concerning \<open>c\<^sub>1\<close> and \<open>c\<^sub>2\<close> |
80 |
restricted to @{typ nat}, see note above on \<open>(\<lesssim>)\<close>. |
|
60500 | 81 |
\<close> |
51263
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 |
||
61585 | 108 |
subsection \<open>The \<open>\<prec>\<close> relation, the strict part of \<open>\<lesssim>\<close>\<close> |
31381 | 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) |
60500 | 132 |
from \<open>f \<lesssim> g\<close> obtain n c where *:"c > 0" "\<And>m. m > n \<Longrightarrow> f m \<le> c * g m" |
51263
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" |
60500 | 136 |
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
|
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 |
|
60500 | 149 |
text \<open> |
61585 | 150 |
I did not find a proof for \<open>f \<prec> g \<longleftrightarrow> f \<in> o(g)\<close>. Maybe this only |
151 |
holds if \<open>f\<close> and/or \<open>g\<close> are of a certain class of functions. |
|
152 |
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
|
153 |
handy introduction rule. |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
154 |
|
61585 | 155 |
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
|
156 |
|
61585 | 157 |
Something still has to be said about the coefficient \<open>c\<close> in |
158 |
the definition of \<open>(\<prec>)\<close>. In the typical definition of \<open>o\<close>, |
|
159 |
it occurs on the \emph{right} hand side of the \<open>(>)\<close>. The reason |
|
160 |
is that the situation is dual to the definition of \<open>O\<close>: the definition |
|
161 |
works since \<open>c\<close> may become arbitrary small. Since this is not possible |
|
51263
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. |
60500 | 164 |
\<close> |
31381 | 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 |
60500 | 171 |
from assms \<open>1 > 0\<close> have "\<exists>n. \<forall>m>n. 1 * f m < g m" . |
51263
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 |
60500 | 180 |
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
|
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 |
|
61585 | 190 |
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
|
191 |
|
61585 | 192 |
text \<open>This yields all lemmas relating \<open>\<lesssim>\<close>, \<open>\<prec>\<close> and \<open>\<cong>\<close>.\<close> |
31381 | 193 |
|
194 |
interpretation fun_order: preorder_equiv less_eq_fun less_fun |
|
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
60500
diff
changeset
|
195 |
rewrites "preorder_equiv.equiv less_eq_fun = equiv_fun" |
31381 | 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 |
60500 | 210 |
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
|
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 |
60500 | 213 |
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
|
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 |
60500 | 222 |
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
|
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 |
60500 | 226 |
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
|
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 |
60500 | 246 |
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
|
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 |
60500 | 254 |
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
|
255 |
then have "g \<lesssim> f" .. |
60500 | 256 |
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
|
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 |
60500 | 260 |
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
|
261 |
and P\<^sub>1: "\<And>m. m > n\<^sub>1 \<Longrightarrow> f m \<le> c\<^sub>1 * g m" by rule blast |
60500 | 262 |
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
|
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 |
60500 | 272 |
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
|
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 |
||
60500 | 280 |
subsection \<open>Simple examples\<close> |
31381 | 281 |
|
60500 | 282 |
text \<open> |
51263
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 |
59113 | 285 |
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
|
286 |
has to be added yet. |
60500 | 287 |
\<close> |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
288 |
|
60500 | 289 |
text \<open>@{prop "(\<lambda>n. f n + k) \<cong> f"}\<close> |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
290 |
|
60500 | 291 |
text \<open>@{prop "(\<lambda>n. Suc k * f n) \<cong> f"}\<close> |
51263
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 |
|
60500 | 315 |
text \<open>@{prop "Discrete.log \<prec> Discrete.sqrt"}\<close> |
51263
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 |
60500 | 329 |
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
|
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 |
|
60500 | 343 |
text \<open>@{prop "(\<lambda>n. n ^ k) \<prec> (\<lambda>n. 2 ^ n)"}\<close> |
31381 | 344 |
|
345 |
end |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
41413
diff
changeset
|
346 |