src/HOL/Real_Asymp/Real_Asymp_Examples.thy

   shows   "(f \<longlongrightarrow> 0) at_top" (is ?thesis1)
           "f \<sim> (\<lambda>x. -(ln x ^ 2) / (2*x))" (is ?thesis2)
   unfolding f_def by real_asymp+
 
   
-subsection \<open>Asymptotic inequalities related to the Akra–Bazzi theorem\<close>
+subsection \<open>Asymptotic inequalities related to the Akra--Bazzi theorem\<close>
   
 definition "akra_bazzi_asymptotic1 b hb e p x \<longleftrightarrow>
   (1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))
   \<ge> 1 + (ln x powr (-e/2) :: real)"
 definition "akra_bazzi_asymptotic1' b hb e p x \<longleftrightarrow>