Theory Landau_Symbols.Landau_Real_Products

(*
  File:   Landau_Real_Products.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

  Mathematical background and reification for a decision procedure for Landau symbols of
  products of powers of real functions (currently the identity and the natural logarithm)

  TODO: more functions (exp?), more preprocessing (log)
*)
section ‹Decision procedure for real functions›

theory Landau_Real_Products
imports
  Main
  "HOL-Library.Function_Algebras" 
  "HOL-Library.Set_Algebras"
  "HOL-Library.Landau_Symbols"
  Group_Sort
begin

subsection ‹Eventual non-negativity/non-zeroness›

text ‹
  For certain transformations of Landau symbols, it is required that the functions involved 
  are eventually non-negative of non-zero. In the following, we set up a system to guide the 
  simplifier to discharge these requirements during simplification at least in obvious cases.
›

definition "eventually_nonzero F f  eventually (λx. (f x :: _ :: real_normed_field)  0) F"
definition "eventually_nonneg F f  eventually (λx. (f x :: _ :: linordered_field)  0) F"

named_theorems eventually_nonzero_simps

lemmas [eventually_nonzero_simps] = 
  eventually_nonzero_def [symmetric] eventually_nonneg_def [symmetric]

lemma eventually_nonzeroD: "eventually_nonzero F f  eventually (λx. f x  0) F"
  by (simp add: eventually_nonzero_def)

lemma eventually_nonzero_const [eventually_nonzero_simps]:
  "eventually_nonzero F (λ_::_::linorder. c)  F = bot  c  0"
  unfolding eventually_nonzero_def by (auto simp add: eventually_False)

lemma eventually_nonzero_inverse [eventually_nonzero_simps]:
  "eventually_nonzero F (λx. inverse (f x))  eventually_nonzero F f"
  unfolding eventually_nonzero_def by simp

lemma eventually_nonzero_mult [eventually_nonzero_simps]:
  "eventually_nonzero F (λx. f x * g x)  eventually_nonzero F f  eventually_nonzero F g"
  unfolding eventually_nonzero_def by (simp_all add: eventually_conj_iff[symmetric])

lemma eventually_nonzero_pow [eventually_nonzero_simps]:
  "eventually_nonzero F (λx::_::linorder. f x ^ n)  n = 0  eventually_nonzero F f"
  by (induction n) (auto simp: eventually_nonzero_simps)

lemma eventually_nonzero_divide [eventually_nonzero_simps]:
  "eventually_nonzero F (λx. f x / g x)  eventually_nonzero F f  eventually_nonzero F g"
  unfolding eventually_nonzero_def by (simp_all add: eventually_conj_iff[symmetric])

lemma eventually_nonzero_ident_at_top_linorder [eventually_nonzero_simps]:
  "eventually_nonzero at_top (λx::'a::{real_normed_field,linordered_field}. x)"
  unfolding eventually_nonzero_def by simp

lemma eventually_nonzero_ident_nhds [eventually_nonzero_simps]:
  "eventually_nonzero (nhds a) (λx. x)  a  0"
  using eventually_nhds_in_open[of "-{0}" a]
  by (auto elim!: eventually_mono simp: eventually_nonzero_def open_Compl 
           dest: eventually_nhds_x_imp_x)

lemma eventually_nonzero_ident_at_within [eventually_nonzero_simps]:
  "eventually_nonzero (at a within A) (λx. x)"
  using eventually_nonzero_ident_nhds[of a]
  by (cases "a = 0") (auto simp: eventually_nonzero_def eventually_at_filter elim!: eventually_mono)

lemma eventually_nonzero_ln_at_top [eventually_nonzero_simps]:
  "eventually_nonzero at_top (λx::real. ln x)"
  unfolding eventually_nonzero_def by (auto intro!: eventually_mono[OF eventually_gt_at_top[of 1]])

lemma eventually_nonzero_ln_const_at_top [eventually_nonzero_simps]:
  "b > 0  eventually_nonzero at_top (λx. ln (b * x :: real))"
  unfolding eventually_nonzero_def 
    apply (rule eventually_mono [OF eventually_gt_at_top[of "max 1 (inverse b)"]])
  by (metis exp_ln exp_minus exp_minus_inverse less_numeral_extra(3) ln_gt_zero max_less_iff_conj mult.commute mult_strict_right_mono)

lemma eventually_nonzero_ln_const'_at_top [eventually_nonzero_simps]:
  "b > 0  eventually_nonzero at_top (λx. ln (x * b :: real))"
  using eventually_nonzero_ln_const_at_top[of b] by (simp add: mult.commute)

lemma eventually_nonzero_powr_at_top [eventually_nonzero_simps]:
  "eventually_nonzero at_top (λx::real. f x powr p)  eventually_nonzero at_top f"
  unfolding eventually_nonzero_def by simp



lemma eventually_nonneg_const [eventually_nonzero_simps]:
  "eventually_nonneg F (λ_. c)  F = bot  c  0"
  unfolding eventually_nonneg_def by (auto simp: eventually_False)

lemma eventually_nonneg_inverse [eventually_nonzero_simps]:
  "eventually_nonneg F (λx. inverse (f x))  eventually_nonneg F f"
  unfolding eventually_nonneg_def by (intro eventually_subst) (auto)

lemma eventually_nonneg_add [eventually_nonzero_simps]:
  assumes "eventually_nonneg F f" "eventually_nonneg F g"
  shows   "eventually_nonneg F (λx. f x + g x)"
  using assms unfolding eventually_nonneg_def by eventually_elim simp

lemma eventually_nonneg_mult [eventually_nonzero_simps]:
  assumes "eventually_nonneg F f" "eventually_nonneg F g"
  shows   "eventually_nonneg F (λx. f x * g x)"
  using assms unfolding eventually_nonneg_def by eventually_elim simp

lemma eventually_nonneg_mult' [eventually_nonzero_simps]:
  assumes "eventually_nonneg F (λx. -f x)" "eventually_nonneg F (λx. - g x)"
  shows   "eventually_nonneg F (λx. f x * g x)"
  using assms unfolding eventually_nonneg_def by eventually_elim (auto intro: mult_nonpos_nonpos)

lemma eventually_nonneg_divide [eventually_nonzero_simps]:
  assumes "eventually_nonneg F f" "eventually_nonneg F g"
  shows   "eventually_nonneg F (λx. f x / g x)"
  using assms unfolding eventually_nonneg_def by eventually_elim simp

lemma eventually_nonneg_divide' [eventually_nonzero_simps]:
  assumes "eventually_nonneg F (λx. -f x)" "eventually_nonneg F (λx. - g x)"
  shows   "eventually_nonneg F (λx. f x / g x)"
  using assms unfolding eventually_nonneg_def by eventually_elim (auto intro: divide_nonpos_nonpos)

lemma eventually_nonneg_ident_at_top [eventually_nonzero_simps]:
  "eventually_nonneg at_top (λx. x)" unfolding eventually_nonneg_def by (rule eventually_ge_at_top)

lemma eventually_nonneg_ident_nhds [eventually_nonzero_simps]:
  fixes a :: "'a :: {linorder_topology, linordered_field}"
  shows "a > 0  eventually_nonneg (nhds a) (λx. x)" unfolding eventually_nonneg_def
  using eventually_nhds_in_open[of "{0<..}" a]
  by (auto simp: eventually_nonneg_def dest: eventually_nhds_x_imp_x elim!: eventually_mono)

