L'Hôpital's rule for infinity/infinity

Stream: Is there code for X?

[Aaron Hill]

I found https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/LHopital.html but it only seems to handle the 0/0 case, not the infinity/infinity case. Do we have any theorems for that case?

[Kevin Buzzard]

Can you state the theorem that you're looking for (ideally in lean but even in maths would be a start)

[Aaron Hill]

What I'd like is that if f(x) -> infinity and g(x) -> infinity as x -> infinity, then f(x)/g(x) -> f'(x)/g'(x) (assuming both are differentiable). Specifically, an atTop (instead of nhds 0) version of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/LHopital.html#HasDerivAt.lhopital_zero_atTop:

import Mathlib
import Mathlib.Topology.Defs.Filter
open Filter
open Topology

theorem lhopital_atTop_atTop {a b : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ} (hff' : ∀ᶠ x in atTop, HasDerivAt f (f' x) x)
    (hgg' : ∀ᶠ x in atTop, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in atTop, g' x ≠ 0)
    (hftop : Tendsto f atTop atTop) (hgtop : Tendsto g atTop atTop)
    (hdiv : Tendsto (fun x => f' x / g' x) atTop l) : Tendsto (fun x => f x / g x) atTop l := by
  sorry

[Aaron Liu]

This version doesn't seem to be true, for f := Real.cosh, g := Real.sinh, f' := Real.sinh, g' := Real.cosh, l := 𝓝[<] 1.