author wenzelm Mon, 08 Dec 2014 23:06:19 +0100 changeset 59113 3cded6b57a82 parent 59112 e670969f34df child 59114 8281f83d286f
tuned spelling;
```--- a/src/HOL/Library/Function_Growth.thy	Mon Dec 08 22:42:12 2014 +0100
+++ b/src/HOL/Library/Function_Growth.thy	Mon Dec 08 23:06:19 2014 +0100
@@ -14,12 +14,12 @@
on Landau Symbols (``O-Notation'').  However these come at the cost of notational
oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc.

-  Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
+  Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood,
Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225).
We establish a quasi order relation @{text "\<lesssim>"} on functions such that
@{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}.  From a didactic point of view, this does not only
avoid the notational oddities mentioned above but also emphasizes the key insight
-  of a growth hierachy of functions:
+  of a growth hierarchy of functions:
@{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}.
*}

@@ -147,7 +147,7 @@
using assms unfolding less_fun_def linorder_not_less [symmetric] by blast

text {*
-  I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
+  I did not find a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}.  Maybe this only
holds if @{text f} and/or @{text g} are of a certain class of functions.
However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a
handy introduction rule.
@@ -282,7 +282,7 @@
text {*
Most of these are left as constructive exercises for the reader.  Note that additional
preconditions to the functions may be necessary.  The list here is by no means to be
-  intended as complete contruction set for typical functions, here surely something
+  intended as complete construction set for typical functions, here surely something