Theory BigO

(*  Title:      HOL/ex/BigO.thy
    Authors:    Jeremy Avigad and Kevin Donnelly; proofs tidied by LCP
*)

section ‹Big O notation›

theory BigO
  imports
    Complex_Main
    "HOL-Library.Function_Algebras"
    "HOL-Library.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>‹"Avigad-Donnelly"›.

  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¦))"
  by (metis (no_types, opaque_lifting) abs_ge_zero abs_not_less_zero abs_of_nonneg dual_order.trans
        mult_1 zero_less_abs_iff zero_less_mult_iff zero_less_one)

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 (auto simp add: bigo_alt_def)
  by (metis (no_types, opaque_lifting) mult.assoc mult_le_cancel_iff2 order.trans
      zero_less_mult_iff)

lemma bigo_refl [intro]: "f ∈ O(f)"
  using bigo_def comm_monoid_mult_class.mult_1 dual_order.eq_iff by blast

lemma bigo_zero: "0 ∈ O(g)"
  using bigo_def mult_le_cancel_left1 by fastforce

lemma bigo_zero2: "O(λx. 0) = {λx. 0}"
  by (auto simp add: bigo_def)

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)
  by (smt (verit, best) abs_triangle_ineq add_mono add_pos_pos comm_semiring_class.distrib dual_order.trans)

lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
  by (simp add: antisym bigo_plus_self_subset bigo_zero set_zero_plus2)

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 (smt (verit, ccfv_threshold) mult.commute abs_triangle_ineq add_le_cancel_left dual_order.trans mult.left_commute mult_2 mult_le_cancel_iff2)
  apply (simp add: order_less_le)
  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 (metis mult_2 order.trans)
  apply simp
  done

lemma bigo_plus_subset2 [intro]: "A ⊆ O(f) ⟹ B ⊆ O(f) ⟹ A + B ⊆ O(f)"
  using bigo_plus_idemp set_plus_mono2 by blast

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)
  by (smt (verit, del_insts) add.commute abs_triangle_ineq add_mono_thms_linordered_field(3) distrib_left less_max_iff_disj linorder_not_less max.orderE max_mult_distrib_right order_le_less)

lemma bigo_bounded_alt: "∀x. 0 ≤ f x ⟹ ∀x. f x ≤ c * g x ⟹ f ∈ O(g)"
  by (simp add: bigo_def) (metis abs_mult abs_of_nonneg order_trans)

lemma bigo_bounded: "∀x. 0 ≤ f x ⟹ ∀x. f x ≤ g x ⟹ f ∈ O(g)"
  by (metis bigo_bounded_alt mult_1)

lemma bigo_bounded2: "∀x. lb x ≤ f x ⟹ ∀x. f x ≤ lb x + g x ⟹ f ∈ lb +o O(g)"
  by (simp add: add.commute bigo_bounded diff_le_eq set_minus_imp_plus)

lemma bigo_abs: "(λx. ¦f x¦) =o O(f)"
  by (smt (verit, del_insts) abs_abs bigo_def bigo_refl mem_Collect_eq)

lemma bigo_abs2: "f =o O(λx. ¦f x¦)"
  by (smt (verit, del_insts) abs_abs bigo_def bigo_refl mem_Collect_eq)

lemma bigo_abs3: "O(f) = O(λx. ¦f x¦)"
  using bigo_abs bigo_abs2 bigo_elt_subset by blast

lemma bigo_abs4: assumes "f =o g +o O(h)" shows "(λx. ¦f x¦) =o (λx. ¦g x¦) +o O(h)"
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¦)"
      by (simp add: abs_triangle_ineq3 bigo_bounded bigo_elt_subset)
    also have "… ⊆ O(f - g)"
      using bigo_abs3 by fastforce
    also from * have "… ⊆ O(h)"
      by (rule bigo_elt_subset)
    finally have "(λx. ¦f x¦ - ¦g x¦) ∈ O(h)" . }
  then show ?thesis
    by (smt (verit) assms bigo_alt_def fun_diff_def mem_Collect_eq set_minus_imp_plus set_plus_imp_minus)
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
    by (simp flip: bigo_abs3)
qed

lemma bigo_mult [intro]: "O(f)*O(g) ⊆ O(f * g)"
  apply (rule subsetI)
  apply (subst bigo_def)
  apply (clarsimp simp add: bigo_alt_def set_times_def func_times)
  apply (rule_tac x = "c * ca" in exI)
  by (smt (verit, ccfv_threshold) mult.commute mult.assoc abs_ge_zero abs_mult dual_order.trans mult_mono)

