(* Author: Florian Haftmann, TU Muenchen *)
section \Comparing growth of functions on natural numbers by a preorder relation\
theory Function_Growth
imports Main Preorder Discrete
begin
(* FIXME move *)
context linorder
begin
lemma mono_invE:
fixes f :: "'a \ 'b::order"
assumes "mono f"
assumes "f x < f y"
obtains "x < y"
proof
show "x < y"
proof (rule ccontr)
assume "\ x < y"
then have "y \ x" by simp
with \mono f\ obtain "f y \ f x" by (rule monoE)
with \f x < f y\ show False by simp
qed
qed
end
lemma (in semidom_divide) power_diff:
fixes a :: 'a
assumes "a \ 0"
assumes "m \ n"
shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
proof -
def q == "m - n"
moreover with assms have "m = q + n" by (simp add: q_def)
ultimately show ?thesis using `a \ 0` by (simp add: power_add)
qed
subsection \Motivation\
text \
When comparing growth of functions in computer science, it is common to adhere
on Landau Symbols (``O-Notation''). However these come at the cost of notational
oddities, particularly writing \f = O(g)\ for \f \ O(g)\ etc.
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 \\\ on functions such that
\f \ g \ f \ 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 hierarchy of functions:
\(\n. 0) \ (\n. k) \ Discrete.log \ Discrete.sqrt \ id \ \\.
\
subsection \Model\
text \
Our growth functions are of type \\ \ \\. This is different
to the usual conventions for Landau symbols for which \\ \ \\
would be appropriate, but we argue that \\ \ \\ is more
appropriate for analysis, whereas our setting is discrete.
Note that we also restrict the additional coefficients to \\\, something
we discuss at the particular definitions.
\
subsection \The \\\ relation\
definition less_eq_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50)
where
"f \ g \ (\c>0. \n. \m>n. f m \ c * g m)"
text \
This yields \f \ g \ f \ O(g)\. Note that \c\ is restricted to
\\\. This does not pose any problems since if \f \ O(g)\ holds for
a \c \ \\, it also holds for \\c\ \ \\ by transitivity.
\
lemma less_eq_funI [intro?]:
assumes "\c>0. \n. \m>n. f m \ c * g m"
shows "f \ g"
unfolding less_eq_fun_def by (rule assms)
lemma not_less_eq_funI:
assumes "\c n. c > 0 \ \m>n. c * g m < f m"
shows "\ f \ g"
using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
lemma less_eq_funE [elim?]:
assumes "f \ g"
obtains n c where "c > 0" and "\m. m > n \ f m \ c * g m"
using assms unfolding less_eq_fun_def by blast
lemma not_less_eq_funE:
assumes "\ f \ g" and "c > 0"
obtains m where "m > n" and "c * g m < f m"
using assms unfolding less_eq_fun_def linorder_not_le [symmetric] by blast
subsection \The \\\ relation, the equivalence relation induced by \\\\
definition equiv_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50)
where
"f \ g \
(\c\<^sub>1>0. \c\<^sub>2>0. \n. \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m)"
text \
This yields \f \ g \ f \ \(g)\. Concerning \c\<^sub>1\ and \c\<^sub>2\
restricted to @{typ nat}, see note above on \(\)\.
\
lemma equiv_funI:
assumes "\c\<^sub>1>0. \c\<^sub>2>0. \n. \m>n. f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m"
shows "f \ g"
unfolding equiv_fun_def by (rule assms)
lemma not_equiv_funI:
assumes "\c\<^sub>1 c\<^sub>2 n. c\<^sub>1 > 0 \ c\<^sub>2 > 0 \
\m>n. c\<^sub>1 * f m < g m \ c\<^sub>2 * g m < f m"
shows "\ f \ g"
using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
lemma equiv_funE:
assumes "f \ g"
obtains n c\<^sub>1 c\<^sub>2 where "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
and "\m. m > n \ f m \ c\<^sub>1 * g m \ g m \ c\<^sub>2 * f m"
using assms unfolding equiv_fun_def by blast
lemma not_equiv_funE:
fixes n c\<^sub>1 c\<^sub>2
assumes "\ f \ g" and "c\<^sub>1 > 0" and "c\<^sub>2 > 0"
obtains m where "m > n"
and "c\<^sub>1 * f m < g m \ c\<^sub>2 * g m < f m"
using assms unfolding equiv_fun_def linorder_not_le [symmetric] by blast
subsection \The \\\ relation, the strict part of \\\\
definition less_fun :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50)
where
"f \ g \ f \ g \ \ g \ f"
lemma less_funI:
assumes "\c>0. \n. \m>n. f m \ c * g m"
and "\c n. c > 0 \ \m>n. c * f m < g m"
shows "f \ g"
using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
lemma not_less_funI:
assumes "\c n. c > 0 \ \m>n. c * g m < f m"
and "\c>0. \n. \m>n. g m \ c * f m"
shows "\ f \ g"
using assms unfolding less_fun_def less_eq_fun_def linorder_not_less [symmetric] by blast
lemma less_funE [elim?]:
assumes "f \ g"
obtains n c where "c > 0" and "\m. m > n \ f m \ c * g m"
and "\c n. c > 0 \ \m>n. c * f m < g m"
proof -
from assms have "f \ g" and "\ g \ f" by (simp_all add: less_fun_def)
from \f \ g\ obtain n c where *:"c > 0" "\m. m > n \ f m \ c * g m"
by (rule less_eq_funE) blast
{ fix c n :: nat
assume "c > 0"
with \\ g \ f\ obtain m where "m > n" "c * f m < g m"
by (rule not_less_eq_funE) blast
then have **: "\m>n. c * f m < g m" by blast
} note ** = this
from * ** show thesis by (rule that)
qed
lemma not_less_funE:
assumes "\ f \ g" and "c > 0"
obtains m where "m > n" and "c * g m < f m"
| d q where "\m. d > 0 \ m > q \ g q \ d * f q"
using assms unfolding less_fun_def linorder_not_less [symmetric] by blast
text \
I did not find a proof for \f \ g \ f \ o(g)\. Maybe this only
holds if \f\ and/or \g\ are of a certain class of functions.
However \f \ o(g) \