Theory Real_Asymp_Examples

section ‹Examples for the ‹real_asymp› method›
theory Real_Asymp_Examples
  imports Real_Asymp
begin

context
  includes asymp_equiv_notation
begin

subsection ‹Dominik Gruntz's examples›

lemma "((λx::real. exp x * (exp (1/x - exp (-x)) - exp (1/x))) ⤏ -1) at_top"
  by real_asymp
  
lemma "((λx::real. exp x * (exp (1/x + exp (-x) + exp (-(x^2))) -
                     exp (1/x - exp (-exp x)))) ⤏ 1) at_top"
  by real_asymp
  
lemma "filterlim (λx::real. exp (exp (x - exp (-x)) / (1 - 1/x)) - exp (exp x)) at_top at_top"
  by real_asymp

text ‹This example is notable because it produces an expansion of level 9.›
lemma "filterlim (λx::real. exp (exp (exp x / (1 - 1/x))) - 
                    exp (exp (exp x / (1 - 1/x - ln x powr (-ln x))))) at_bot at_top"
  by real_asymp

lemma "filterlim (λx::real. exp (exp (exp (x + exp (-x)))) / exp (exp (exp x))) at_top at_top"
  by real_asymp

lemma "filterlim (λx::real. exp (exp (exp x)) / (exp (exp (exp (x - exp (-exp x)))))) at_top at_top"
  by real_asymp

lemma "((λx::real. exp (exp (exp x)) / exp (exp (exp x - exp (-exp (exp x))))) ⤏ 1) at_top"
  by real_asymp

lemma "((λx::real. exp (exp x) / exp (exp x - exp (-exp (exp x)))) ⤏ 1) at_top"
  by real_asymp

lemma "filterlim (λx::real. ln x ^ 2 * exp (sqrt (ln x) * ln (ln x) ^ 2 * 
         exp (sqrt (ln (ln x)) * ln (ln (ln x)) ^ 3)) / sqrt x) (at_right 0) at_top"
  by real_asymp

lemma "((λx::real. (x * ln x * ln (x * exp x - x^2) ^ 2) / 
                    ln (ln (x^2 + 2*exp (exp (3*x^3*ln x))))) ⤏ 1/3) at_top"
  by real_asymp

lemma "((λx::real. (exp (x * exp (-x) / (exp (-x) + exp (-(2*x^2)/(x+1)))) - exp x) / x)
          ⤏ -exp 2) at_top"
  by real_asymp
  
lemma "((λx::real. (3 powr x + 5 powr x) powr (1/x)) ⤏ 5) at_top"
  by real_asymp
 
lemma "filterlim (λx::real. x / (ln (x powr (ln x powr (ln 2 / ln x))))) at_top at_top"
  by real_asymp

lemma "filterlim (λx::real. exp (exp (2*ln (x^5 + x) * ln (ln x))) / 
                     exp (exp (10*ln x * ln (ln x)))) at_top at_top"
  by real_asymp

lemma "filterlim (λx::real. 4/9 * (exp (exp (5/2*x powr (-5/7) + 21/8*x powr (6/11) + 
              2*x powr (-8) + 54/17*x powr (49/45))) ^ 8) / (ln (ln (-ln (4/3*x powr (-5/14))))))
         at_top at_top"
  by real_asymp

lemma "((λx::real. (exp (4*x*exp (-x) / 
                    (1/exp x + 1/exp (2*x^2/(x+1)))) - exp x) / ((exp x)^4)) ⤏ 1) at_top "
  by real_asymp

lemma "((λx::real. exp (x*exp (-x) / (exp (-x) + exp (-2*x^2/(x+1))))/exp x) ⤏ 1) at_top"
  by real_asymp

lemma "((λx::real. exp (exp (-x/(1+exp (-x)))) * exp (-x/(1+exp (-x/(1+exp (-x))))) * 
           exp (exp (-x+exp (-x/(1+exp (-x))))) / (exp (-x/(1+exp (-x))))^2 - exp x + x) 
         ⤏ 2) at_top"
  by real_asymp

lemma "((λx::real. (ln(ln x + ln (ln x)) - ln (ln x)) / 
                      (ln (ln x + ln (ln (ln x)))) * ln x) ⤏ 1) at_top"
  by real_asymp
  
