# Theory BigO

theory BigO
imports Complex_Main Function_Algebras Set_Algebras
```(*  Title:      HOL/Library/BigO.thy
Authors:    Jeremy Avigad and Kevin Donnelly
*)

section ‹Big O notation›

theory BigO
imports
Complex_Main
Function_Algebras
Set_Algebras
begin

text ‹
This library is designed to support asymptotic ``big O'' calculations,
i.e.~reasoning with expressions of the form ‹f = O(g)› and ‹f = g + O(h)›.
An earlier version of this library is described in detail in @{cite

The main changes in this version are as follows:

▪ We have eliminated the ‹O› operator on sets. (Most uses of this seem
to be inessential.)
▪ We no longer use ‹+› as output syntax for ‹+o›
▪ Lemmas involving ‹sumr› have been replaced by more general lemmas
involving `‹sum›.
▪ The library has been expanded, with e.g.~support for expressions of
the form ‹f < g + O(h)›.

Note also since the Big O library includes rules that demonstrate set
inclusion, to use the automated reasoners effectively with the library one
should redeclare the theorem ‹subsetI› as an intro rule, rather than as an
‹intro!› rule, for example, using ⬚‹declare subsetI [del, intro]›.
›

subsection ‹Definitions›

definition bigo :: "('a ⇒ 'b::linordered_idom) ⇒ ('a ⇒ 'b) set"  ("(1O'(_'))")
where "O(f:: 'a ⇒ 'b) = {h. ∃c. ∀x. ¦h x¦ ≤ c * ¦f x¦}"

lemma bigo_pos_const:
"(∃c::'a::linordered_idom. ∀x. ¦h x¦ ≤ c * ¦f x¦) ⟷
(∃c. 0 < c ∧ (∀x. ¦h x¦ ≤ c * ¦f x¦))"
apply auto
apply (case_tac "c = 0")
apply simp
apply (rule_tac x = "1" in exI)
apply simp
apply (rule_tac x = "¦c¦" in exI)
apply auto
apply (subgoal_tac "c * ¦f x¦ ≤ ¦c¦ * ¦f x¦")
apply (erule_tac x = x in allE)
apply force
apply (rule mult_right_mono)
apply (rule abs_ge_self)
apply (rule abs_ge_zero)
done

lemma bigo_alt_def: "O(f) = {h. ∃c. 0 < c ∧ (∀x. ¦h x¦ ≤ c * ¦f x¦)}"
by (auto simp add: bigo_def bigo_pos_const)

lemma bigo_elt_subset [intro]: "f ∈ O(g) ⟹ O(f) ≤ O(g)"
apply (rule_tac x = "ca * c" in exI)
apply (rule conjI)
apply simp
apply (rule allI)
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "ca * ¦f xa¦ ≤ ca * (c * ¦g xa¦)")
apply (erule order_trans)
apply (rule mult_left_mono, assumption)
apply (rule order_less_imp_le, assumption)
done

lemma bigo_refl [intro]: "f ∈ O(f)"
apply (rule_tac x = 1 in exI)
apply simp
done

lemma bigo_zero: "0 ∈ O(g)"
apply (auto simp add: bigo_def func_zero)
apply (rule_tac x = 0 in exI)
apply auto
done

lemma bigo_zero2: "O(λx. 0) = {λx. 0}"

lemma bigo_plus_self_subset [intro]: "O(f) + O(f) ⊆ O(f)"
apply (auto simp add: bigo_alt_def set_plus_def)
apply (rule_tac x = "c + ca" in exI)
apply auto
apply (rule order_trans)
apply (rule abs_triangle_ineq)
apply force
apply force
done

lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
apply (rule equalityI)
apply (rule bigo_plus_self_subset)
apply (rule set_zero_plus2)
apply (rule bigo_zero)
done

