Theory Landau_Symbols.Landau_More

(*
  File:   Landau_More.thy
  Author: Andreas Lochbihler, Manuel Eberl <manuel@pruvisto.org>

  Some more facts about Landau symbols.
*)
theory Landau_More
imports
  "HOL-Library.Landau_Symbols"
  Landau_Simprocs
begin

(* Additional theorems, contributed by Andreas Lochbihler and adapted by Manuel Eberl *)

lemma bigo_const_inverse [simp]:
  assumes "filterlim f at_top F" "F  bot"
  shows "(λ_. c)  O[F](λx. inverse (f x) :: real)  c = 0"
proof -
  {
    assume A: "(λ_. 1)  O[F](λx. inverse (f x))"
    from assms have "(λ_. 1)  o[F](f)"
      by (simp add: eventually_nonzero_simps smallomega_iff_smallo filterlim_at_top_iff_smallomega)
    also from assms A have "f  O[F](λ_. 1)"
      by (simp add: eventually_nonzero_simps landau_divide_simps)
    finally have False using assms by (simp add: landau_o.small_refl_iff)
  }
  thus ?thesis by (cases "c = 0") auto
qed
 
lemma smallo_const_inverse [simp]:
  "filterlim f at_top F  F  bot  (λ_. c :: real)  o[F](λx. inverse (f x))  c = 0"
  by (auto dest: landau_o.small_imp_big)

lemma const_in_smallo_const [simp]: "(λ_. b)  o(λ_ :: _ :: linorder. c)  b = 0" (is "?lhs  ?rhs")
  by (cases "b = 0"; cases "c = 0") (simp_all add: landau_o.small_refl_iff)

lemma smallomega_1_conv_filterlim: "f  ω[F](λ_. 1)  filterlim f at_infinity F"
  by (auto intro: smallomegaI_filterlim_at_infinity dest: smallomegaD_filterlim_at_infinity)
  
lemma bigtheta_powr_1 [landau_simp]: 
  "eventually (λx. (f x :: real)  0) F  (λx. f x powr 1)  Θ[F](f)"
  by (intro bigthetaI_cong) (auto elim!: eventually_mono)

lemma bigtheta_powr_0 [landau_simp]: 
  "eventually (λx. (f x :: real)  0) F  (λx. f x powr 0)  Θ[F](λ_. 1)"
  by (intro bigthetaI_cong) (auto elim!: eventually_mono)

lemma bigtheta_powr_nonzero [landau_simp]: 
  "eventually (λx. (f x :: real)  0) F  (λx. if f x = 0 then g x else h x)  Θ[F](h)"
  by (intro bigthetaI_cong) (auto elim!: eventually_mono)

lemma bigtheta_powr_nonzero' [landau_simp]: 
  "eventually (λx. (f x :: real)  0) F  (λx. if f x  0 then g x else h x)  Θ[F](g)"
  by (intro bigthetaI_cong) (auto elim!: eventually_mono)

lemma bigtheta_powr_nonneg [landau_simp]: 
  "eventually (λx. (f x :: real)  0) F  (λx. if f x  0 then g x else h x)  Θ[F](g)"
  by (intro bigthetaI_cong) (auto elim!: eventually_mono)

lemma bigtheta_powr_nonneg' [landau_simp]: 
  "eventually (λx. (f x :: real)  0) F  (λx. if f x < 0 then g x else h x)  Θ[F](h)"
  by (intro bigthetaI_cong) (auto elim!: eventually_mono)    

lemma bigo_powr_iff:
  assumes "0 < p" "eventually (λx. f x  0) F" "eventually (λx. g x  0) F"
  shows "(λx. (f x :: real) powr p)  O[F](λx. g x powr p)  f  O[F](g)" (is "?lhs  ?rhs")
proof
  assume ?lhs
  with assms bigo_powr[OF this, of "inverse p"] show ?rhs 
    by (simp add: powr_powr landau_simps)
qed (insert assms, simp_all add: bigo_powr_nonneg)

lemma inverse_powr [simp]:
  assumes "(x::real)  0"
  shows   "inverse x powr y = inverse (x powr y)"
proof (cases "x > 0")
  assume x: "x > 0"
  from x have "inverse x powr y = exp (y * ln (inverse x))" by (simp add: powr_def)
  also have "ln (inverse x) = -ln x" by (simp add: x ln_inverse)
  also have "exp (y * -ln x) = inverse (exp (y * ln x))" by (simp add: exp_minus)
  also from x have "exp (y * ln x) = x powr y" by (simp add: powr_def)
  finally show ?thesis .