lemma "((λx::real. exp (ln (ln (x + exp (ln x * ln (ln x)))) / 
                       (ln (ln (ln (exp x + x + ln x)))))) ⤏ exp 1) at_top"
  by real_asymp

lemma "((λx::real. exp x * (sin (1/x + exp (-x)) - sin (1/x + exp (-(x^2))))) ⤏ 1) at_top"
  by real_asymp

lemma "((λx::real. exp (exp x) * (exp (sin (1/x + exp (-exp x))) - exp (sin (1/x)))) ⤏ 1) at_top"
  by real_asymp

lemma "((λx::real. max x (exp x) / ln (min (exp (-x)) (exp (-exp x)))) ⤏ -1) at_top"
  by real_asymp

text ‹The following example is taken from the paper by Richardson ∗‹et al›.›
lemma 
  defines "f ≡ (λx::real. ln (ln (x * exp (x * exp x) + 1)) - exp (exp (ln (ln x) + 1 / x)))"
  shows   "(f ⤏ 0) at_top" (is ?thesis1)
          "f ∼ (λx. -(ln x ^ 2) / (2*x))" (is ?thesis2)
  unfolding f_def by real_asymp+

  
subsection ‹Asymptotic inequalities related to the Akra--Bazzi theorem›
  
definition "akra_bazzi_asymptotic1 b hb e p x ⟷
  (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))
  ≥ 1 + (ln x powr (-e/2) :: real)"
definition "akra_bazzi_asymptotic1' b hb e p x ⟷
  (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))
  ≥ 1 + (ln x powr (-e/2) :: real)"
definition "akra_bazzi_asymptotic2 b hb e p x ⟷
  (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))
      ≤ 1 - ln x powr (-e/2 :: real)"
definition "akra_bazzi_asymptotic2' b hb e p x ⟷
  (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))
      ≤ 1 - ln x powr (-e/2 :: real)"
definition "akra_bazzi_asymptotic3 e x ⟷ (1 + (ln x powr (-e/2))) / 2 ≤ (1::real)"
definition "akra_bazzi_asymptotic4 e x ⟷ (1 - (ln x powr (-e/2))) * 2 ≥ (1::real)"
definition "akra_bazzi_asymptotic5 b hb e x ⟷ 
  ln (b*x - hb*x*ln x powr -(1+e)) powr (-e/2::real) < 1"

definition "akra_bazzi_asymptotic6 b hb e x ⟷ hb / ln x powr (1 + e :: real) < b/2"
definition "akra_bazzi_asymptotic7 b hb e x ⟷ hb / ln x powr (1 + e :: real) < (1 - b) / 2"
definition "akra_bazzi_asymptotic8 b hb e x ⟷ x*(1 - b - hb / ln x powr (1 + e :: real)) > 1"

definition "akra_bazzi_asymptotics b hb e p x ⟷
  akra_bazzi_asymptotic1 b hb e p x ∧ akra_bazzi_asymptotic1' b hb e p x ∧
  akra_bazzi_asymptotic2 b hb e p x ∧ akra_bazzi_asymptotic2' b hb e p x ∧
  akra_bazzi_asymptotic3 e x ∧ akra_bazzi_asymptotic4 e x ∧ akra_bazzi_asymptotic5 b hb e x ∧
  akra_bazzi_asymptotic6 b hb e x ∧ akra_bazzi_asymptotic7 b hb e x ∧ 
  akra_bazzi_asymptotic8 b hb e x"

lemmas akra_bazzi_asymptotic_defs = 
  akra_bazzi_asymptotic1_def akra_bazzi_asymptotic1'_def 
  akra_bazzi_asymptotic2_def akra_bazzi_asymptotic2'_def akra_bazzi_asymptotic3_def
  akra_bazzi_asymptotic4_def akra_bazzi_asymptotic5_def akra_bazzi_asymptotic6_def
  akra_bazzi_asymptotic7_def akra_bazzi_asymptotic8_def akra_bazzi_asymptotics_def
  
lemma akra_bazzi_asymptotics:
  assumes "⋀b. b ∈ set bs ⟹ b ∈ {0<..<1}" and "e > 0"
  shows "eventually (λx. ∀b∈set bs. akra_bazzi_asymptotics b hb e p x) at_top"
