author | wenzelm |

Mon Dec 08 23:06:19 2014 +0100 (2014-12-08) | |

changeset 59113 | 3cded6b57a82 |

parent 59112 | e670969f34df |

child 59114 | 8281f83d286f |

tuned spelling;

1.1 --- a/src/HOL/Library/Function_Growth.thy Mon Dec 08 22:42:12 2014 +0100 1.2 +++ b/src/HOL/Library/Function_Growth.thy Mon Dec 08 23:06:19 2014 +0100 1.3 @@ -14,12 +14,12 @@ 1.4 on Landau Symbols (``O-Notation''). However these come at the cost of notational 1.5 oddities, particularly writing @{text "f = O(g)"} for @{text "f \<in> O(g)"} etc. 1.6 1.7 - Here we suggest a diffent way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood, 1.8 + Here we suggest a different way, following Hardy (G.~H.~Hardy and J.~E.~Littlewood, 1.9 Some problems of Diophantine approximation, Acta Mathematica 37 (1914), p.~225). 1.10 We establish a quasi order relation @{text "\<lesssim>"} on functions such that 1.11 @{text "f \<lesssim> g \<longleftrightarrow> f \<in> O(g)"}. From a didactic point of view, this does not only 1.12 avoid the notational oddities mentioned above but also emphasizes the key insight 1.13 - of a growth hierachy of functions: 1.14 + of a growth hierarchy of functions: 1.15 @{text "(\<lambda>n. 0) \<lesssim> (\<lambda>n. k) \<lesssim> Discrete.log \<lesssim> Discrete.sqrt \<lesssim> id \<lesssim> \<dots>"}. 1.16 *} 1.17 1.18 @@ -147,7 +147,7 @@ 1.19 using assms unfolding less_fun_def linorder_not_less [symmetric] by blast 1.20 1.21 text {* 1.22 - I did not found a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}. Maybe this only 1.23 + I did not find a proof for @{text "f \<prec> g \<longleftrightarrow> f \<in> o(g)"}. Maybe this only 1.24 holds if @{text f} and/or @{text g} are of a certain class of functions. 1.25 However @{text "f \<in> o(g) \<longrightarrow> f \<prec> g"} is provable, and this yields a 1.26 handy introduction rule. 1.27 @@ -282,7 +282,7 @@ 1.28 text {* 1.29 Most of these are left as constructive exercises for the reader. Note that additional 1.30 preconditions to the functions may be necessary. The list here is by no means to be 1.31 - intended as complete contruction set for typical functions, here surely something 1.32 + intended as complete construction set for typical functions, here surely something 1.33 has to be added yet. 1.34 *} 1.35