English
L'Hôpital's rule at +∞ states that if f and g tend to 0 and the ratio of derivatives tends to l at infinity, then f/g tends to l at infinity.
Русский
Правило Лопиталя при +∞: если f,g стремятся к 0 и отношение их производных стремится к l при x→+∞, то f/g стремится к l.
LaTeX
$$$$ \\lim_{x\\to +\\infty} \\frac{f(x)}{g(x)} = l \\quad \\text{if } \\lim_{x\\to +\\infty} \\frac{f'(x)}{g'(x)} = l \\text{ and } f(x),g(x) \\to 0. $$$$
Lean4
/-- L'Hôpital's rule for approaching +∞, `HasDerivAt` version -/
theorem lhopital_zero_atTop (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 (𝓝 0)) (hgtop : Tendsto g atTop (𝓝 0))
(hdiv : Tendsto (fun x => f' x / g' x) atTop l) : Tendsto (fun x => f x / g x) atTop l :=
by
rw [eventually_iff_exists_mem] at *
rcases hff' with ⟨s₁, hs₁, hff'⟩
rcases hgg' with ⟨s₂, hs₂, hgg'⟩
rcases hg' with ⟨s₃, hs₃, hg'⟩
let s := s₁ ∩ s₂ ∩ s₃
have hs : s ∈ atTop := inter_mem (inter_mem hs₁ hs₂) hs₃
rw [mem_atTop_sets] at hs
rcases hs with ⟨l, hl⟩
have hl' : Ioi l ⊆ s := fun x hx => hl x (le_of_lt hx)
refine lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx => hg' x <| (hl' hx).2) hftop hgtop hdiv <;> intro x hx <;>
apply_assumption <;>
first
| exact (hl' hx).1.1
| exact (hl' hx).1.2