proof (intro eventually_ball_finite ballI)
  fix b assume "b ∈ set bs"
  with assms have "b ∈ {0<..<1}" by simp
  with ‹e > 0› show "eventually (λx. akra_bazzi_asymptotics b hb e p x) at_top"
    unfolding akra_bazzi_asymptotic_defs 
    by (intro eventually_conj; real_asymp simp: mult_neg_pos)
qed simp
  
lemma
  fixes b ε :: real
  assumes "b ∈ {0<..<1}" and "ε > 0"
  shows "filterlim (λx. (1 - H / (b * ln x powr (1 + ε))) powr p * 
           (1 + ln (b * x + H * x / ln x powr (1+ε)) powr (-ε/2)) - 
           (1 + ln x powr (-ε/2))) (at_right 0) at_top"
  using assms by (real_asymp simp: mult_neg_pos)

context
  fixes b e p :: real
  assumes assms: "b > 0" "e > 0"
begin

lemmas [simp] = mult_neg_pos

real_limit "(λx. ((1 - 1 / (b * ln x powr (1 + e))) powr p * 
               (1 + ln (b * x +  x / ln x powr (1+e)) powr (-e/2)) - 
               (1 + ln x powr (-e/2))) * ln x powr ((e / 2) + 1))"
  facts: assms

end

context
  fixes b ε :: real
  assumes assms: "b > 0" "ε > 0" "ε < 1 / 4"
begin

real_expansion "(λx. (1 - H / (b * ln x powr (1 + ε))) powr p * 
           (1 + ln (b * x + H * x / ln x powr (1+ε)) powr (-ε/2)) - 
           (1 + ln x powr (-ε/2)))"
  terms: 10 (strict)
  facts: assms

end

context
  fixes e :: real
  assumes e: "e > 0" "e < 1 / 4"
begin

real_expansion "(λx. (1 - 1 / (1/2 * ln x powr (1 + e))) * 
           (1 + ln (1/2 * x + x / ln x powr (1+e)) powr (-e/2)) - 
           (1 + ln x powr (-e/2)))"
  terms: 10 (strict)
  facts: e

end


subsection ‹Concrete Mathematics›
  
text ‹The following inequalities are discussed on p.\ 441 in Concrete Mathematics.›
lemma 
  fixes c ε :: real
  assumes "0 < ε" "ε < 1" "1 < c"
    shows "(λ_::real. 1) ∈ o(λx. ln (ln x))"
      and "(λx::real. ln (ln x)) ∈ o(λx. ln x)"
      and "(λx::real. ln x) ∈ o(λx. x powr ε)"
      and "(λx::real. x powr ε) ∈ o(λx. x powr c)"
      and "(λx. x powr c) ∈ o(λx. x powr ln x)"
      and "(λx. x powr ln x) ∈ o(λx. c powr x)"
      and "(λx. c powr x) ∈ o(λx. x powr x)"
      and "(λx. x powr x) ∈ o(λx. c powr (c powr x))"
  using assms by (real_asymp (verbose))+

    
subsection ‹Stack Exchange›

text ‹
  http://archives.math.utk.edu/visual.calculus/1/limits.15/
›
lemma "filterlim (λx::real. (x * sin x) / abs x) (at_right 0) (at 0)"
  by real_asymp

lemma "filterlim (λx::real. x^2 / (sqrt (x^2 + 12) - sqrt (12))) (nhds (12 / sqrt 3)) (at 0)"
proof -
  note [simp] = powr_half_sqrt sqrt_def (* TODO: Better simproc for sqrt/root? *)
  have "sqrt (12 :: real) = sqrt (4 * 3)"
    by simp
  also have "… = 2 * sqrt 3" by (subst real_sqrt_mult) simp
  finally show ?thesis by real_asymp
qed


text ‹🌐‹http://math.stackexchange.com/questions/625574››
lemma "(λx::real. (1 - 1/2 * x^2 - cos (x / (1 - x^2))) / x^4) ─0→ 23/24"
  by real_asymp


text ‹🌐‹http://math.stackexchange.com/questions/122967››

real_limit "λx. (x + 1) powr (1 + 1 / x) - x powr (1 + 1 / (x + a))"