lemma bigo_mult2 [intro]: "f *o O(g) ⊆ O(f * g)"
  by (metis bigo_mult bigo_refl dual_order.trans mult.commute set_times_mono4)

lemma bigo_mult3: "f ∈ O(h) ⟹ g ∈ O(j) ⟹ f * g ∈ O(h * j)"
  using bigo_mult mult.commute mult.commute set_times_intro subsetD by blast

lemma bigo_mult4 [intro]: "f ∈ k +o O(h) ⟹ g * f ∈ (g * k) +o O(g * h)"
  by (metis bigo_mult3 bigo_refl left_diff_distrib' mult.commute set_minus_imp_plus set_plus_imp_minus)

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"
    using assms by auto
  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"
  by (simp add: assms times_fun_def)
  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"
  by (simp add: bigo_mult2 bigo_mult5 subset_antisym)

lemma bigo_mult7: "∀x. f x ≠ 0 ⟹ O(f * g) ⊆ O(f) * O(g)"
  for f :: "'a ⇒ 'b::linordered_field"
  by (metis bigo_mult6 bigo_refl mult.commute set_times_mono4)

lemma bigo_mult8: "∀x. f x ≠ 0 ⟹ O(f * g) = O(f) * O(g)"
  for f :: "'a ⇒ 'b::linordered_field"
  by (simp add: bigo_mult bigo_mult7 subset_antisym)

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

lemma bigo_minus2:
  assumes "f ∈ g +o O(h)" shows "- f ∈ -g +o O(h)"
proof -
   have "- f + g ∈ O(h)"
    by (metis assms bigo_minus minus_diff_eq set_plus_imp_minus uminus_add_conv_diff)
  then show ?thesis
    by (simp add: set_minus_imp_plus)
qed

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)"
  using assms bigo_plus_idemp set_plus_mono4 by blast

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)"
    by (simp add: set_plus_rearranges)
  finally show ?thesis .
qed

lemma bigo_plus_absorb [simp]: "f ∈ O(g) ⟹ f +o O(g) = O(g)"
  by (simp add: bigo_plus_absorb_lemma1 bigo_plus_absorb_lemma2 subset_antisym)

lemma bigo_plus_absorb2 [intro]: "f ∈ O(g) ⟹ A ⊆ O(g) ⟹ f +o A ⊆ O(g)"
  using bigo_plus_absorb set_plus_mono by blast

lemma bigo_add_commute_imp: "f ∈ g +o O(h) ⟹ g ∈ f +o O(h)"
  by (metis bigo_minus minus_diff_eq set_minus_imp_plus set_plus_imp_minus)

lemma bigo_add_commute: "f ∈ g +o O(h) ⟷ g ∈ f +o O(h)"
  using bigo_add_commute_imp by blast

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)"
  by (metis bigo_elt_subset bigo_const1)

lemma bigo_const3: "c ≠ 0 ⟹ (λx. 1) ∈ O(λx. c)"
  for c :: "'a::linordered_field"
  by (metis bigo_bounded_alt le_numeral_extra(4) nonzero_divide_eq_eq zero_less_one_class.zero_le_one)

lemma bigo_const4: "c ≠ 0 ⟹ O(λx. 1) ⊆ O(λx. c)"
  for c :: "'a::linordered_field"
  by (metis bigo_elt_subset bigo_const3)

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

lemma bigo_const_mult1: "(λx. c * f x) ∈ O(f)"
  by (smt (z3) abs_mult bigo_def bigo_refl mem_Collect_eq mult.left_commute mult_commute_abs)

lemma bigo_const_mult2: "O(λx. c * f x) ⊆ O(f)"
  by (metis bigo_elt_subset bigo_const_mult1)

lemma bigo_const_mult3: "c ≠ 0 ⟹ f ∈ O(λx. c * f x)"
  for c :: "'a::linordered_field"
  by (simp add: bigo_def) (metis abs_mult field_class.field_divide_inverse mult.commute nonzero_divide_eq_eq order_refl)

lemma bigo_const_mult4: "c ≠ 0 ⟹ O(f) ⊆ O(λx. c * f x)"
  for c :: "'a::linordered_field"
  by (simp add: bigo_const_mult3 bigo_elt_subset)

lemma bigo_const_mult [simp]: "c ≠ 0 ⟹ O(λx. c * f x) = O(f)"
  for c :: "'a::linordered_field"
  by (simp add: bigo_const_mult2 bigo_const_mult4 subset_antisym)