lemma eventually_nonneg_ident_at_within [eventually_nonzero_simps]:
  fixes a :: "'a :: {linorder_topology, linordered_field}"
  shows "a > 0  eventually_nonneg (at a within A) (λx. x)"
  using eventually_nonneg_ident_nhds[of a]
  by (auto simp: eventually_nonneg_def eventually_at_filter elim: eventually_mono)

lemma eventually_nonneg_pow [eventually_nonzero_simps]:
  "eventually_nonneg F f  eventually_nonneg F (λx. f x ^ n)"
  by (induction n) (auto simp: eventually_nonzero_simps)

lemma eventually_nonneg_powr [eventually_nonzero_simps]:
  "eventually_nonneg F (λx. f x powr y :: real)" by (simp add: eventually_nonneg_def)

lemma eventually_nonneg_ln_at_top [eventually_nonzero_simps]:
  "eventually_nonneg at_top (λx. ln x :: real)"
  by (auto intro!: eventually_mono[OF eventually_gt_at_top[of "1::real"]]
           simp: eventually_nonneg_def)

lemma eventually_nonneg_ln_const [eventually_nonzero_simps]:
  "b > 0  eventually_nonneg at_top (λx. ln (b*x) :: real)" 
  unfolding eventually_nonneg_def using eventually_ge_at_top[of "inverse b"]
  by eventually_elim (simp_all add: field_simps)

lemma eventually_nonneg_ln_const' [eventually_nonzero_simps]:
  "b > 0  eventually_nonneg at_top (λx. ln (x*b) :: real)" 
  using eventually_nonneg_ln_const[of b] by (simp add: mult.commute)

lemma eventually_nonzero_bigtheta':
  "f  Θ[F](g)  eventually_nonzero F f  eventually_nonzero F g"
  unfolding eventually_nonzero_def by (rule eventually_nonzero_bigtheta)

lemma eventually_nonneg_at_top: 
  assumes "filterlim f at_top F"
  shows   "eventually_nonneg F f"
proof -
  from assms have "eventually (λx. f x  0) F"
    by (simp add: filterlim_at_top)
  thus ?thesis unfolding eventually_nonneg_def by eventually_elim simp
qed

lemma eventually_nonzero_at_top: 
  assumes "filterlim (f :: 'a  'b :: {linordered_field, real_normed_field}) at_top F"
  shows   "eventually_nonzero F f"
proof -
  from assms have "eventually (λx. f x  1) F"
    by (simp add: filterlim_at_top)
  thus ?thesis unfolding eventually_nonzero_def by eventually_elim auto
qed

lemma eventually_nonneg_at_top_ASSUMPTION [eventually_nonzero_simps]:
  "ASSUMPTION (filterlim f at_top F)  eventually_nonneg F f"
  by (simp add: ASSUMPTION_def eventually_nonneg_at_top)

lemma eventually_nonzero_at_top_ASSUMPTION [eventually_nonzero_simps]:
  "ASSUMPTION (filterlim f (at_top :: 'a :: {linordered_field, real_normed_field} filter) F)  
     eventually_nonzero F f"
  using eventually_nonzero_at_top[of f F] by (simp add: ASSUMPTION_def)

lemma filterlim_at_top_iff_smallomega:
  fixes f :: "_  real"
  shows "filterlim f at_top F  f  ω[F](λ_. 1)  eventually_nonneg F f"
  unfolding eventually_nonneg_def
proof safe
  assume A: "filterlim f at_top F"
  thus B: "eventually (λx. f x  0) F" by (simp add: eventually_nonzero_simps)
  {
    fix c
    from A have "filterlim (λx. norm (f x)) at_top F"
      by (intro filterlim_at_infinity_imp_norm_at_top filterlim_at_top_imp_at_infinity) 
    hence "eventually (λx. norm (f x)  c) F" by (auto simp: filterlim_at_top)
  }
  thus "f  ω[F](λ_. 1)" by (rule landau_omega.smallI)
next
  assume A: "f  ω[F](λ_. 1)" and B: "eventually (λx. f x  0) F"
  {
    fix c :: real assume "c > 0"
    from landau_omega.smallD[OF A this] B 
      have "eventually (λx. f x  c) F" by eventually_elim simp
  }
  thus "filterlim f at_top F"
    by (subst filterlim_at_top_gt[of _ _ 0]) simp_all
qed

lemma smallomega_1_iff: 
  "eventually_nonneg F f  f  ω[F](λ_. 1 :: real)  filterlim f at_top F"
  by (simp add: filterlim_at_top_iff_smallomega)

lemma smallo_1_iff: 
  "eventually_nonneg F f  (λ_. 1 :: real)  o[F](f)  filterlim f at_top F"
  by (simp add: filterlim_at_top_iff_smallomega smallomega_iff_smallo)

lemma eventually_nonneg_add1 [eventually_nonzero_simps]:
  assumes "eventually_nonneg F f" "g  o[F](f)"
  shows   "eventually_nonneg F (λx. f x + g x :: real)"
  using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
  by eventually_elim simp_all

lemma eventually_nonneg_add2 [eventually_nonzero_simps]:
  assumes "eventually_nonneg F g" "f  o[F](g)"
  shows   "eventually_nonneg F (λx. f x + g x :: real)"
  using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
  by eventually_elim simp_all

lemma eventually_nonneg_diff1 [eventually_nonzero_simps]:
  assumes "eventually_nonneg F f" "g  o[F](f)"
  shows   "eventually_nonneg F (λx. f x - g x :: real)"
  using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
  by eventually_elim simp_all

lemma eventually_nonneg_diff2 [eventually_nonzero_simps]:
  assumes "eventually_nonneg F (λx. - g x)" "f  o[F](g)"
  shows   "eventually_nonneg F (λx. f x - g x :: real)"
  using  landau_o.smallD[OF assms(2) zero_less_one] assms(1) unfolding eventually_nonneg_def
  by eventually_elim simp_all


subsection ‹Rewriting Landau symbols›

lemma bigtheta_mult_eq: "Θ[F](λx. f x * g x) = Θ[F](f) * Θ[F](g)"
proof (intro equalityI subsetI)
  fix h assume "h  Θ[F](f) * Θ[F](g)"
  thus "h  Θ[F](λx. f x * g x)"
    by (elim set_times_elim, hypsubst, unfold func_times) (erule (1) landau_theta.mult)