qed (insert assms, simp)

lemma bigo_neg_powr_iff:
  assumes "p < 0" "eventually (λx. f x  0) F" "eventually (λx. g x  0) F"
                  "eventually (λx. f x  0) F" "eventually (λx. g x  0) F"
  shows "(λx. (f x :: real) powr p)  O[F](λx. g x powr p)  g  O[F](f)" (is "?lhs  ?rhs")
proof -
  have "(λx. f x powr p)  O[F](λx. g x powr p) 
          (λx. (inverse (f x)) powr -p)  O[F](λx. (inverse (g x)) powr -p)"
    using assms by (intro landau_o.big.cong_ex) (auto simp: powr_minus elim: eventually_mono)
  also from assms have "  ((λx. inverse (f x))  O[F](λx. inverse (g x)))"
    by (subst bigo_powr_iff) simp_all
  also from assms have "  g  O[F](f)" by (simp add: landau_o.big.inverse_cancel)
  finally show ?thesis .
qed

lemma smallo_powr_iff:
  assumes "0 < p" "eventually (λx. f x  0) F" "eventually (λx. g x  0) F"
  shows "(λx. (f x :: real) powr p)  o[F](λx. g x powr p)  f  o[F](g)" (is "?lhs  ?rhs")
proof
  assume ?lhs
  with assms smallo_powr[OF this, of "inverse p"] show ?rhs 
    by (simp add: powr_powr landau_simps)
qed (insert assms, simp_all add: smallo_powr_nonneg)

lemma smallo_neg_powr_iff:
  assumes "p < 0" "eventually (λx. f x  0) F" "eventually (λx. g x  0) F"
                  "eventually (λx. f x  0) F" "eventually (λx. g x  0) F"
  shows "(λx. (f x :: real) powr p)  o[F](λx. g x powr p)  g  o[F](f)" (is "?lhs  ?rhs")
proof -
  have "(λx. f x powr p)  o[F](λx. g x powr p) 
          (λx. (inverse (f x)) powr -p)  o[F](λx. (inverse (g x)) powr -p)"
    using assms by (intro landau_o.small.cong_ex) (auto simp: powr_minus elim: eventually_mono)
  also from assms have "  ((λx. inverse (f x))  o[F](λx. inverse (g x)))"
    by (subst smallo_powr_iff) simp_all
  also from assms have "  g  o[F](f)" by (simp add: landau_o.small.inverse_cancel)
  finally show ?thesis .
qed    

lemma const_smallo_powr:
  assumes "filterlim f at_top F" "F  bot"
  shows "(λ_. c :: real)  o[F](λx. f x powr p)  p > 0  c = 0"
  by (rule linorder_cases[of p 0]; cases "c = 0")
     (insert assms smallo_powr_iff[of p "λ_. 1" F f] smallo_neg_powr_iff[of p f F "λ_. 1"],
      auto simp: landau_simps eventually_nonzero_simps smallo_1_iff[of F f] not_less 
           dest: landau_o.small_asymmetric simp: eventually_False landau_o.small_refl_iff)

lemma bigo_const_powr:
  assumes "filterlim f at_top F" "F  bot"
  shows "(λ_. c :: real)  O[F](λx. f x powr p)  p  0  c = 0"
proof -
  from assms have A: "(λ_. 1)  o[F](f)"
    by (simp add: filterlim_at_top_iff_smallomega smallomega_iff_smallo landau_o.small_imp_big)
  hence B: "(λ_. 1)  O[F](f)" "f  O[F](λ_. 1)" using assms
    by (auto simp: landau_o.small_imp_big dest: landau_o.small_big_asymmetric)
  show ?thesis
    by (rule linorder_cases[of p 0]; cases "c = 0")
       (insert insert assms A B bigo_powr_iff[of p "λ_. 1" F f] bigo_neg_powr_iff[of p "λ_. 1" F f],
        auto simp: landau_simps eventually_nonzero_simps not_less dest: landau_o.small_asymmetric)
qed

lemma filterlim_powr_at_top:
  "(b::real) > 1  filterlim (λx. b powr x) at_top at_top"
  unfolding powr_def mult.commute[of _ "ln b"]
  by (auto intro!: filterlim_compose[OF exp_at_top] 
        filterlim_tendsto_pos_mult_at_top filterlim_ident)