lemma "((λx::real. ((x + 1) powr (1 + 1/x) - x powr (1 + 1 / (x + a)))) ⤏ 1) at_top"
  by real_asymp


real_limit "λx. x ^ 2 * (arctan x - pi / 2) + x"

lemma "filterlim (λx::real. x^2 * (arctan x - pi/2) + x) (at_right 0) at_top"
  by real_asymp


real_limit "λx. (root 3 (x ^ 3 + x ^ 2 + x + 1) - sqrt (x ^ 2 + x + 1) * ln (exp x + x) / x)"

lemma "((λx::real. root 3 (x^3 + x^2 + x + 1) - sqrt (x^2 + x + 1) * ln (exp x + x) / x)
           ⤏ -1/6) at_top"
  by real_asymp


context
  fixes a b :: real
  assumes ab: "a > 0" "b > 0"
begin
real_limit "λx. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)"
  limit: "at_right 0" facts: ab
real_limit "λx. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)"
  limit: "at_left 0" facts: ab
lemma "(λx. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2))
         ─0→ exp (ln a * ln a / 2 - ln b * ln b / 2)" using ab by real_asymp
end


text ‹🌐‹http://math.stackexchange.com/questions/547538››
lemma "(λx::real. ((x+4) powr (3/2) + exp x - 9) / x) ─0→ 4"
  by real_asymp

text ‹🌐‹https://www.freemathhelp.com/forum/threads/93513››
lemma "((λx::real. ((3 powr x + 4 powr x) / 4) powr (1/x)) ⤏ 4) at_top"
  by real_asymp
    
lemma "((λx::real. x powr (3/2) * (sqrt (x + 1) + sqrt (x - 1) - 2 * sqrt x)) ⤏ -1/4) at_top"
  by real_asymp


text ‹🌐‹https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/limcondirectory/LimitConstant.html››
lemma  "(λx::real. (cos (2*x) - 1) / (cos x - 1)) ─0→ 4"
  by real_asymp

lemma "(λx::real. tan (2*x) / (x - pi/2)) ─pi/2→ 2"
  by real_asymp


text ‹@url{"https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/liminfdirectory/LimitInfinity.html"}›
lemma "filterlim (λx::real. (3 powr x + 3 powr (2*x)) powr (1/x)) (nhds 9) at_top"
  using powr_def[of 3 "2::real"] by real_asymp

text ‹🌐‹https://www.math.ucdavis.edu/~kouba/CalcOneDIRECTORY/lhopitaldirectory/LHopital.html››
lemma "filterlim (λx::real. (x^2 - 1) / (x^2 + 3*x - 4)) (nhds (2/5)) (at 1)"
  by real_asymp
    
lemma "filterlim (λx::real. (x - 4) / (sqrt x - 2)) (nhds 4) (at 4)"
  by real_asymp
    
lemma "filterlim (λx::real. sin x / x) (at_left 1) (at 0)"
  by real_asymp

lemma "filterlim (λx::real. (3 powr x - 2 powr x) / (x^2 - x)) (nhds (ln (2/3))) (at 0)"
  by (real_asymp simp: ln_div)
    
lemma "filterlim (λx::real. (1/x - 1/3) / (x^2 - 9)) (nhds (-1/54)) (at 3)"
  by real_asymp

lemma "filterlim (λx::real. (x * tan x) / sin (3*x)) (nhds 0) (at 0)"
  by real_asymp

lemma "filterlim (λx::real. sin (x^2) / (x * tan x)) (at 1) (at 0)"
  by real_asymp

lemma "filterlim (λx::real. (x^2 * exp x) / tan x ^ 2) (at 1) (at 0)"
  by real_asymp

lemma "filterlim (λx::real. exp (-1/x^2) / x^2) (at 0) (at 0)"
  by real_asymp

lemma "filterlim (λx::real. exp x / (5 * x + 200)) at_top at_top"
  by real_asymp
    
lemma "filterlim (λx::real. (3 + ln x) / (x^2 + 7)) (at 0) at_top"
  by real_asymp

lemma "filterlim (λx::real. (x^2 + 3*x - 10) / (7*x^2 - 5*x + 4)) (at_right (1/7)) at_top"
  by real_asymp

lemma "filterlim (λx::real. (ln x ^ 2) / exp (2*x)) (at_right 0) at_top"
  by real_asymp
    