next
  fix h assume "h  Θ[F](λx. f x * g x)"
  then obtain c1 c2 :: real
    where c:
      "c1 > 0" "F x in F. norm (h x)  c1 * norm (f x * g x)"
      "c2 > 0" "F x in F. c2 * norm (f x * g x)  norm (h x)"
    unfolding bigtheta_def by (blast elim: landau_o.bigE)

  define h1 h2
    where "h1 x = (if g x = 0 then if f x = 0 then if h x = 0 then h x else 1 else f x else h x / g x)"
      and "h2 x = (if g x = 0 then if f x = 0 then h x else h x / f x else g x)"
    for x

  have "h = h1 * h2" by (intro ext) (auto simp: h1_def h2_def field_simps)
  moreover have "h1  Θ[F](f)"
  proof (rule bigthetaI')
    from c(3) show "min c2 1 > 0" by simp
    from c(1) show "max c1 1 > 0" by simp
    from c(2,4) 
      show "eventually (λx. min c2 1 * (norm (f x))  norm (h1 x)  
                            norm (h1 x)  max c1 1 * (norm (f x))) F"
      apply eventually_elim
    proof (rule conjI)
      fix x assume A: "(norm (h x))  c1 * norm (f x * g x)" 
               and B: "(norm (h x))  c2 * norm (f x * g x)"
      have m: "min c2 1 * (norm (f x))  1 * (norm (f x))" by (rule mult_right_mono) simp_all
      have "min c2 1 * norm (f x * g x)  c2 * norm (f x * g x)" by (intro mult_right_mono) simp_all
      also note B
      finally show "norm (h1 x)  min c2 1 * (norm (f x))" using m A
        by (cases "g x = 0") (simp_all add: h1_def norm_mult norm_divide field_simps)+

      have m: "1 * (norm (f x))  max c1 1 * (norm (f x))" by (rule mult_right_mono) simp_all
      note A
      also have "c1 * norm (f x * g x)  max c1 1 * norm (f x * g x)" 
        by (intro mult_right_mono) simp_all
      finally show "norm (h1 x)  max c1 1 * (norm (f x))" using m A
        by (cases "g x = 0") (simp_all add: h1_def norm_mult norm_divide field_simps)+
    qed
  qed
  moreover have "h2  Θ[F](g)"
  proof (rule bigthetaI')
    from c(3) show "min c2 1 > 0" by simp
    from c(1) show "max c1 1 > 0" by simp
    from c(2,4) 
      show "eventually (λx. min c2 1 * (norm (g x))  norm (h2 x)   
                            norm (h2 x)  max c1 1 * (norm (g x))) F"
      apply eventually_elim
    proof (rule conjI)
      fix x assume A: "(norm (h x))  c1 * norm (f x * g x)" 
               and B: "(norm (h x))  c2 * norm (f x * g x)"
      have m: "min c2 1 * (norm (f x))  1 * (norm (f x))" by (rule mult_right_mono) simp_all
      have "min c2 1 * norm (f x * g x)  c2 * norm (f x * g x)" 
        by (intro mult_right_mono) simp_all
      also note B
      finally show "norm (h2 x)  min c2 1 * (norm (g x))" using m A B
        by (cases "g x = 0") (auto simp: h2_def abs_mult field_simps)+

      have m: "1 * (norm (g x))  max c1 1 * (norm (g x))" by (rule mult_right_mono) simp_all
      note A
      also have "c1 * norm (f x * g x)  max c1 1 * norm (f x * g x)" 
        by (intro mult_right_mono) simp_all
      finally show "norm (h2 x)  max c1 1 * (norm (g x))" using m A
        by (cases "g x = 0") (simp_all add: h2_def abs_mult field_simps)+
    qed
  qed
  ultimately show "h  Θ[F](f) * Θ[F](g)" by blast
qed

text ‹
  Since the simplifier does not currently rewriting with relations other than equality,
  but we want to rewrite terms like @{term "Θ(λx. log 2 x * x)"} to @{term "Θ(λx. ln x * x)"}, 
  we need to bring the term into something that contains @{term "Θ(λx. log 2 x)"} and 
  @{term "Θ(λx. x)"}, which can then be rewritten individually.
  For this, we introduce the following constants and rewrite rules. The rules are mainly used 
  by the simprocs, but may be useful for manual reasoning occasionally.
›

definition "set_mult A B = {λx. f x * g x |f g. f  A  g  B}"
definition "set_inverse A = {λx. inverse (f x) |f. f  A}"
definition "set_divide A B = {λx. f x / g x |f g. f  A  g  B}"
definition "set_pow A n = {λx. f x ^ n |f. f  A}"
definition "set_powr A y = {λx. f x powr y |f. f  A}"

lemma bigtheta_mult_eq_set_mult:
  shows "Θ[F](λx. f x * g x) = set_mult (Θ[F](f)) (Θ[F](g))"
  unfolding bigtheta_mult_eq set_mult_def set_times_def func_times by blast

lemma bigtheta_inverse_eq_set_inverse:
  shows "Θ[F](λx. inverse (f x)) = set_inverse (Θ[F](f))"
proof (intro equalityI subsetI)
  fix g :: "'a  'b" assume "g  Θ[F](λx. inverse (f x))"
  hence "(λx. inverse (g x))  Θ[F](λx. inverse (inverse (f x)))" by (subst bigtheta_inverse)
  also have "(λx. inverse (inverse (f x))) = f" by (rule ext) simp
  finally show "g  set_inverse (Θ[F](f))" unfolding set_inverse_def by force
next
  fix g :: "'a  'b" assume "g  set_inverse (Θ[F](f))"
  then obtain g' where "g = (λx. inverse (g' x))" "g'  Θ[F](f)" unfolding set_inverse_def by blast
  hence "(λx. inverse (g' x))  Θ[F](λx. inverse (f x))" by (subst bigtheta_inverse)
  also from g = (λx. inverse (g' x)) have "(λx. inverse (g' x)) = g" by (intro ext) simp
  finally show "g  Θ[F](λx. inverse (f x))" .
qed

lemma set_divide_inverse: 
  "set_divide (A :: (_  (_ :: division_ring)) set) B = set_mult A (set_inverse B)"
proof (intro equalityI subsetI)
  fix f assume "f  set_divide A B"
  then obtain g h where "f = (λx. g x / h x)" "g  A" "h  B" unfolding set_divide_def by blast
  hence "f = g * (λx. inverse (h x))" "(λx. inverse (h x))  set_inverse B"
    unfolding set_inverse_def by (auto simp: divide_inverse)
  with g  A show "f  set_mult A (set_inverse B)" unfolding set_mult_def by force
next
  fix f assume "f  set_mult A (set_inverse B)"
  then obtain g h where "f = g * (λx. inverse (h x))" "g  A" "h  B"
    unfolding set_times_def set_inverse_def set_mult_def by force
  hence "f = (λx. g x / h x)" by (intro ext) (simp add: divide_inverse)
  with g  A h  B show "f  set_divide A B" unfolding set_divide_def by blast
qed

lemma bigtheta_divide_eq_set_divide:
  shows "Θ[F](λx. f x / g x) = set_divide (Θ[F](f)) (Θ[F](g))"
  by (simp only: set_divide_inverse divide_inverse bigtheta_mult_eq_set_mult 
                 bigtheta_inverse_eq_set_inverse)

primrec bigtheta_pow where
  "bigtheta_pow F A 0 = Θ[F](λ_. 1)"
| "bigtheta_pow F A (Suc n) = set_mult A (bigtheta_pow F A n)"

lemma bigtheta_pow_eq_set_pow: "Θ[F](λx. f x ^ n) = bigtheta_pow F (Θ[F](f)) n"
  by (induction n) (simp_all add: bigtheta_mult_eq_set_mult)

definition bigtheta_powr where
  "bigtheta_powr F A y = (if y = 0 then {f. gA. eventually_nonneg F g  f  Θ[F](λx. g x powr y)} 
     else {f. gA. eventually_nonneg F g  (x. (norm (f x)) = g x powr y)})"

lemma bigtheta_powr_eq_set_powr: 
  assumes "eventually_nonneg F f"
  shows   "Θ[F](λx. f x powr (y::real)) = bigtheta_powr F (Θ[F](f)) y"