lemma power_smallo_exponential:
  fixes b :: real
  assumes b: "b > 1"
  shows "(λx. x powr n)  o(λx. b powr x)"
proof (rule smalloI_tendsto)
  from assms have "filterlim (λx. x * ln b - n * ln x) at_top at_top" 
    using [[simproc add: simplify_landau_sum]]
    by (simp add: filterlim_at_top_iff_smallomega eventually_nonzero_simps)
  hence "((λx. exp (-(x * ln b - n * ln x)))  0) at_top" (is ?A)
    by (intro filterlim_compose[OF exp_at_bot] 
              filterlim_compose[OF filterlim_uminus_at_bot_at_top])
  also have "?A  ((λx. x powr n / b powr x)  0) at_top"
    using b eventually_gt_at_top[of 0]
    by (intro tendsto_cong) 
       (auto simp: exp_diff powr_def field_simps exp_of_nat_mult elim: eventually_mono)
  finally show "((λx. x powr n / b powr x)  0) at_top" .
qed (insert assms, simp_all add: eventually_nonzero_simps)

lemma powr_fast_growth_tendsto:
  assumes gf: "g  O[F](f)"
  and n: "n  0"
  and k: "k > 1"
  and f: "filterlim f at_top F"
  and g: "eventually (λx. g x  0) F"
  shows "(λx. g x powr n)  o[F](λx. k powr f x :: real)"
proof -
  from f have f': "eventually (λx. f x  0) F" by (simp add: eventually_nonzero_simps)
  from gf obtain c where c: "c > 0" "eventually (λx. norm (g x)  c * norm (f x)) F" 
    by (elim landau_o.bigE)
  from c(2) g f' have "eventually (λx. g x  c * f x) F" by eventually_elim simp
  from c(2) g f' have "eventually (λx. norm (g x powr n)  norm (c powr n * f x powr n)) F"
    by eventually_elim (insert n c(1), auto simp: powr_mult [symmetric] intro!: powr_mono2)
  from landau_o.big_mono[OF this] c(1) 
    have "(λx. g x powr n)  O[F](λx. f x powr n)" by simp
  also from power_smallo_exponential f
    have "(λx. f x powr n)  o[F](λx. k powr f x)" by (rule landau_o.small.compose) fact+
  finally show ?thesis .
qed

(* lemma bigo_const_inverse [simp]:
  "filterlim f at_top at_top ⟹ (λ_ :: _ :: linorder. c) ∈ O(λx. inverse (f x)) ⟷ c = 0"
  for f :: "_ ⇒ real"
by simp

lemma smallo_const_inverse [simp]:
  "filterlim f at_top at_top ⟹ (λ_ :: _ :: linorder. c) ∈ o(λx. inverse (f x)) ⟷ c = 0"
  for f :: "_ ⇒ real"
by(simp)
 *)
lemma bigo_abs_powr_iff [simp]:
  "0 < p  (λx. ¦f x :: real¦ powr p)  O[F](λx. ¦g x¦ powr p)  f  O[F](g)"
  by(subst bigo_powr_iff; simp)

lemma smallo_abs_powr_iff [simp]:
  "0 < p  (λx. ¦f x :: real¦ powr p)  o[F](λx. ¦g x¦ powr p)  f  o[F](g)"
  by(subst smallo_powr_iff; simp)

lemma const_smallo_inverse_powr:
  assumes "filterlim f at_top at_top"
  shows "(λ_ :: _ :: linorder. c :: real)  o(λx. inverse (f x powr p))  (p  0  c = 0)"
proof(cases p "0 :: real" rule: linorder_cases)
  case p: greater
  have "(λ_. c)  o(λx. inverse (f x powr p))  (λ_. ¦c¦)  o(λx. inverse (f x powr p))" by simp
  also have "¦c¦ = ¦(¦c¦ powr (inverse p))¦ powr p" using p by(simp add: powr_powr)
  also { have "eventually (λx. f x  0) at_top" using assms by(simp add: filterlim_at_top)
    then have "o(λx. inverse (f x powr p)) = o(λx. ¦inverse (f x)¦ powr p)"
      by(intro landau_o.small.cong)(auto elim!: eventually_rev_mp)
    also have "(λ_. ¦(¦c¦ powr inverse p)¦ powr p)    (λ_. ¦c¦ powr (inverse p))  o(λx. inverse (f x))"
      using p by(rule smallo_abs_powr_iff)
    also note calculation }
  also have "(λ_. ¦c¦ powr (inverse p))  o(λx. inverse (f x))  c = 0" using assms by simp
  finally show ?thesis using p by simp