lemma "filterlim (λx::real. (3 * x + 2 powr x) / (2 * x + 3 powr x)) (at 0) at_top"
  by real_asymp
    
lemma "filterlim (λx::real. (exp x + 2 / x) / (exp x + 5 / x)) (at_left 1) at_top"
  by real_asymp
    
lemma "filterlim (λx::real. sqrt (x^2 + 1) - sqrt (x + 1)) at_top at_top"
  by real_asymp

  
lemma "filterlim (λx::real. x * ln x) (at_left 0) (at_right 0)"
  by real_asymp

lemma "filterlim (λx::real. x * ln x ^ 2) (at_right 0) (at_right 0)"
  by real_asymp

lemma "filterlim (λx::real. ln x * tan x) (at_left 0) (at_right 0)"
  by real_asymp

lemma "filterlim (λx::real. x powr sin x) (at_left 1) (at_right 0)"
  by real_asymp

lemma "filterlim (λx::real. (1 + 3 / x) powr x) (at_left (exp 3)) at_top"
  by real_asymp

lemma "filterlim (λx::real. (1 - x) powr (1 / x)) (at_left (exp (-1))) (at_right 0)"
  by real_asymp

lemma "filterlim (λx::real. (tan x) powr x^2) (at_left 1) (at_right 0)"
  by real_asymp

lemma "filterlim (λx::real. x powr (1 / sqrt x)) (at_right 1) at_top"
  by real_asymp

lemma "filterlim (λx::real. ln x powr (1/x)) (at_right 1) at_top"
  by (real_asymp (verbose))

lemma "filterlim (λx::real. x powr (x powr x)) (at_right 0) (at_right 0)"
  by (real_asymp (verbose))


text ‹🌐‹http://calculus.nipissingu.ca/problems/limit_problems.html››
lemma "((λx::real. (x^2 - 1) / ¦x - 1¦) ⤏ -2) (at_left 1)"
      "((λx::real. (x^2 - 1) / ¦x - 1¦) ⤏ 2) (at_right 1)"
  by real_asymp+

lemma "((λx::real. (root 3 x - 1) / ¦sqrt x - 1¦) ⤏ -2 / 3) (at_left 1)"
      "((λx::real. (root 3 x - 1) / ¦sqrt x - 1¦) ⤏ 2 / 3) (at_right 1)"
  by real_asymp+


text ‹🌐‹https://math.stackexchange.com/questions/547538››

lemma "(λx::real. ((x + 4) powr (3/2) + exp x - 9) / x) ─0→ 4"
  by real_asymp

text ‹🌐‹https://math.stackexchange.com/questions/625574››
lemma "(λx::real. (1 - x^2 / 2 - cos (x / (1 - x^2))) / x^4) ─0→ 23/24"
  by real_asymp

text ‹🌐‹https://www.mapleprimes.com/questions/151308-A-Hard-Limit-Question››
lemma "(λx::real. x / (x - 1) - 1 / ln x) ─1→ 1 / 2"
  by real_asymp

text ‹🌐‹https://www.freemathhelp.com/forum/threads/93513-two-extremely-difficult-limit-problems››
lemma "((λx::real. ((3 powr x + 4 powr x) / 4) powr (1/x)) ⤏ 4) at_top"
  by real_asymp

lemma "((λx::real. x powr 1.5 * (sqrt (x + 1) + sqrt (x - 1) - 2 * sqrt x)) ⤏ -1/4) at_top"
  by real_asymp

text ‹🌐‹https://math.stackexchange.com/questions/1390833››
context
  fixes a b :: real
  assumes ab: "a + b > 0" "a + b = 1"
begin
real_limit "λx. (a * x powr (1 / x) + b) powr (x / ln x)"
  facts: ab
end


subsection ‹Unsorted examples›

context
  fixes a :: real
  assumes a: "a > 1"
begin

text ‹
  It seems that Mathematica fails to expand the following example when ‹a› is a variable.
›
lemma "(λx. 1 - (1 - 1 / x powr a) powr x) ∼ (λx. x powr (1 - a))"
  using a by real_asymp

real_limit "λx. (1 - (1 - 1 / x powr a) powr x) * x powr (a - 1)"
  facts: a