lemma bigo_const_mult5 [simp]: "(λx. c) *o O(f) = O(f)" if "c ≠ 0"
  for c :: "'a::linordered_field"
proof
  show "O(f) ⊆ (λx. c) *o O(f)"
    using that
    apply (clarsimp 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
  have "O(λx. c * f x) ⊆ O(f)"
    by (simp add: bigo_const_mult2)
  then show "(λx. c) *o O(f) ⊆ O(f)"
    using order_trans[OF bigo_mult2] by (force simp add: times_fun_def)
qed


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)
  by (smt (verit, ccfv_SIG) ab_semigroup_mult_class.mult_ac(1) abs_abs abs_le_self_iff abs_mult le_cases3 mult.commute mult_left_mono)

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)"
    by (simp add: func_times)
  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))"
  by (smt (verit, best) set_minus_plus bigo_def fun_diff_def mem_Collect_eq)


subsection ‹Sum›

lemma bigo_sum_main:
  assumes "∀x. ∀y ∈ A x. 0 ≤ h x y" and "∀x. ∀y ∈ A x. ¦f x y¦ ≤ c * h x y"
  shows "(λx. ∑y ∈ A x. f x y) =o O(λx. ∑y ∈ A x. h x y)"
proof -
  have "(∑i∈A x. ¦f x i¦) ≤ ¦c¦ * sum (h x) (A x)" for x
    by (smt (verit, ccfv_threshold) assms abs_mult_pos abs_of_nonneg abs_of_nonpos dual_order.trans le_cases3 neg_0_le_iff_le sum_distrib_left sum_mono)
  then show ?thesis
    using assms by (fastforce simp add: bigo_def sum_nonneg intro: order_trans [OF sum_abs])
qed

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)"
  by (metis (no_types) bigo_sum_main)

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)
  using abs_ge_zero apply blast
  apply (clarsimp simp: bigo_def)
  by (smt (verit, ccfv_threshold) abs_mult abs_not_less_zero mult.left_commute mult_le_cancel_left)

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)¦)"
  using bigo_sum3 [of "f-g" h l k A]
  apply (simp add: algebra_simps sum_subtractf)
  by (smt (verit) bigo_alt_def minus_apply set_minus_imp_plus set_plus_imp_minus mem_Collect_eq)

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))"
  using bigo_sum3 [of f h l k A] by simp

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))"
  using bigo_sum5 [of "f-g" h l k A]
  apply (simp add: algebra_simps sum_subtractf)
  by (smt (verit, del_insts) bigo_alt_def set_minus_imp_plus minus_apply set_plus_imp_minus mem_Collect_eq)


subsection ‹Misc useful stuff›

lemma bigo_useful_add: "f =o O(h) ⟹ g =o O(h) ⟹ f + g =o O(h)"
  using bigo_plus_idemp set_plus_intro by blast

lemma bigo_useful_const_mult: "c ≠ 0 ⟹ (λx. c) * f =o O(h) ⟹ f =o O(h)"
  for c :: "'a::linordered_field"
  using bigo_elt_subset bigo_mult6 by fastforce

lemma bigo_fix: "(λx::nat. f (x + 1)) =o O(λx. h (x + 1)) ⟹ f 0 = 0 ⟹ f =o O(h)"
  by (simp add: bigo_alt_def) (metis abs_eq_0_iff abs_ge_zero abs_mult abs_of_pos not0_implies_Suc)

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 [OF bigo_fix])
   apply (smt (verit, del_insts) bigo_alt_def fun_diff_def set_plus_imp_minus mem_Collect_eq)
  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)"
  by (smt (verit, del_insts) bigo_def mem_Collect_eq order_trans)

lemma bigo_lesseq2: "f =o O(h) ⟹ ∀x. ¦g x¦ ≤ f x ⟹ g =o O(h)"
  by (metis (mono_tags, lifting) abs_ge_zero abs_of_nonneg bigo_lesseq1 dual_order.trans)

lemma bigo_lesseq3: "f =o O(h) ⟹ ∀x. 0 ≤ g x ⟹ ∀x. g x ≤ f x ⟹ g =o O(h)"
  by (meson bigo_bounded bigo_elt_subset subsetD)

lemma bigo_lesseq4: "f =o O(h) ⟹ ∀x. 0 ≤ g x ⟹ ∀x. g x ≤ ¦f x¦ ⟹ g =o O(h)"
  by (metis abs_of_nonneg bigo_lesseq1)