next
  case equal
  from assms have "eventually (λx. f x  1) at_top" using assms by(simp add: filterlim_at_top)
  then have "o(λx. inverse (f x powr p)) = o(λx. 1)"
    by(intro landau_o.small.cong)(auto simp add: equal elim!: eventually_rev_mp)
  then show ?thesis using equal by simp
next
  case less
  from assms have nonneg: "F x in at_top. 0  f x" by(simp add: filterlim_at_top)
  with assms have "F x in at_top. ¦¦c¦ powr (1 / - p)¦ / d  ¦f x¦" (is "F x in _. ?c  _") if "d > 0" for d
    by(fastforce dest!: spec[where x="?c"] simp add: filterlim_at_top elim: eventually_rev_mp)
  then have "(λ_. ¦c¦ powr (1 / - p))  o(f)" by(intro landau_o.smallI)(simp add: field_simps)
  then have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p)  o(λx. ¦f x¦ powr - p)"
    using less by(subst smallo_powr_iff) simp_all
  also have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p) = (λ_. ¦c¦)" using less by(simp add: powr_powr)
  also have "o(λx. ¦f x¦ powr - p) = o(λx. f x powr - p)" using nonneg
    by(auto intro!: landau_o.small.cong elim: eventually_rev_mp)
  finally have "(λ_. c)  o(λx. f x powr - p)" by simp
  with less show ?thesis by(simp add: powr_minus[symmetric])
qed

lemma bigo_const_inverse_powr:
  assumes "filterlim f at_top at_top"
  shows "(λ_ :: _ :: linorder. c :: real)  O(λx. inverse (f x powr p))  c = 0  p  0"
proof(cases p "0 :: real" rule: linorder_cases)
  case p_pos: greater
  have "(λ_. c)  O(λx. inverse (f x powr p))  (λ_. ¦c¦)  O(λx. inverse (f x powr p))" by simp
  also have "¦c¦ = ¦(¦c¦ powr inverse p)¦ powr p" using p_pos by(simp add: powr_powr)
  also { have "eventually (λx. f x  0) at_top" using assms by(simp add: filterlim_at_top)
    then have "O(λx. inverse (f x powr p)) = O(λx. ¦inverse (f x)¦ powr p)"
      by(intro landau_o.big.cong)(auto elim!: eventually_rev_mp)
    also have "(λ_. ¦(¦c¦ powr inverse p)¦ powr p)    
                 (λ_. ¦c¦ powr (inverse p))  O(λx. inverse (f x))"
      using p_pos by (rule bigo_abs_powr_iff)
    also note calculation }
  also have "(λ_. ¦c¦ powr (inverse p))  O(λx. inverse (f x))  c = 0" using assms by simp
  finally show ?thesis using p_pos by simp
next
  case equal
  from assms have "eventually (λx. f x  1) at_top" using assms by(simp add: filterlim_at_top)
  then have "O(λx. inverse (f x powr p)) = O(λx. 1)"
    by(intro landau_o.big.cong) (auto simp add: equal elim!: eventually_rev_mp)
  then show ?thesis using equal by simp
next
  case less
  from assms have *: "F x in at_top. 1  f x" by(simp add: filterlim_at_top)
  then have "(λ_. ¦c¦ powr (1 / - p))  O(f)" 
    by(intro bigoI[where c="¦c¦ powr (1 / - p)"])
      (auto intro: order_trans[OF _ mult_left_mono, rotated] elim!: eventually_rev_mp[OF _ always_eventually])
  then have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p)  O(λx. ¦f x¦ powr - p)"
    using less by (subst bigo_powr_iff) simp_all
  also have "(λ_. ¦¦c¦ powr (1 / - p)¦ powr - p) = (λ_. ¦c¦)" using less by(simp add: powr_powr)
  also have "O(λx. ¦f x¦ powr - p) = O(λx. f x powr - p)" using *
    by (auto intro!: landau_o.big.cong elim: eventually_rev_mp)
  finally have "(λ_. c)  O(λx. f x powr - p)" by simp
  thus ?thesis using less by (simp add: powr_minus[symmetric])
qed

end