lemma "(λn. log 2 (real ((n + 3) choose 3) / 4) + 1) ∼ (λn. 3 / ln 2 * ln n)"
proof -
  have "(λn. log 2 (real ((n + 3) choose 3) / 4) + 1) =
          (λn. log 2 ((real n + 1) * (real n + 2) * (real n + 3) / 24) + 1)"
    by (subst binomial_gbinomial) 
       (simp add: gbinomial_pochhammer' numeral_3_eq_3 pochhammer_Suc add_ac)
  moreover have "… ∼ (λn. 3 / ln 2 * ln n)"
    by (real_asymp simp: field_split_simps)
  ultimately show ?thesis by simp
qed

end

lemma "(λx::real. exp (sin x) / ln (cos x)) ∼[at 0] (λx. -2 / x ^ 2)"
  by real_asymp

real_limit "λx. ln (1 + 1 / x) * x"
real_limit "λx. ln x powr ln x / x"
real_limit "λx. (arctan x - pi/2) * x"
real_limit "λx. arctan (1/x) * x"

context
  fixes c :: real assumes c: "c ≥ 2"
begin
lemma c': "c^2 - 3 > 0"
proof -
  from c have "c^2 ≥ 2^2" by (rule power_mono) auto
  thus ?thesis by simp
qed

real_limit "λx. (c^2 - 3) * exp (-x)"
real_limit "λx. (c^2 - 3) * exp (-x)" facts: c'
end

lemma "c < 0 ⟹ ((λx::real. exp (c*x)) ⤏ 0) at_top"
  by real_asymp

lemma "filterlim (λx::real. -exp (1/x)) (at_left 0) (at_left 0)"
  by real_asymp

lemma "((λt::real. t^2 / (exp t - 1)) ⤏ 0) at_top"
  by real_asymp

lemma "(λn. (1 + 1 / real n) ^ n) ⇢ exp 1"
  by real_asymp
  
lemma "((λx::real. (1 + y / x) powr x) ⤏ exp y) at_top"
  by real_asymp

lemma "eventually (λx::real. x < x^2) at_top"
  by real_asymp
  
lemma "eventually (λx::real. 1 / x^2 ≥ 1 / x) (at_left 0)"
  by real_asymp

lemma "A > 1 ⟹ (λn. ((1 + 1 / sqrt A) / 2) powr real_of_int (2 ^ Suc n)) ⇢ 0"
  by (real_asymp simp: field_split_simps add_pos_pos)  

lemma 
  assumes "c > (1 :: real)" "k ≠ 0"
  shows   "(λn. real n ^ k) ∈ o(λn. c ^ n)"
  using assms by (real_asymp (verbose))

lemma "(λx::real. exp (-(x^4))) ∈ o(λx. exp (-(x^4)) + 1 / x ^ n)"
  by real_asymp
    
lemma "(λx::real. x^2) ∈ o[at_right 0](λx. x)"
  by real_asymp
    
lemma "(λx::real. x^2) ∈ o[at_left 0](λx. x)"
  by real_asymp

lemma "(λx::real. 2 * x + x ^ 2) ∈ Θ[at_left 0](λx. x)"
  by real_asymp
  
lemma "(λx::real. inverse (x - 1)^2) ∈ ω[at 1](λx. x)"
  by real_asymp

lemma "(λx::real. sin (1 / x)) ∼ (λx::real. 1 / x)"
  by real_asymp

lemma
  assumes "q ∈ {0<..<1}"
  shows   "LIM x at_left 1. log q (1 - x) :> at_top"
  using assms by real_asymp

context
  fixes x k :: real
  assumes xk: "x > 1" "k > 0"
begin

lemmas [simp] = add_pos_pos

real_expansion "λl. sqrt (1 + l * (l + 1) * 4 * pi^2 * k^2 * (log x (l + 1) - log x l)^2)"
  terms: 2 facts: xk

lemma
  "(λl. sqrt (1 + l * (l + 1) * 4 * pi^2 * k^2 * (log x (l + 1) - log x l)^2) -
          sqrt (1 + 4 * pi⇧2 * k⇧2 / (ln x ^ 2))) ∈ O(λl. 1 / l ^ 2)"
  using xk by (real_asymp simp: inverse_eq_divide power_divide root_powr_inverse)

end