proof (cases "y = 0")
  assume [simp]: "y = 0"
  show ?thesis
  proof (intro equalityI subsetI)
    fix h assume "h  bigtheta_powr F Θ[F](f) y"
    then obtain g where g: "g  Θ[F](f)" "eventually_nonneg F g" "h  Θ[F](λx. g x powr 0)"
      unfolding bigtheta_powr_def by force
    note this(3)
    also have "(λx. g x powr 0)  Θ[F](λx. ¦g x¦ powr 0)" 
      using assms unfolding eventually_nonneg_def
      by (intro bigthetaI_cong) (auto elim!: eventually_mono)
    also from g(1) have "(λx. ¦g x¦ powr 0)  Θ[F](λx. ¦f x¦ powr 0)" 
      by (rule bigtheta_powr)
    also from g(2) have "(λx. f x powr 0)  Θ[F](λx. ¦f x¦ powr 0)" 
      unfolding eventually_nonneg_def
      by (intro bigthetaI_cong) (auto elim!: eventually_mono)
    finally show "h  Θ[F](λx. f x powr y)" by simp
  next
    fix h assume "h  Θ[F](λx. f x powr y)"
    with assms have "gΘ[F](f). eventually_nonneg F g  h  Θ[F](λx. g x powr 0)"
      by (intro bexI[of _ f] conjI) simp_all
    thus "h  bigtheta_powr F Θ[F](f) y" unfolding bigtheta_powr_def by simp
  qed
