Theory More_Asymptotics

theory More_Asymptotics
  imports
   "Asymptotics_1D"
   "Asymptotics_2D"
   "HOL-Real_Asymp.Real_Asymp"
begin

(* by Manuel Eberl *)
lemma dlog[asym_bound]:  "(λx. real (Discrete.log x)) ∈ Θ(λx. ln (real x))"
proof -
  have "(λx. real (Discrete.log x))  ∈ Θ(λn. real (nat ⌊log 2 (real n)⌋))"
    by (intro bigthetaI_cong eventually_mono[OF eventually_gt_at_top[of 0]])
       (auto simp: Discrete.log_altdef)
  also have "(λn. real (nat ⌊log 2 (real n)⌋)) ∈ Θ(λx. ln (real x))"
    by real_asymp
  finally show ?thesis .
qed

end