lemma "(λx. (2 * x^3 - 128) / (sqrt x - 2)) ─4→ 384"
  by real_asymp

lemma 
  "((λx::real. (x^2 - 1) / abs (x - 1)) ⤏ 2) (at_right 1)"
  "((λx::real. (x^2 - 1) / abs (x - 1)) ⤏ -2) (at_left 1)"
  by real_asymp+

lemma "(λx::real. (root 3 x - 1) / (sqrt x - 1)) ─1→ 2/3"
  by real_asymp

lemma 
  fixes a b :: real
  assumes "a > 1" "b > 1" "a ≠ b"
  shows   "((λx. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1/x^3)) ⤏ 1) at_top"
  using assms by real_asymp


context
  fixes a b :: real
  assumes ab: "a > 0" "b > 0"
begin

lemma 
  "((λx. ((a powr x - x * ln a) / (b powr x - x * ln b)) powr (1 / x ^ 2)) ⤏
     exp ((ln a ^ 2 - ln b ^ 2) / 2)) (at 0)"
  using ab by (real_asymp simp: power2_eq_square)

end

real_limit "λx. 1 / sin (1/x) ^ 2 + 1 / tan (1/x) ^ 2 - 2 * x ^ 2"

real_limit "λx. ((1 / x + 4) powr 1.5 + exp (1 / x) - 9) * x"

lemma "x > (1 :: real) ⟹
         ((λn. abs (x powr n / (n * (1 + x powr (2 * n)))) powr (1 / n)) ⤏ 1 / x) at_top"
  by (real_asymp simp add: exp_minus field_simps)

lemma "x = (1 :: real) ⟹
         ((λn. abs (x powr n / (n * (1 + x powr (2 * n)))) powr (1 / n)) ⤏ 1 / x) at_top"
  by (real_asymp simp add: exp_minus field_simps)

lemma "x > (0 :: real) ⟹ x < 1 ⟹
         ((λn. abs (x powr n / (n * (1 + x powr (2 * n)))) powr (1 / n)) ⤏ x) at_top"
  by real_asymp

lemma "(λx. (exp (sin b) - exp (sin (b * x))) * tan (pi * x / 2)) ─1→
         (2*b/pi * exp (sin b) * cos b)"
  by real_asymp

(* SLOW *)
lemma "filterlim (λx::real. (sin (tan x) - tan (sin x))) (at 0) (at 0)"
  by real_asymp

(* SLOW *)
lemma "(λx::real. 1 / sin x powr (tan x ^ 2)) ─pi/2→ exp (1 / 2)"
  by (real_asymp simp: exp_minus)

lemma "a > 0 ⟹ b > 0 ⟹ c > 0 ⟹
  filterlim (λx::real. ((a powr x + b powr x + c powr x) / 3) powr (3 / x))
    (nhds (a * b * c)) (at 0)"
  by (real_asymp simp: exp_add add_divide_distrib exp_minus algebra_simps)

real_expansion "λx. arctan (sin (1 / x))"

real_expansion "λx. ln (1 + 1 / x)"
  terms: 5 (strict)

real_expansion "λx. sqrt (x + 1) - sqrt (x - 1)"
  terms: 3 (strict)


text ‹
  In this example, the first 7 terms of ‹tan (sin x)› and ‹sin (tan x)› coincide, which makes
  the calculation a bit slow.
›
real_limit "λx. (tan (sin x) - sin (tan x)) / x ^ 7" limit: "at_right 0"

(* SLOW *)
real_expansion "λx. sin (tan (1/x)) - tan (sin (1/x))"
  terms: 1 (strict)

(* SLOW *)
real_expansion "λx. tan (1 / x)"
  terms: 6

real_expansion "λx::real. arctan x"

real_expansion "λx. sin (tan (1/x))"

real_expansion "λx. (sin (-1 / x) ^ 2) powr sin (-1/x)"

real_limit "λx. exp (max (sin x) 1)"

lemma "filterlim (λx::real. 1 - 1 / x + ln x) at_top at_top"
  by (force intro: tendsto_diff filterlim_tendsto_add_at_top
        real_tendsto_divide_at_top filterlim_ident ln_at_top)

lemma "filterlim (λi::real. i powr (-i/(i-1)) - i powr (-1/(i-1))) (at_left 1) (at_right 0)"
  by real_asymp

