Theory Landau_More

theory Landau_More
imports Landau_Simprocs
(*
  File:   Landau_More.thy
  Author: Andreas Lochbihler, Manuel Eberl <eberlm@in.tum.de>

  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