lemma bigo_lesso1: "∀x. f x ≤ g x ⟹ f <o g =o O(h)"
  by (smt (verit, del_insts) abs_ge_zero add_0 bigo_abs3 bigo_bounded diff_le_eq lesso_def max_def order_refl)

lemma bigo_lesso2: "f =o g +o O(h) ⟹ ∀x. 0 ≤ k x ⟹ ∀x. k x ≤ f x ⟹ k <o g =o O(h)"
  unfolding lesso_def
  apply (rule bigo_lesseq4 [of "f-g"])
    apply (erule set_plus_imp_minus)
  using max.cobounded2 apply blast
  by (smt (verit) abs_ge_zero abs_of_nonneg diff_ge_0_iff_ge diff_mono diff_self fun_diff_def order_refl max.coboundedI2 max_def)

lemma bigo_lesso3: "f =o g +o O(h) ⟹ ∀x. 0 ≤ k x ⟹ ∀x. g x ≤ k x ⟹ f <o k =o O(h)"
  unfolding lesso_def
  apply (rule bigo_lesseq4 [of "f-g"])
    apply (erule set_plus_imp_minus)
  using max.cobounded2 apply blast
  by (smt (verit) abs_eq_iff abs_ge_zero abs_if abs_minus_le_zero diff_left_mono fun_diff_def le_max_iff_disj order.trans order_eq_refl)

lemma bigo_lesso4:
  fixes k :: "'a ⇒ 'b::linordered_field"
  assumes f: "f <o g =o O(k)" and g: "g =o h +o O(k)"
  shows "f <o h =o O(k)"
proof -
  have "g - h ∈ O(k)"
    by (simp add: g set_plus_imp_minus)
  then have "(λx. ¦g x - h x¦) ∈ O(k)"
    using bigo_abs5 by force
  then have §: "(λx. max (f x - g x) 0) + (λx. ¦g x - h x¦) ∈ O(k)"
    by (metis (mono_tags, lifting) bigo_lesseq1 bigo_useful_add dual_order.eq_iff f lesso_def)
  have "¦max (f x - h x) 0¦ ≤ ((λx. max (f x - g x) 0) + (λx. ¦g x - h x¦)) x" for x
    by (auto simp add: func_plus fun_diff_def algebra_simps split: split_max abs_split)
  then show ?thesis
    by (smt (verit, ccfv_SIG) § bigo_lesseq2 lesso_def)
qed


lemma bigo_lesso5:
  assumes "f <o g =o O(h)" shows "∃C. ∀x. f x ≤ g x + C * ¦h x¦"
proof -
  obtain c where "0 < c" and c: "⋀x. f x - g x ≤ c * ¦h x¦"
    using assms by (auto simp: lesso_def bigo_alt_def)
  have "¦max (f x - g x) 0¦ = max (f x - g x) 0" for x
    by (auto simp add: algebra_simps)
  then show ?thesis
    by (metis c add.commute diff_le_eq)
qed

lemma lesso_add: "f <o g =o O(h) ⟹ k <o l =o O(h) ⟹ (f + k) <o (g + l) =o O(h)"
  unfolding lesso_def
  using bigo_useful_add by (fastforce split: split_max intro: bigo_lesseq3)

lemma bigo_LIMSEQ1: "f ⇢ 0" if f: "f =o O(g)" and g: "g ⇢ 0"
  for f g :: "nat ⇒ real"
proof -
  { fix r::real
    assume "0 < r"
    obtain c::real where "0 < c"  and rc: "⋀x. ¦f x¦ ≤ c * ¦g x¦"
      using f by (auto simp: LIMSEQ_iff bigo_alt_def)
    with g ‹0 < r› obtain no where "∀n≥no. ¦g n¦ < r/c"
      by (fastforce simp: LIMSEQ_iff)
    then have "∃no. ∀n≥no. ¦f n¦ < r"
      by (metis ‹0 < c› mult.commute order_le_less_trans pos_less_divide_eq rc) }
  then show ?thesis
    by (auto simp: LIMSEQ_iff)
qed

lemma bigo_LIMSEQ2:
  fixes f g :: "nat ⇒ real"
  assumes "f =o g +o O(h)" "h ⇢ 0" and f: "f ⇢ a"
  shows  "g ⇢ a"
proof -
  have "f - g ⇢ 0"
    using assms bigo_LIMSEQ1 set_plus_imp_minus by blast
  then have "(λn. f n - g n) ⇢ 0"
    by (simp add: fun_diff_def)
  then show ?thesis
    using Lim_transform_eq f by blast
qed

end