lemma bigo_plus_subset [intro]: "O(f + g) ⊆ O(f) + O(g)"
apply (rule subsetI)
apply (auto simp add: bigo_def bigo_pos_const func_plus set_plus_def)
apply (subst bigo_pos_const [symmetric])+
apply (rule_tac x = "λn. if ¦g n¦ ≤ ¦f n¦ then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply (clarsimp)
apply (subgoal_tac "c * ¦f xa + g xa¦ ≤ (c + c) * ¦f xa¦")
apply (erule_tac x = xa in allE)
apply (erule order_trans)
apply (simp)
apply (subgoal_tac "c * ¦f xa + g xa¦ ≤ c * (¦f xa¦ + ¦g xa¦)")
apply (erule order_trans)
apply (rule mult_left_mono)
apply (rule_tac x = "λn. if ¦f n¦ < ¦g n¦ then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply auto
apply (subgoal_tac "c * ¦f xa + g xa¦ ≤ (c + c) * ¦g xa¦")
apply (erule_tac x = xa in allE)
apply (erule order_trans)
apply simp
apply (subgoal_tac "c * ¦f xa + g xa¦ ≤ c * (¦f xa¦ + ¦g xa¦)")
apply (erule order_trans)
apply (rule mult_left_mono)
apply (rule abs_triangle_ineq)
done

lemma bigo_plus_subset2 [intro]: "A ⊆ O(f) ⟹ B ⊆ O(f) ⟹ A + B ⊆ O(f)"
apply (subgoal_tac "A + B ⊆ O(f) + O(f)")
apply (erule order_trans)
apply simp
apply (auto del: subsetI simp del: bigo_plus_idemp)
done

lemma bigo_plus_eq: "∀x. 0 ≤ f x ⟹ ∀x. 0 ≤ g x ⟹ O(f + g) = O(f) + O(g)"
apply (rule equalityI)
apply (rule bigo_plus_subset)
apply (simp add: bigo_alt_def set_plus_def func_plus)
apply clarify
apply (rule_tac x = "max c ca" in exI)
apply (rule conjI)
apply (subgoal_tac "c ≤ max c ca")
apply (erule order_less_le_trans)
apply assumption
apply (rule max.cobounded1)
apply clarify
apply (drule_tac x = "xa" in spec)+
apply (subgoal_tac "0 ≤ f xa + g xa")
apply (subgoal_tac "¦a xa + b xa¦ ≤ ¦a xa¦ + ¦b xa¦")
apply (subgoal_tac "¦a xa¦ + ¦b xa¦ ≤ max c ca * f xa + max c ca * g xa")
apply force
apply (subgoal_tac "c * f xa ≤ max c ca * f xa")
apply force
apply (rule mult_right_mono)
apply (rule max.cobounded1)
apply assumption
apply (subgoal_tac "ca * g xa ≤ max c ca * g xa")
apply force
apply (rule mult_right_mono)
apply (rule max.cobounded2)
apply assumption
apply (rule abs_triangle_ineq)
apply assumption+
done

lemma bigo_bounded_alt: "∀x. 0 ≤ f x ⟹ ∀x. f x ≤ c * g x ⟹ f ∈ O(g)"
apply (rule_tac x = "¦c¦" in exI)
apply auto
apply (drule_tac x = x in spec)+
done

lemma bigo_bounded: "∀x. 0 ≤ f x ⟹ ∀x. f x ≤ g x ⟹ f ∈ O(g)"
apply (erule bigo_bounded_alt [of f 1 g])
apply simp
done

lemma bigo_bounded2: "∀x. lb x ≤ f x ⟹ ∀x. f x ≤ lb x + g x ⟹ f ∈ lb +o O(g)"
apply (rule set_minus_imp_plus)
apply (rule bigo_bounded)
apply (auto simp add: fun_Compl_def func_plus)
apply (drule_tac x = x in spec)+
apply force
done

lemma bigo_abs: "(λx. ¦f x¦) =o O(f)"
apply (unfold bigo_def)
apply auto
apply (rule_tac x = 1 in exI)
apply auto
done

lemma bigo_abs2: "f =o O(λx. ¦f x¦)"
apply (unfold bigo_def)
apply auto
apply (rule_tac x = 1 in exI)
apply auto
done

lemma bigo_abs3: "O(f) = O(λx. ¦f x¦)"
apply (rule equalityI)
apply (rule bigo_elt_subset)
apply (rule bigo_abs2)
apply (rule bigo_elt_subset)
apply (rule bigo_abs)
done

lemma bigo_abs4: "f =o g +o O(h) ⟹ (λx. ¦f x¦) =o (λx. ¦g x¦) +o O(h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
proof -
assume *: "f - g ∈ O(h)"
have "(λx. ¦f x¦ - ¦g x¦) =o O(λx. ¦¦f x¦ - ¦g x¦¦)"
by (rule bigo_abs2)
also have "… ⊆ O(λx. ¦f x - g x¦)"
apply (rule bigo_elt_subset)
apply (rule bigo_bounded)
apply force
apply (rule allI)
apply (rule abs_triangle_ineq3)
done
also have "… ⊆ O(f - g)"
apply (rule bigo_elt_subset)
apply (subst fun_diff_def)
apply (rule bigo_abs)
done
also from * have "… ⊆ O(h)"
by (rule bigo_elt_subset)
finally show "(λx. ¦f x¦ - ¦g x¦) ∈ O(h)".
qed

lemma bigo_abs5: "f =o O(g) ⟹ (λx. ¦f x¦) =o O(g)"
by (auto simp: bigo_def)

lemma bigo_elt_subset2 [intro]:
assumes *: "f ∈ g +o O(h)"
shows "O(f) ⊆ O(g) + O(h)"
proof -
note *
also have "g +o O(h) ⊆ O(g) + O(h)"
by (auto del: subsetI)
also have "… = O(λx. ¦g x¦) + O(λx. ¦h x¦)"
by (subst bigo_abs3 [symmetric])+ (rule refl)
also have "… = O((λx. ¦g x¦) + (λx. ¦h x¦))"
by (rule bigo_plus_eq [symmetric]) auto
finally have "f ∈ …" .
then have "O(f) ⊆ …"
by (elim bigo_elt_subset)
also have "… = O(λx. ¦g x¦) + O(λx. ¦h x¦)"
by (rule bigo_plus_eq, auto)
finally show ?thesis
qed

lemma bigo_mult [intro]: "O(f)*O(g) ⊆ O(f * g)"
apply (rule subsetI)
apply (subst bigo_def)
apply (auto simp add: bigo_alt_def set_times_def func_times)
apply (rule_tac x = "c * ca" in exI)
apply (rule allI)
apply (erule_tac x = x in allE)+
apply (subgoal_tac "c * ca * ¦f x * g x¦ = (c * ¦f x¦) * (ca * ¦g x¦)")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_mono)
apply assumption+
apply auto
done

lemma bigo_mult2 [intro]: "f *o O(g) ⊆ O(f * g)"
apply (auto simp add: bigo_def elt_set_times_def func_times abs_mult)
apply (rule_tac x = c in exI)
apply auto
apply (drule_tac x = x in spec)
apply (subgoal_tac "¦f x¦ * ¦b x¦ ≤ ¦f x¦ * (c * ¦g x¦)")
apply (rule mult_left_mono, assumption)
apply (rule abs_ge_zero)
done

lemma bigo_mult3: "f ∈ O(h) ⟹ g ∈ O(j) ⟹ f * g ∈ O(h * j)"
apply (rule subsetD)
apply (rule bigo_mult)
apply (erule set_times_intro, assumption)
done

lemma bigo_mult4 [intro]: "f ∈ k +o O(h) ⟹ g * f ∈ (g * k) +o O(g * h)"
apply (drule set_plus_imp_minus)
apply (rule set_minus_imp_plus)
apply (drule bigo_mult3 [where g = g and j = g])
done

lemma bigo_mult5:
fixes f :: "'a ⇒ 'b::linordered_field"
assumes "∀x. f x ≠ 0"
shows "O(f * g) ⊆ f *o O(g)"
proof
fix h
assume "h ∈ O(f * g)"
then have "(λx. 1 / (f x)) * h ∈ (λx. 1 / f x) *o O(f * g)"
by auto
also have "… ⊆ O((λx. 1 / f x) * (f * g))"
by (rule bigo_mult2)
also have "(λx. 1 / f x) * (f * g) = g"
apply (rule ext)
apply (simp add: assms nonzero_divide_eq_eq ac_simps)
done
finally have "(λx. (1::'b) / f x) * h ∈ O(g)" .
then have "f * ((λx. (1::'b) / f x) * h) ∈ f *o O(g)"
by auto
also have "f * ((λx. (1::'b) / f x) * h) = h"
apply (rule ext)
apply (simp add: assms nonzero_divide_eq_eq ac_simps)
done
finally show "h ∈ f *o O(g)" .
qed

lemma bigo_mult6: "∀x. f x ≠ 0 ⟹ O(f * g) = f *o O(g)"
for f :: "'a ⇒ 'b::linordered_field"
apply (rule equalityI)
apply (erule bigo_mult5)
apply (rule bigo_mult2)
done

lemma bigo_mult7: "∀x. f x ≠ 0 ⟹ O(f * g) ⊆ O(f) * O(g)"
for f :: "'a ⇒ 'b::linordered_field"
apply (subst bigo_mult6)
apply assumption
apply (rule set_times_mono3)
apply (rule bigo_refl)
done

lemma bigo_mult8: "∀x. f x ≠ 0 ⟹ O(f * g) = O(f) * O(g)"
for f :: "'a ⇒ 'b::linordered_field"
apply (rule equalityI)
apply (erule bigo_mult7)
apply (rule bigo_mult)
done

lemma bigo_minus [intro]: "f ∈ O(g) ⟹ - f ∈ O(g)"
by (auto simp add: bigo_def fun_Compl_def)

lemma bigo_minus2: "f ∈ g +o O(h) ⟹ - f ∈ -g +o O(h)"
apply (rule set_minus_imp_plus)
apply (drule set_plus_imp_minus)
apply (drule bigo_minus)
apply simp
done

lemma bigo_minus3: "O(- f) = O(f)"
by (auto simp add: bigo_def fun_Compl_def)

lemma bigo_plus_absorb_lemma1:
assumes *: "f ∈ O(g)"
shows "f +o O(g) ⊆ O(g)"
proof -
have "f ∈ O(f)" by auto
then have "f +o O(g) ⊆ O(f) + O(g)"
by (auto del: subsetI)
also have "… ⊆ O(g) + O(g)"
proof -
from * have "O(f) ⊆ O(g)"
by (auto del: subsetI)
then show ?thesis
by (auto del: subsetI)
qed
also have "… ⊆ O(g)" by simp
finally show ?thesis .
qed

lemma bigo_plus_absorb_lemma2:
assumes *: "f ∈ O(g)"
shows "O(g) ⊆ f +o O(g)"
proof -
from * have "- f ∈ O(g)"
by auto
then have "- f +o O(g) ⊆ O(g)"
by (elim bigo_plus_absorb_lemma1)
then have "f +o (- f +o O(g)) ⊆ f +o O(g)"
by auto
also have "f +o (- f +o O(g)) = O(g)"
finally show ?thesis .
qed

lemma bigo_plus_absorb [simp]: "f ∈ O(g) ⟹ f +o O(g) = O(g)"
apply (rule equalityI)
apply (erule bigo_plus_absorb_lemma1)
apply (erule bigo_plus_absorb_lemma2)
done

lemma bigo_plus_absorb2 [intro]: "f ∈ O(g) ⟹ A ⊆ O(g) ⟹ f +o A ⊆ O(g)"
apply (subgoal_tac "f +o A ⊆ f +o O(g)")
apply force+
done

lemma bigo_add_commute_imp: "f ∈ g +o O(h) ⟹ g ∈ f +o O(h)"
apply (subst set_minus_plus [symmetric])
apply (subgoal_tac "g - f = - (f - g)")
apply (erule ssubst)
apply (rule bigo_minus)
apply (subst set_minus_plus)
apply assumption
done

lemma bigo_add_commute: "f ∈ g +o O(h) ⟷ g ∈ f +o O(h)"
apply (rule iffI)
done

lemma bigo_const1: "(λx. c) ∈ O(λx. 1)"
by (auto simp add: bigo_def ac_simps)

lemma bigo_const2 [intro]: "O(λx. c) ⊆ O(λx. 1)"
apply (rule bigo_elt_subset)
apply (rule bigo_const1)
done

lemma bigo_const3: "c ≠ 0 ⟹ (λx. 1) ∈ O(λx. c)"
for c :: "'a::linordered_field"
apply (rule_tac x = "¦inverse c¦" in exI)
done

lemma bigo_const4: "c ≠ 0 ⟹ O(λx. 1) ⊆ O(λx. c)"
for c :: "'a::linordered_field"
apply (rule bigo_elt_subset)
apply (rule bigo_const3)
apply assumption
done

lemma bigo_const [simp]: "c ≠ 0 ⟹ O(λx. c) = O(λx. 1)"
for c :: "'a::linordered_field"
apply (rule equalityI)
apply (rule bigo_const2)
apply (rule bigo_const4)
apply assumption
done

lemma bigo_const_mult1: "(λx. c * f x) ∈ O(f)"
apply (rule_tac x = "¦c¦" in exI)
apply (auto simp add: abs_mult [symmetric])
done

lemma bigo_const_mult2: "O(λx. c * f x) ⊆ O(f)"
apply (rule bigo_elt_subset)
apply (rule bigo_const_mult1)
done

lemma bigo_const_mult3: "c ≠ 0 ⟹ f ∈ O(λx. c * f x)"
for c :: "'a::linordered_field"
apply (rule_tac x = "¦inverse c¦" in exI)
apply (simp add: abs_mult mult.assoc [symmetric])
done

lemma bigo_const_mult4: "c ≠ 0 ⟹ O(f) ⊆ O(λx. c * f x)"
for c :: "'a::linordered_field"
apply (rule bigo_elt_subset)
apply (rule bigo_const_mult3)
apply assumption
done

lemma bigo_const_mult [simp]: "c ≠ 0 ⟹ O(λx. c * f x) = O(f)"
for c :: "'a::linordered_field"
apply (rule equalityI)
apply (rule bigo_const_mult2)
apply (erule bigo_const_mult4)
done

lemma bigo_const_mult5 [simp]: "c ≠ 0 ⟹ (λx. c) *o O(f) = O(f)"
for c :: "'a::linordered_field"
apply (auto del: subsetI)
apply (rule order_trans)
apply (rule bigo_mult2)
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
apply (rule_tac x = "λy. inverse c * x y" in exI)
apply (simp add: mult.assoc [symmetric] abs_mult)
apply (rule_tac x = "¦inverse c¦ * ca" in exI)
apply auto
done

lemma bigo_const_mult6 [intro]: "(λx. c) *o O(f) ⊆ O(f)"
apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
apply (rule_tac x = "ca * ¦c¦" in exI)
apply (rule allI)
apply (subgoal_tac "ca * ¦c¦ * ¦f x¦ = ¦c¦ * (ca * ¦f x¦)")
apply (erule ssubst)
apply (subst abs_mult)
apply (rule mult_left_mono)
apply (erule spec)
apply simp
done

lemma bigo_const_mult7 [intro]:
assumes *: "f =o O(g)"
shows "(λx. c * f x) =o O(g)"
proof -
from * have "(λx. c) * f =o (λx. c) *o O(g)"
by auto
also have "(λx. c) * f = (λx. c * f x)"
also have "(λx. c) *o O(g) ⊆ O(g)"
by (auto del: subsetI)
finally show ?thesis .
qed

lemma bigo_compose1: "f =o O(g) ⟹ (λx. f (k x)) =o O(λx. g (k x))"
by (auto simp: bigo_def)

lemma bigo_compose2: "f =o g +o O(h) ⟹ (λx. f (k x)) =o (λx. g (k x)) +o O(λx. h(k x))"
apply (simp only: set_minus_plus [symmetric] fun_Compl_def func_plus)
apply (drule bigo_compose1)
done

subsection ‹Sum›

lemma bigo_sum_main: "∀x. ∀y ∈ A x. 0 ≤ h x y ⟹
∃c. ∀x. ∀y ∈ A x. ¦f x y¦ ≤ c * h x y ⟹
(λx. ∑y ∈ A x. f x y) =o O(λx. ∑y ∈ A x. h x y)"
apply (rule_tac x = "¦c¦" in exI)
apply (subst abs_of_nonneg) back back
apply (rule sum_nonneg)
apply force
apply (subst sum_distrib_left)
apply (rule allI)
apply (rule order_trans)
apply (rule sum_abs)
apply (rule sum_mono)
apply (rule order_trans)
apply (drule spec)+
apply (drule bspec)+
apply assumption+
apply (drule bspec)
apply assumption+
apply (rule mult_right_mono)
apply (rule abs_ge_self)
apply force
done

lemma bigo_sum1: "∀x y. 0 ≤ h x y ⟹
∃c. ∀x y. ¦f x y¦ ≤ c * h x y ⟹
(λx. ∑y ∈ A x. f x y) =o O(λx. ∑y ∈ A x. h x y)"
apply (rule bigo_sum_main)
apply force
apply clarsimp
apply (rule_tac x = c in exI)
apply force
done

lemma bigo_sum2: "∀y. 0 ≤ h y ⟹
∃c. ∀y. ¦f y¦ ≤ c * (h y) ⟹
(λx. ∑y ∈ A x. f y) =o O(λx. ∑y ∈ A x. h y)"
by (rule bigo_sum1) auto

lemma bigo_sum3: "f =o O(h) ⟹
(λx. ∑y ∈ A x. l x y * f (k x y)) =o O(λx. ∑y ∈ A x. ¦l x y * h (k x y)¦)"
apply (rule bigo_sum1)
apply (rule allI)+
apply (rule abs_ge_zero)
apply (unfold bigo_def)
apply auto
apply (rule_tac x = c in exI)
apply (rule allI)+
apply (subst abs_mult)+
apply (subst mult.left_commute)
apply (rule mult_left_mono)
apply (erule spec)
apply (rule abs_ge_zero)
done

lemma bigo_sum4: "f =o g +o O(h) ⟹
(λx. ∑y ∈ A x. l x y * f (k x y)) =o
(λx. ∑y ∈ A x. l x y * g (k x y)) +o
O(λx. ∑y ∈ A x. ¦l x y * h (k x y)¦)"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst sum_subtractf [symmetric])
apply (subst right_diff_distrib [symmetric])
apply (rule bigo_sum3)
apply (subst fun_diff_def [symmetric])
apply (erule set_plus_imp_minus)
done

lemma bigo_sum5: "f =o O(h) ⟹ ∀x y. 0 ≤ l x y ⟹
∀x. 0 ≤ h x ⟹
(λx. ∑y ∈ A x. l x y * f (k x y)) =o
O(λx. ∑y ∈ A x. l x y * h (k x y))"
apply (subgoal_tac "(λx. ∑y ∈ A x. l x y * h (k x y)) =
(λx. ∑y ∈ A x. ¦l x y * h (k x y)¦)")
apply (erule ssubst)
apply (erule bigo_sum3)
apply (rule ext)
apply (rule sum.cong)
apply (rule refl)
apply (subst abs_of_nonneg)
apply auto
done

lemma bigo_sum6: "f =o g +o O(h) ⟹ ∀x y. 0 ≤ l x y ⟹
∀x. 0 ≤ h x ⟹
(λx. ∑y ∈ A x. l x y * f (k x y)) =o
(λx. ∑y ∈ A x. l x y * g (k x y)) +o
O(λx. ∑y ∈ A x. l x y * h (k x y))"
apply (rule set_minus_imp_plus)
apply (subst fun_diff_def)
apply (subst sum_subtractf [symmetric])
apply (subst right_diff_distrib [symmetric])
apply (rule bigo_sum5)
apply (subst fun_diff_def [symmetric])
apply (drule set_plus_imp_minus)
apply auto
done

subsection ‹Misc useful stuff›

lemma bigo_useful_intro: "A ⊆ O(f) ⟹ B ⊆ O(f) ⟹ A + B ⊆ O(f)"
apply (subst bigo_plus_idemp [symmetric])
apply (rule set_plus_mono2)
apply assumption+
done

lemma bigo_useful_add: "f =o O(h) ⟹ g =o O(h) ⟹ f + g =o O(h)"
apply (subst bigo_plus_idemp [symmetric])
apply (rule set_plus_intro)
apply assumption+
done

lemma bigo_useful_const_mult: "c ≠ 0 ⟹ (λx. c) * f =o O(h) ⟹ f =o O(h)"
for c :: "'a::linordered_field"
apply (rule subsetD)
apply (subgoal_tac "(λx. 1 / c) *o O(h) ⊆ O(h)")
apply assumption
apply (rule bigo_const_mult6)
apply (subgoal_tac "f = (λx. 1 / c) * ((λx. c) * f)")
apply (erule ssubst)
apply (erule set_times_intro2)
done

lemma bigo_fix: "(λx::nat. f (x + 1)) =o O(λx. h (x + 1)) ⟹ f 0 = 0 ⟹ f =o O(h)"
apply auto
apply (rule_tac x = c in exI)
apply auto
apply (case_tac "x = 0")
apply simp
apply (subgoal_tac "x = Suc (x - 1)")
apply (erule ssubst) back
apply (erule spec)
apply simp
done

lemma bigo_fix2:
"(λx. f ((x::nat) + 1)) =o (λx. g(x + 1)) +o O(λx. h(x + 1)) ⟹
f 0 = g 0 ⟹ f =o g +o O(h)"
apply (rule set_minus_imp_plus)
apply (rule bigo_fix)
apply (subst fun_diff_def)
apply (subst fun_diff_def [symmetric])
apply (rule set_plus_imp_minus)
apply simp
done

subsection ‹Less than or equal to›

definition lesso :: "('a ⇒ 'b::linordered_idom) ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b"  (infixl "<o" 70)
where "f <o g = (λx. max (f x - g x) 0)"

lemma bigo_lesseq1: "f =o O(h) ⟹ ∀x. ¦g x¦ ≤ ¦f x¦ ⟹ g =o O(h)"
apply (unfold bigo_def)
apply clarsimp
apply (rule_tac x = c in exI)
apply (rule allI)
apply (rule order_trans)
apply (erule spec)+
done

lemma bigo_lesseq2: "f =o O(h) ⟹ ∀x. ¦g x¦ ≤ f x ⟹ g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
apply (drule_tac x = x in spec)
apply (rule order_trans)
apply assumption
apply (rule abs_ge_self)
done

lemma bigo_lesseq3: "f =o O(h) ⟹ ∀x. 0 ≤ g x ⟹ ∀x. g x ≤ f x ⟹ g =o O(h)"
apply (erule bigo_lesseq2)
apply (rule allI)
apply (subst abs_of_nonneg)
apply (erule spec)+
done

lemma bigo_lesseq4: "f =o O(h) ⟹
∀x. 0 ≤ g x ⟹ ∀x. g x ≤ ¦f x¦ ⟹ g =o O(h)"
apply (erule bigo_lesseq1)
apply (rule allI)
apply (subst abs_of_nonneg)
apply (erule spec)+
done

lemma bigo_lesso1: "∀x. f x ≤ g x ⟹ f <o g =o O(h)"
apply (unfold lesso_def)
apply (subgoal_tac "(λx. max (f x - g x) 0) = 0")
apply (erule ssubst)
apply (rule bigo_zero)
apply (unfold func_zero)
apply (rule ext)
apply (simp split: split_max)
done

lemma bigo_lesso2: "f =o g +o O(h) ⟹ ∀x. 0 ≤ k x ⟹ ∀x. k x ≤ f x ⟹ k <o g =o O(h)"
apply (unfold lesso_def)
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
apply (rule allI)
apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
apply (case_tac "0 ≤ k x - g x")
apply simp
apply (subst abs_of_nonneg)
apply (drule_tac x = x in spec) back
apply (erule spec)
apply (rule order_trans)
prefer 2
apply (rule abs_ge_zero)
done

lemma bigo_lesso3: "f =o g +o O(h) ⟹ ∀x. 0 ≤ k x ⟹ ∀x. g x ≤ k x ⟹ f <o k =o O(h)"
apply (unfold lesso_def)
apply (rule bigo_lesseq4)
apply (erule set_plus_imp_minus)
apply (rule allI)
apply (rule max.cobounded2)
apply (rule allI)
apply (subst fun_diff_def)
apply (case_tac "0 ≤ f x - k x")
apply simp
apply (subst abs_of_nonneg)
apply (drule_tac x = x in spec) back
apply (rule le_imp_neg_le)
apply (erule spec)
apply (rule order_trans)
prefer 2
apply (rule abs_ge_zero)
done

lemma bigo_lesso4: "f <o g =o O(k) ⟹ g =o h +o O(k) ⟹ f <o h =o O(k)"
for k :: "'a ⇒ 'b::linordered_field"
apply (unfold lesso_def)
apply (drule set_plus_imp_minus)
apply (drule bigo_abs5) back
apply assumption
apply (erule bigo_lesseq2) back
apply (rule allI)
apply (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
done

lemma bigo_lesso5: "f <o g =o O(h) ⟹ ∃C. ∀x. f x ≤ g x + C * ¦h x¦"
apply (simp only: lesso_def bigo_alt_def)
apply clarsimp
apply (rule_tac x = c in exI)
apply (rule allI)
apply (drule_tac x = x in spec)
apply (subgoal_tac "¦max (f x - g x) 0¦ = max (f x - g x) 0")
apply (rule abs_of_nonneg)
apply (rule max.cobounded2)
done

lemma lesso_add: "f <o g =o O(h) ⟹ k <o l =o O(h) ⟹ (f + k) <o (g + l) =o O(h)"
apply (unfold lesso_def)
apply (rule bigo_lesseq3)
apply assumption
apply (force split: split_max)
apply (auto split: split_max simp add: func_plus)
done

lemma bigo_LIMSEQ1: "f =o O(g) ⟹ g ⇢ 0 ⟹ f ⇢ 0"
for f g :: "nat ⇒ real"
apply clarify
apply (drule_tac x = "r / c" in spec)
apply (drule mp)
apply simp
apply clarify
apply (rule_tac x = no in exI)
apply (rule allI)
apply (drule_tac x = n in spec)+
apply (rule impI)
apply (drule mp)
apply assumption
apply (rule order_le_less_trans)
apply assumption
apply (rule order_less_le_trans)
apply (subgoal_tac "c * ¦g n¦ < c * (r / c)")
apply assumption
apply (erule mult_strict_left_mono)
apply assumption
apply simp
done

lemma bigo_LIMSEQ2: "f =o g +o O(h) ⟹ h ⇢ 0 ⟹ f ⇢ a ⟹ g ⇢ a"
for f g h :: "nat ⇒ real"
apply (drule set_plus_imp_minus)
apply (drule bigo_LIMSEQ1)
apply assumption
apply (simp only: fun_diff_def)
apply (erule Lim_transform2)
apply assumption
done

end
```