lemma "filterlim (λi::real. i powr (-i/(i-1)) - i powr (-1/(i-1))) (at_right (-1)) at_top"
  by real_asymp

lemma "eventually (λi::real. i powr (-i/(i-1)) - i powr (-1/(i-1)) < 1) (at_right 0)"
  and "eventually (λi::real. i powr (-i/(i-1)) - i powr (-1/(i-1)) > -1) at_top"
  by real_asymp+

end


subsection ‹Interval arithmetic tests›

lemma "filterlim (λx::real. x + sin x) at_top at_top"
      "filterlim (λx::real. sin x + x) at_top at_top"
      "filterlim (λx::real. x + (sin x + sin x)) at_top at_top"
  by real_asymp+

lemma "filterlim (λx::real. 2 * x + sin x * x) at_infinity at_top"
      "filterlim (λx::real. 2 * x + (sin x + 1) * x) at_infinity at_top"
      "filterlim (λx::real. 3 * x + (sin x - 1) * x) at_infinity at_top"
      "filterlim (λx::real. 2 * x + x * sin x) at_infinity at_top"
      "filterlim (λx::real. 2 * x + x * (sin x + 1)) at_infinity at_top"
      "filterlim (λx::real. 3 * x + x * (sin x - 1)) at_infinity at_top"

      "filterlim (λx::real. x + sin x * sin x) at_infinity at_top"
      "filterlim (λx::real. x + sin x * (sin x + 1)) at_infinity at_top"
      "filterlim (λx::real. x + sin x * (sin x - 1)) at_infinity at_top"
      "filterlim (λx::real. x + sin x * (sin x + 2)) at_infinity at_top"
      "filterlim (λx::real. x + sin x * (sin x - 2)) at_infinity at_top"

      "filterlim (λx::real. x + (sin x - 1) * sin x) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 1) * (sin x + 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 1) * (sin x - 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 1) * (sin x + 2)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 1) * (sin x - 2)) at_infinity at_top"

      "filterlim (λx::real. x + (sin x - 2) * sin x) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 2) * (sin x + 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 2) * (sin x - 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 2) * (sin x + 2)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x - 2) * (sin x - 2)) at_infinity at_top"

      "filterlim (λx::real. x + (sin x + 1) * sin x) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 1) * (sin x + 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 1) * (sin x - 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 1) * (sin x + 2)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 1) * (sin x - 2)) at_infinity at_top"

      "filterlim (λx::real. x + (sin x + 2) * sin x) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 2) * (sin x + 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 2) * (sin x - 1)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 2) * (sin x + 2)) at_infinity at_top"
      "filterlim (λx::real. x + (sin x + 2) * (sin x - 2)) at_infinity at_top"
  by real_asymp+

lemma "filterlim (λx::real. x * inverse (sin x + 2)) at_top at_top"
      "filterlim (λx::real. x * inverse (sin x - 2)) at_bot at_top"
      "filterlim (λx::real. x / inverse (sin x + 2)) at_top at_top"
      "filterlim (λx::real. x / inverse (sin x - 2)) at_bot at_top"
  by real_asymp+

lemma "filterlim (λx::real. ⌊x⌋) at_top at_top"
      "filterlim (λx::real. ⌈x⌉) at_top at_top"
      "filterlim (λx::real. nat ⌊x⌋) at_top at_top"
      "filterlim (λx::real. nat ⌈x⌉) at_top at_top"
      "filterlim (λx::int. nat x) at_top at_top"
      "filterlim (λx::int. nat x) at_top at_top"
      "filterlim (λn::nat. real (n mod 42) + real n) at_top at_top"
  by real_asymp+

lemma "(λn. real_of_int ⌊n⌋) ∼[at_top] (λn. real_of_int n)"
      "(λn. sqrt ⌊n⌋) ∼[at_top] (λn. sqrt n)"
  by real_asymp+

lemma
  "c > 1 ⟹ (λn::nat. 2 ^ (n div c) :: int) ∈ o(λn. 2 ^ n)"
  by (real_asymp simp: field_simps)

lemma
  "c > 1 ⟹ (λn::nat. 2 ^ (n div c) :: nat) ∈ o(λn. 2 ^ n)"
  by (real_asymp simp: field_simps)

end