next
  assume y: "y  0"
  show ?thesis
  proof (intro equalityI subsetI)
    fix h assume h: "h  Θ[F](λx. f x powr y)"
    let ?h' = "λx. ¦h x¦ powr inverse y"
    from bigtheta_powr[OF h, of "inverse y"] y
      have "?h'  Θ[F](λx. f x powr 1)" by (simp add: powr_powr)
    also have "(λx. f x powr 1)  Θ[F](f)" using assms unfolding eventually_nonneg_def 
      by (intro bigthetaI_cong) (auto elim!: eventually_mono)
    finally have "?h'  Θ[F](f)" .
    with y have "gΘ[F](f). eventually_nonneg F g  (x. (norm (h x)) = g x powr y)"
      by (intro bexI[of _ ?h']) (simp_all add: powr_powr eventually_nonneg_def)
    thus "h  bigtheta_powr F Θ[F](f) y" using y unfolding bigtheta_powr_def by simp
  next
    fix h assume "h  bigtheta_powr F (Θ[F](f)) y"
    with y obtain g where A: "g  Θ[F](f)" "x. ¦h x¦ = g x powr y" "eventually_nonneg F g"
      unfolding bigtheta_powr_def by force
    from this(3) have "(λx. g x powr y)  Θ[F](λx. ¦g x¦ powr y)" unfolding eventually_nonneg_def
      by (intro bigthetaI_cong) (auto elim!: eventually_mono)
    also from A(1) have "(λx. ¦g x¦ powr y)  Θ[F](λx. ¦f x¦ powr y)" by (rule bigtheta_powr)
    also have "(λx. ¦f x¦ powr y)  Θ[F](λx. f x powr y)" using assms unfolding eventually_nonneg_def
      by (intro bigthetaI_cong) (auto elim!: eventually_mono)
    finally have "(λx. ¦h x¦)  Θ[F](λx. f x powr y)" by (subst A(2))
    thus "(λx. h x)  Θ[F](λx. f x powr y)" by simp
  qed
qed


lemmas bigtheta_factors_eq = 
  bigtheta_mult_eq_set_mult bigtheta_inverse_eq_set_inverse bigtheta_divide_eq_set_divide 
  bigtheta_pow_eq_set_pow bigtheta_powr_eq_set_powr

lemmas landau_bigtheta_congs = landau_symbols[THEN landau_symbol.cong_bigtheta]

lemma (in landau_symbol) meta_cong_bigtheta: "Θ[F](f)  Θ[F](g)  L F (f)  L F (g)"
  using bigtheta_refl[of f] by (intro eq_reflection cong_bigtheta) blast

lemmas landau_bigtheta_meta_congs = landau_symbols[THEN landau_symbol.meta_cong_bigtheta]


subsection ‹Preliminary facts›

lemma real_powr_at_top: 
  assumes "(p::real) > 0"
  shows   "filterlim (λx. x powr p) at_top at_top"
proof (subst filterlim_cong[OF refl refl])
  show "LIM x at_top. exp (p * ln x) :> at_top"
    by (rule filterlim_compose[OF exp_at_top filterlim_tendsto_pos_mult_at_top[OF tendsto_const]])
       (simp_all add: ln_at_top assms)
  show "eventually (λx. x powr p = exp (p * ln x)) at_top"
    using eventually_gt_at_top[of 0] by eventually_elim (simp add: powr_def)
qed

lemma tendsto_ln_over_powr: 
  assumes "(a::real) > 0"
  shows   "((λx. ln x / x powr a)  0) at_top"
proof (rule lhospital_at_top_at_top)
  from assms show "LIM x at_top. x powr a :> at_top" by (rule real_powr_at_top)
  show "eventually (λx. a * x powr (a - 1)  0) at_top"
    using eventually_gt_at_top[of "0::real"] by eventually_elim (insert assms, simp)
  show "eventually (λx::real. (ln has_real_derivative (inverse x)) (at x)) at_top"
    using eventually_gt_at_top[of "0::real"] DERIV_ln by (elim eventually_mono) simp
  show "eventually (λx. ((λx. x powr a) has_real_derivative a * x powr (a - 1)) (at x)) at_top"
    using eventually_gt_at_top[of "0::real"]
    by eventually_elim (auto intro!: derivative_eq_intros)
  have "eventually (λx. inverse a * x powr -a = inverse x / (a*x powr (a-1))) at_top"
    using eventually_gt_at_top[of "0::real"] 
    by (elim eventually_mono) (simp add: field_simps powr_diff powr_minus)
  moreover from assms have "((λx. inverse a * x powr -a)  0) at_top"
    by (intro tendsto_mult_right_zero tendsto_neg_powr filterlim_ident) simp_all
  ultimately show "((λx. inverse x / (a * x powr (a - 1)))  0) at_top"
    by (subst (asm) tendsto_cong) simp_all
qed

lemma tendsto_ln_powr_over_powr: 
  assumes "(a::real) > 0" "b > 0"
  shows   "((λx. ln x powr a / x powr b)  0) at_top"
proof-
  have "eventually (λx. ln x powr a / x powr b = (ln x / x powr (b/a)) powr a) at_top"
    using assms eventually_gt_at_top[of "1::real"]
    by (elim eventually_mono) (simp add: powr_divide powr_powr)
  moreover have "eventually (λx. 0 < ln x / x powr (b / a)) at_top"
    using eventually_gt_at_top[of "1::real"] by (elim eventually_mono) simp
  with assms have "((λx. (ln x / x powr (b/a)) powr a)  0) at_top"
    by (intro tendsto_zero_powrI tendsto_ln_over_powr) (simp_all add: eventually_mono)
  ultimately show ?thesis by (subst tendsto_cong) simp_all
qed

lemma tendsto_ln_powr_over_powr': 
  assumes "b > 0"
  shows   "((λx::real. ln x powr a / x powr b)  0) at_top"
proof (cases "a  0")
  assume a: "a  0"
  show ?thesis
  proof (rule tendsto_sandwich[of "λ_::real. 0"])
    have "eventually (λx. ln x powr a  1) at_top" unfolding eventually_at_top_linorder
    proof (intro allI exI impI)
      fix x :: real assume x: "x  exp 1"
      have "0 < exp (1::real)" by simp
      also have "  x" by fact
      finally have "ln x  ln (exp 1)" using x by (subst ln_le_cancel_iff) auto
      hence "ln x powr a  ln (exp 1) powr a" using a by (intro powr_mono2') simp_all
      thus "ln x powr a  1" by simp
    qed
    thus "eventually (λx. ln x powr a / x powr b  x powr -b) at_top"
      by eventually_elim (insert a, simp add: field_simps powr_minus divide_right_mono)
  qed (auto intro!: filterlim_ident tendsto_neg_powr assms)
qed (intro tendsto_ln_powr_over_powr, simp_all add: assms)

lemma tendsto_ln_over_ln:
  assumes "(a::real) > 0" "c > 0"
  shows   "((λx. ln (a*x) / ln (c*x))  1) at_top"
proof (rule lhospital_at_top_at_top)
  show "LIM x at_top. ln (c*x) :> at_top"
    by (intro filterlim_compose[OF ln_at_top] filterlim_tendsto_pos_mult_at_top[OF tendsto_const] 
              filterlim_ident assms(2))
  show "eventually (λx. ((λx. ln (a*x)) has_real_derivative (inverse x)) (at x)) at_top"
    using eventually_gt_at_top[of "inverse a"] assms
    by (auto elim!: eventually_mono intro!: derivative_eq_intros simp: field_simps)
  show "eventually (λx. ((λx. ln (c*x)) has_real_derivative (inverse x)) (at x)) at_top"
    using eventually_gt_at_top[of "inverse c"] assms
    by (auto elim!: eventually_mono intro!: derivative_eq_intros simp: field_simps)
  show "((λx::real. inverse x / inverse x)  1) at_top"
    by (subst tendsto_cong[of _ "λ_. 1"]) simp_all
qed simp_all

lemma tendsto_ln_powr_over_ln_powr:
  assumes "(a::real) > 0" "c > 0"
  shows   "((λx. ln (a*x) powr d / ln (c*x) powr d)  1) at_top"
proof-
  have "eventually (λx. ln (a*x) powr d / ln (c*x) powr d = (ln (a*x) / ln (c*x)) powr d) at_top"
    using assms eventually_gt_at_top[of "max (inverse a) (inverse c)"]
    by (auto elim!: eventually_mono simp: powr_divide field_simps)
  moreover have "((λx. (ln (a*x) / ln (c*x)) powr d)  1) at_top" using assms
    by (intro tendsto_eq_rhs[OF tendsto_powr[OF tendsto_ln_over_ln tendsto_const]]) simp_all
  ultimately show ?thesis by (subst tendsto_cong)
qed

lemma tendsto_ln_powr_over_ln_powr': 
  "c > 0  ((λx::real. ln x powr d / ln (c*x) powr d)  1) at_top"
  using tendsto_ln_powr_over_ln_powr[of 1 c d] by simp

lemma tendsto_ln_powr_over_ln_powr'': 
  "a > 0  ((λx::real. ln (a*x) powr d / ln x powr d)  1) at_top"
  using tendsto_ln_powr_over_ln_powr[of _ 1] by simp

lemma bigtheta_const_ln_powr [simp]: "a > 0  (λx::real. ln (a*x) powr d)  Θ(λx. ln x powr d)"
  by (intro bigthetaI_tendsto[of 1] tendsto_ln_powr_over_ln_powr'') simp

lemma bigtheta_const_ln_pow [simp]: "a > 0  (λx::real. ln (a*x) ^ d)  Θ(λx. ln x ^ d)"
proof-
  assume a: "a > 0"
  have "F x in at_top. ln (a * x) ^ d = ln (a * x) powr real d"
    using eventually_gt_at_top[of "1/a"] 
    by eventually_elim (insert a, subst powr_realpow, auto simp: field_simps)
  hence "(λx::real. ln (a*x) ^ d)  Θ(λx. ln (a*x) powr real d)"
    by (rule bigthetaI_cong)
  also from a have "(λx. ln (a*x) powr real d)  Θ(λx. ln x powr real d)" by simp
  also have "F x in at_top. ln x powr real d = ln x ^ d"
    using eventually_gt_at_top[of 1] 
    by eventually_elim (subst powr_realpow, auto simp: field_simps)
  hence "(λx. ln x powr real d)  Θ(λx. ln x ^ d)"
    by (rule bigthetaI_cong)
  finally show ?thesis .
qed

lemma bigtheta_const_ln [simp]: "a > 0  (λx::real. ln (a*x))  Θ(λx. ln x)"
  using tendsto_ln_over_ln[of a 1]  by (intro bigthetaI_tendsto[of 1]) simp_all


text ‹
  If there are two functions @{term "f"} and @{term "g"} where any power of @{term "g"} is
  asymptotically smaller than @{term "f"}, propositions like @{term "(λx. f x ^ p1 * g x ^ q1) 
  O(λx. f x ^ p2 * g x ^ q2)"} can be decided just by looking at the exponents:
  the proposition is true iff @{term "p1 < p2"} or @{term "p1 = p2  q1  q2"}.

  The functions @{term "λx. x"}, @{term "λx. ln x"}, @{term "λx. ln (ln x)"}, $\ldots$
  form a chain in which every function dominates all succeeding functions in the above sense,
  allowing to decide propositions involving Landau symbols and functions that are products of
  powers of functions from this chain by reducing the proposition to a statement involving only
  logical connectives and comparisons on the exponents.

  We will now give the mathematical background for this and implement reification to bring
  functions from this class into a canonical form, allowing the decision procedure to be
  implemented in a simproc.
›

subsection ‹Decision procedure›

definition "powr_closure f  {λx. f x powr p :: real |p. True}"

lemma powr_closureI [simp]: "(λx. f x powr p)  powr_closure f"
  unfolding powr_closure_def by force

lemma powr_closureE:
  assumes "g  powr_closure f"
  obtains p where "g = (λx. f x powr p)"
  using assms unfolding powr_closure_def by force


locale landau_function_family =
  fixes F :: "'a filter" and H :: "('a  real) set"
  assumes F_nontrivial: "F  bot"
  assumes pos: "h  H  eventually (λx. h x > 0) F"
  assumes linear: "h1  H  h2  H  h1  o[F](h2)  h2  o[F](h1)  h1  Θ[F](h2)"
  assumes mult: "h1  H  h2  H  (λx. h1 x * h2 x)  H"
  assumes inverse: "h  H  (λx. inverse (h x))  H"
begin

lemma div: "h1  H  h2  H  (λx. h1 x / h2 x)  H"
  by (subst divide_inverse) (intro mult inverse)

lemma nonzero: "h  H  eventually (λx. h x  0) F"
  by (drule pos) (auto elim: eventually_mono)

lemma landau_cases:
  assumes "h1  H" "h2  H"
  obtains "h1  o[F](h2)" | "h2  o[F](h1)" | "h1  Θ[F](h2)"
  using linear[OF assms] by blast

lemma small_big_antisym:
  assumes "h1  H" "h2  H" "h1  o[F](h2)" "h2  O[F](h1)" shows False
proof-
  from nonzero[OF assms(1)] nonzero[OF assms(2)] landau_o.small_big_asymmetric[OF assms(3,4)]
    have "eventually (λ_::'a. False) F" by eventually_elim simp
  thus False by (simp add: eventually_False F_nontrivial)
qed

lemma small_antisym:
  assumes "h1  H" "h2  H" "h1  o[F](h2)" "h2  o[F](h1)" shows False
  using assms by (blast intro: small_big_antisym landau_o.small_imp_big)

end

locale landau_function_family_pair =
  G: landau_function_family F G + H: landau_function_family F H for F G H +
  fixes g
  assumes gs_dominate: "g1  G  g2  G  h1  H  h2  H  g1  o[F](g2) 
     (λx. g1 x * h1 x)  o[F](λx. g2 x * h2 x)"
  assumes g: "g  G"
  assumes g_dominates: "h  H  h  o[F](g)"
begin

sublocale GH: landau_function_family F "G * H"
proof (unfold_locales; (elim set_times_elim; hypsubst)?)
  fix g h assume "g  G" "h  H"
  from G.pos[OF this(1)] H.pos[OF this(2)] show "eventually (λx. (g*h) x > 0) F"
    by eventually_elim simp
next
  fix g h assume A: "g  G" "h  H"
  have "(λx. inverse ((g * h) x)) = (λx. inverse (g x)) * (λx. inverse (h x))" by (rule ext) simp
  also from A have "...  G * H" by (intro G.inverse H.inverse set_times_intro)
  finally show "(λx. inverse ((g * h) x))  G * H" .
next
  fix g1 g2 h1 h2 assume A: "g1  G" "g2  G" "h1  H" "h2  H"
  from gs_dominate[OF this] gs_dominate[OF this(2,1,4,3)]
       G.linear[OF this(1,2)] H.linear[OF this(3,4)]
    show "g1 * h1  o[F](g2 * h2)  g2 * h2  o[F](g1 * h1)  g1 * h1  Θ[F](g2 * h2)"
    by (elim disjE) (force simp: func_times bigomega_iff_bigo intro: landau_theta.mult
         landau_o.small.mult landau_o.small_big_mult landau_o.big_small_mult)+
  have B: "(λx. (g1 * h1) x * (g2 * h2) x) = (g1 * g2) * (h1 * h2)"
    by (rule ext) (simp add: func_times mult_ac)
  from A show "(λx. (g1 * h1) x * (g2 * h2) x)  G * H"
    by (subst B, intro set_times_intro) (auto intro: G.mult H.mult simp: func_times)
qed (fact G.F_nontrivial)

lemma smallo_iff:
  assumes "g1  G" "g2  G" "h1  H" "h2  H"
  shows "(λx. g1 x * h1 x)  o[F](λx. g2 x * h2 x) 
             g1  o[F](g2)  (g1  Θ[F](g2)  h1  o[F](h2))" (is "?P  ?Q")
proof (rule G.landau_cases[OF assms(1,2)])
  assume "g1  o[F](g2)"
  thus ?thesis by (auto intro!: gs_dominate assms)
next
  assume A: "g1  Θ[F](g2)"
  hence B: "g2  O[F](g1)" by (subst (asm) bigtheta_sym) (rule bigthetaD1)
  hence "g1  o[F](g2)" using assms by (auto dest: G.small_big_antisym)
  moreover from A have "o[F](λx. g2 x * h2 x) = o[F](λx. g1 x * h2 x)"
    by (intro landau_o.small.cong_bigtheta landau_theta.mult_right, subst bigtheta_sym)
  ultimately show ?thesis using G.nonzero[OF assms(1)] A
    by (auto simp add: landau_o.small.mult_cancel_left)
next
  assume A: "g2  o[F](g1)"
  from gs_dominate[OF assms(2,1,4,3) this] have B: "g2 * h2  o[F](g1 * h1)" by (simp add: func_times)
  have "g1  o[F](g2)" "g1  Θ[F](g2)" using assms A
    by (auto dest: G.small_antisym G.small_big_antisym simp: bigomega_iff_bigo)
  moreover have "¬?P"
    by (intro notI GH.small_antisym[OF _ _ B] set_times_intro) (simp_all add: func_times assms)
  ultimately show ?thesis by blast
qed

lemma bigo_iff:
  assumes "g1  G" "g2  G" "h1  H" "h2  H"
  shows "(λx. g1 x * h1 x)  O[F](λx. g2 x * h2 x) 
             g1  o[F](g2)  (g1  Θ[F](g2)  h1  O[F](h2))" (is "?P  ?Q")
proof (rule G.landau_cases[OF assms(1,2)])
  assume "g1  o[F](g2)"
  thus ?thesis by (auto intro!: gs_dominate assms landau_o.small_imp_big)
next
  assume A: "g2  o[F](g1)"
  hence "g1  O[F](g2)" using assms by (auto dest: G.small_big_antisym)
  moreover from gs_dominate[OF assms(2,1,4,3) A] have "g2*h2  o[F](g1*h1)" by (simp add: func_times)
  hence "g1*h1  O[F](g2*h2)" by (blast intro: GH.small_big_antisym assms)
  ultimately show ?thesis using A assms
    by (auto simp: func_times dest: landau_o.small_imp_big)
next
  assume A: "g1  Θ[F](g2)"
  hence "g1  o[F](g2)" unfolding bigtheta_def using assms
    by (auto dest: G.small_big_antisym simp: bigomega_iff_bigo)
  moreover have "O[F](λx. g2 x * h2 x) = O[F](λx. g1 x * h2 x)"
    by (subst landau_o.big.cong_bigtheta[OF landau_theta.mult_right[OF A]]) (rule refl)
  ultimately show ?thesis using A G.nonzero[OF assms(2)]
    by (auto simp: landau_o.big.mult_cancel_left eventually_nonzero_bigtheta)
qed

lemma bigtheta_iff:
  "g1  G  g2  G  h1  H  h2  H 
    (λx. g1 x * h1 x)  Θ[F](λx. g2 x * h2 x)  g1  Θ[F](g2)  h1  Θ[F](h2)"
  by (auto simp: bigtheta_def bigo_iff bigomega_iff_bigo intro: landau_o.small_imp_big
           dest: G.small_antisym G.small_big_antisym)

end


lemma landau_function_family_powr_closure:
  assumes "F  bot" "filterlim f at_top F"
  shows   "landau_function_family F (powr_closure f)"
proof (unfold_locales; (elim powr_closureE; hypsubst)?)
  from assms have "eventually (λx. f x  1) F" using filterlim_at_top by auto
  hence A: "eventually (λx. f x  0) F" by eventually_elim simp
  {
    fix p q :: real
    show "(λx. f x powr p)  o[F](λx. f x powr q) 
          (λx. f x powr q)  o[F](λx. f x powr p) 
          (λx. f x powr p)  Θ[F](λx. f x powr q)"
    by (cases p q rule: linorder_cases)
       (force intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric]  assms A)+
  }
  fix p
  show "eventually (λx. f x powr p > 0) F" using A by simp
qed (auto simp: powr_add[symmetric] powr_minus[symmetric] F  bot intro: powr_closureI)

lemma landau_function_family_pair_trans:
  assumes "landau_function_family_pair Ftr F G f"
  assumes "landau_function_family_pair Ftr G H g"
  shows   "landau_function_family_pair Ftr F (G*H) f"
proof-
  interpret FG: landau_function_family_pair Ftr F G f by fact
  interpret GH: landau_function_family_pair Ftr G H g by fact
  show ?thesis
  proof (unfold_locales; (elim set_times_elim)?; (clarify)?;
         (unfold func_times mult.assoc[symmetric])?)
    fix f1 f2 g1 g2 h1 h2
    assume A: "f1  F" "f2  F" "g1  G" "g2  G" "h1  H" "h2  H" "f1  o[Ftr](f2)"

    from A have "(λx. f1 x * g1 x * h1 x)  o[Ftr](λx. f1 x * g1 x * g x)"
      by (intro landau_o.small.mult_left GH.g_dominates)
    also have "(λx. f1 x * g1 x * g x) = (λx. f1 x * (g1 x * g x))" by (simp only: mult.assoc)
    also from A have "...  o[Ftr](λx. f2 x * (g2 x / g x))"
      by (intro FG.gs_dominate FG.H.mult FG.H.div GH.g)
    also from A have "(λx. inverse (h2 x))  o[Ftr](g)" by (intro GH.g_dominates GH.H.inverse)
    with GH.g A have "(λx. f2 x * (g2 x / g x))  o[Ftr](λx. f2 x * (g2 x * h2 x))"
      by (auto simp: FG.H.nonzero GH.H.nonzero divide_inverse
               intro!: landau_o.small.mult_left intro: landau_o.small.inverse_flip)
    also have "... = o[Ftr](λx. f2 x * g2 x * h2 x)" by (simp only: mult.assoc)
    finally show "(λx. f1 x * g1 x * h1 x)  o[Ftr](λx. f2 x * g2 x * h2 x)" .
  next
    fix g1 h1 assume A: "g1  G" "h1  H"
    hence "(λx. g1 x * h1 x)  o[Ftr](λx. g1 x * g x)"
      by (intro landau_o.small.mult_left GH.g_dominates)
    also from A have "(λx. g1 x * g x)  o[Ftr](f)" by (intro FG.g_dominates FG.H.mult GH.g)
    finally show "(λx. g1 x * h1 x)  o[Ftr](f)" .
  qed (simp_all add: FG.g)
qed

lemma landau_function_family_pair_trans_powr:
  assumes "landau_function_family_pair F (powr_closure g) H (λx. g x powr 1)"
  assumes "filterlim f at_top F"
  assumes "p. (λx. g x powr p)  o[F](f)"
  shows   "landau_function_family_pair F (powr_closure f) (powr_closure g * H) (λx. f x powr 1)"
proof (rule landau_function_family_pair_trans[OF _ assms(1)])
  interpret GH: landau_function_family_pair F "powr_closure g" H "λx. g x powr 1" by fact
  interpret F: landau_function_family F "powr_closure f"
    by (rule landau_function_family_powr_closure) (rule GH.G.F_nontrivial, rule assms)
  show "landau_function_family_pair F (powr_closure f) (powr_closure g) (λx. f x powr 1)"
  proof (unfold_locales; (elim powr_closureE; hypsubst)?)
    show "(λx. f x powr 1)  powr_closure f" by (rule powr_closureI)
  next
    fix p ::real
    note assms(3)[of p]
    also from assms(2) have "eventually (λx. f x  1) F" by (force simp: filterlim_at_top)
    hence "f  Θ[F](λx. f x powr 1)" by (auto intro!: bigthetaI_cong elim!: eventually_mono)
    finally show "(λx. g x powr p)  o[F](λx. f x powr 1)" .
  next
    fix p p1 p2 p3 :: real
    assume A: "(λx. f x powr p)  o[F](λx. f x powr p1)"
    have p: "p < p1"
    proof (cases p p1 rule: linorder_cases)
      assume "p > p1"
      moreover from assms(2) have "eventually (λx. f x  1) F"
        by (force simp: filterlim_at_top)
      hence "eventually (λx. f x  0) F" by eventually_elim simp
      ultimately have "(λx. f x powr p1)  o[F](λx. f x powr p)" using assms
        by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
      from F.small_antisym[OF _ _ this A] show ?thesis by (auto simp: powr_closureI)
    next
      assume "p = p1"
      hence "(λx. f x powr p1)  O[F](λx. f x powr p)" by (intro bigthetaD1) simp
      with F.small_big_antisym[OF _ _ A this] show ?thesis by (auto simp: powr_closureI)
    qed

    from assms(2) have f_pos: "eventually (λx. f x  1) F" by (force simp: filterlim_at_top)
    from assms have "(λx. g x powr ((p2 - p3)/(p1 - p)))  o[F](f)" by simp
    from smallo_powr[OF this, of "p1 - p"] p
      have "(λx. g x powr (p2 - p3))  o[F](λx. ¦f x¦ powr (p1 - p))" by (simp add: powr_powr)
    hence "(λx. ¦f x¦ powr p * g x powr p2)  o[F](λx. ¦f x¦ powr p1 * g x powr p3)" (is ?P)
      using GH.G.nonzero[OF GH.g] F.nonzero[OF powr_closureI]
      by (simp add: powr_diff landau_o.small.divide_eq1
                    landau_o.small.divide_eq2 mult.commute)
    also have "?P  (λx. f x powr p * g x powr p2)  o[F](λx. f x powr p1 * g x powr p3)"
      using f_pos by (intro landau_o.small.cong_ex) (auto elim!: eventually_mono)
    finally show "(λx. f x powr p * g x powr p2)  o[F](λx. f x powr p1 * g x powr p3)" .
  qed
qed


definition dominates :: "'a filter  ('a  real)  ('a  real)  bool" where
  "dominates F f g = (p. (λx. g x powr p)  o[F](f))"

lemma dominates_trans:
  assumes "eventually (λx. g x > 0) F"
  assumes "dominates F f g" "dominates F g h"
  shows   "dominates F f h"
unfolding dominates_def
proof
  fix p :: real
  from assms(3) have "(λx. h x powr p)  o[F](g)" unfolding dominates_def by simp
  also from assms(1) have "g  Θ[F](λx. g x powr 1)"
    by (intro bigthetaI_cong) (auto elim!: eventually_mono)
  also from assms(2) have "(λx. g x powr 1)  o[F](f)"
    using dominates_def by blast
  finally show "(λx. h x powr p)  o[F](f)" .
qed

fun landau_dominating_chain where
  "landau_dominating_chain F (f # g # gs) 
    dominates F f g  landau_dominating_chain F (g # gs)"
| "landau_dominating_chain F [f]  (λx. 1)  o[F](f)"
| "landau_dominating_chain F []  True"

primrec landau_dominating_chain' where
  "landau_dominating_chain' F []  True"
| "landau_dominating_chain' F (f # gs) 
    landau_function_family_pair F (powr_closure f) (prod_list (map powr_closure gs)) (λx. f x powr 1) 
    landau_dominating_chain' F gs"



primrec nonneg_list where
  "nonneg_list []  True"
| "nonneg_list (x#xs)  x > 0  (x = 0  nonneg_list xs)"

primrec pos_list where
  "pos_list []  False"
| "pos_list (x#xs)  x > 0  (x = 0  pos_list xs)"


lemma dominating_chain_imp_dominating_chain':
  "Ftr  bot  (g. g  set gs  filterlim g at_top Ftr) 
     landau_dominating_chain Ftr gs  landau_dominating_chain' Ftr gs"
proof (induction gs rule: landau_dominating_chain.induct)
  case (1 F f g gs)
  from 1 show ?case
    by (auto intro!: landau_function_family_pair_trans_powr simp add: dominates_def simp flip: powr_one')
next
  case (2 F f)
  then interpret F: landau_function_family F "powr_closure f"
    by (intro landau_function_family_powr_closure) simp_all
  from 2 have "eventually (λx. f x  1) F" by (force simp: filterlim_at_top)
  hence "o[F](λx. f x powr 1) = o[F](λx. f x)"
    by (intro landau_o.small.cong) (auto elim!: eventually_mono)
  with 2 have "landau_function_family_pair F (powr_closure f) {λ_. 1} (λx. f x powr 1)"
    by unfold_locales (auto intro: powr_closureI simp flip: powr_one')
  thus ?case by (simp add: one_fun_def)
next
  case 3
  then show ?case by simp
qed


locale landau_function_family_chain =
  fixes F :: "'b filter"
  fixes gs :: "'a list"
  fixes get_param :: "'a  real"
  fixes get_fun :: "'a  ('b  real)"
  assumes F_nontrivial: "F  bot"
  assumes gs_pos: "g  set (map get_fun gs)  filterlim g at_top F"
  assumes dominating_chain: "landau_dominating_chain F (map get_fun gs)"
begin

lemma dominating_chain': "landau_dominating_chain' F (map get_fun gs)"
  by (intro dominating_chain_imp_dominating_chain' gs_pos dominating_chain F_nontrivial)

lemma gs_powr_0_eq_one:
  "eventually (λx. (ggs. get_fun g x powr 0) = 1) F"
using gs_pos
proof (induction gs)
  case (Cons g gs)
  from Cons have "eventually (λx. get_fun g x > 0) F" by (auto simp: filterlim_at_top_dense)
  moreover from Cons have "eventually (λx. (ggs. get_fun g x powr 0) = 1) F" by simp
  ultimately show ?case by eventually_elim simp
qed simp_all

lemma listmap_gs_in_listmap:
  "(λx. gfs. h g x powr p g)  prod_list (map powr_closure (map h fs))"
proof-
  have "(λx. gfs. h g x powr p g) = (gfs. (λx. h g x powr p g))"
    by (rule ext, induction fs) simp_all
  also have "...  prod_list (map powr_closure (map h fs))"
    apply (induction fs)
    apply (simp add: fun_eq_iff)
    apply (simp only: list.map prod_list.Cons, rule set_times_intro)
    apply simp_all
    done
  finally show ?thesis .
qed

lemma smallo_iff:
  "(λ_. 1)  o[F](λx. ggs. get_fun g x powr get_param g)  pos_list (map get_param gs)"
proof-
  have "((λ_. 1)  o[F](λx. ggs. get_fun g x powr get_param g)) 
          ((λx. ggs. get_fun g x powr 0)  o[F](λx. ggs. get_fun g x powr get_param g))"
    by (rule sym, intro landau_o.small.in_cong gs_powr_0_eq_one)
  also from gs_pos dominating_chain' have "...  pos_list (map get_param gs)"
  proof (induction gs)
    case Nil
    have "(λx::'b. 1::real)  o[F](λx. 1)" using F_nontrivial
      by (auto dest!: landau_o.small_big_asymmetric)
    thus ?case by simp
  next
    case (Cons g gs)
    then interpret G: landau_function_family_pair F "powr_closure (get_fun g)"
       "prod_list (map powr_closure (map get_fun gs))" "λx. get_fun g x powr 1" by simp
    from Cons show ?case using listmap_gs_in_listmap[of get_fun _ gs] F_nontrivial
      by (simp_all add: G.smallo_iff listmap_gs_in_listmap powr_smallo_iff powr_bigtheta_iff
                   del: powr_zero_eq_one)
  qed
  finally show ?thesis .
qed

lemma bigo_iff:
  "(λ_. 1)  O[F](λx. ggs. get_fun g x powr get_param g)  nonneg_list (map get_param gs)"
proof-
  have "((λ_. 1)  O[F](λx. ggs. get_fun g x powr get_param g)) 
          ((λx. ggs. get_fun g x powr 0)  O[F](λx. ggs. get_fun g x powr get_param g))"
    by (rule sym, intro landau_o.big.in_cong gs_powr_0_eq_one)
  also from gs_pos dominating_chain' have "...  nonneg_list (map get_param gs)"
  proof (induction gs)
    case Nil
    then show ?case by (simp add: func_one)
  next
    case (Cons g gs)
    then interpret G: landau_function_family_pair F "powr_closure (get_fun g)"
       "prod_list (map powr_closure (map get_fun gs))" "λx. get_fun g x powr 1" by simp
    from Cons show ?case using listmap_gs_in_listmap[of get_fun _ gs] F_nontrivial
      by (simp_all add: G.bigo_iff listmap_gs_in_listmap powr_smallo_iff powr_bigtheta_iff
                   del: powr_zero_eq_one)
  qed
  finally show ?thesis .
qed

lemma bigtheta_iff:
  "(λ_. 1)  Θ[F](λx. ggs. get_fun g x powr get_param g)  list_all ((=) 0) (map get_param gs)"
proof-
  have "((λ_. 1)  Θ[F](λx. ggs. get_fun g x powr get_param g)) 
          ((λx. ggs. get_fun g x powr 0)  Θ[F](λx. ggs. get_fun g x powr get_param g))"
    by (rule sym, intro landau_theta.in_cong gs_powr_0_eq_one)
  also from gs_pos dominating_chain' have "...  list_all ((=) 0) (map get_param gs)"
  proof (induction gs)
    case Nil
    then show ?case by (simp add: func_one)
  next
    case (Cons g gs)
    then interpret G: landau_function_family_pair F "powr_closure (get_fun g)"
       "prod_list (map powr_closure (map get_fun gs))" "λx. get_fun g x powr 1" by simp
    from Cons show ?case using listmap_gs_in_listmap[of get_fun _ gs] F_nontrivial
      by (simp_all add: G.bigtheta_iff listmap_gs_in_listmap powr_smallo_iff powr_bigtheta_iff
                   del: powr_zero_eq_one)
  qed
  finally show ?thesis .
qed

end



lemma fun_chain_at_top_at_top:
  assumes "filterlim (f :: ('a::order)  'a) at_top at_top"
  shows   "filterlim (f ^^ n) at_top at_top"
  by (induction n) (auto intro: filterlim_ident filterlim_compose[OF assms])

lemma const_smallo_ln_chain: "(λ_. 1)  o((ln::realreal)^^n)"
proof (intro smalloI_tendsto)
  show "((λx::real. 1 / (ln^^n) x)  0) at_top"
    by (rule tendsto_divide_0 tendsto_const filterlim_at_top_imp_at_infinity
             fun_chain_at_top_at_top ln_at_top)+
next
  from fun_chain_at_top_at_top[OF ln_at_top, of n]
    have "eventually (λx::real. (ln^^n) x > 0) at_top" by (simp add: filterlim_at_top_dense)
  thus "eventually (λx::real. (ln^^n) x  0) at_top" by eventually_elim simp_all
qed

lemma ln_fun_in_smallo_fun:
  assumes "filterlim f at_top at_top"
  shows   "(λx. ln (f x) powr p :: real)  o(f)"
proof (rule smalloI_tendsto)
  have "((λx. ln x powr p / x powr 1)  0) at_top" by (rule tendsto_ln_powr_over_powr') simp
  moreover have "eventually (λx. ln x powr p / x powr 1 = ln x powr p / x) at_top"
    using eventually_gt_at_top[of "0::real"] by eventually_elim simp
  ultimately have "((λx. ln x powr p / x)  0) at_top" by (subst (asm) tendsto_cong)
  from this assms show "((λx. ln (f x) powr p / f x)  0) at_top"
    by (rule filterlim_compose)
  from assms have "eventually (λx. f x  1) at_top" by (simp add: filterlim_at_top)
  thus "eventually (λx. f x  0) at_top" by eventually_elim simp
qed

lemma ln_chain_dominates: "m > n  dominates at_top ((ln::real  real)^^n) (ln^^m)"
proof (erule less_Suc_induct)
  fix n show "dominates at_top ((ln::realreal)^^n) (ln^^(Suc n))" unfolding dominates_def
    by (force intro: ln_fun_in_smallo_fun fun_chain_at_top_at_top ln_at_top)
next
  fix k m n
  assume A: "dominates at_top ((ln::real  real)^^k) (ln^^m)"
            "dominates at_top ((ln::real  real)^^m) (ln^^n)"
  from fun_chain_at_top_at_top[OF ln_at_top, of m]
    have "eventually (λx::real. (ln^^m) x > 0) at_top" by (simp add: filterlim_at_top_dense)
  from this A show "dominates at_top ((ln::real  real)^^k) ((ln::real  real)^^n)"
    by (rule dominates_trans)
qed






datatype primfun = LnChain nat

instantiation primfun :: linorder
begin