English
Analogous to the +∞ case, but as x → −∞ the derivative ratio governs the limit of f/g provided f and g tend to 0 appropriately.
Русский
Аналогично случаю на +∞, но при x → −∞ отношение производных определяет предел f/g, если f и g сходятся к нулю должным образом.
LaTeX
$$$$ \\lim_{x\\to -\\infty} \\frac{f(x)}{g(x)} = l \\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_atBot (hff' : ∀ᶠ x in atBot, HasDerivAt f (f' x) x) (hgg' : ∀ᶠ x in atBot, HasDerivAt g (g' x) x)
(hg' : ∀ᶠ x in atBot, g' x ≠ 0) (hfbot : Tendsto f atBot (𝓝 0)) (hgbot : Tendsto g atBot (𝓝 0))
(hdiv : Tendsto (fun x => f' x / g' x) atBot l) : Tendsto (fun x => f x / g x) atBot 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 ∈ atBot := inter_mem (inter_mem hs₁ hs₂) hs₃
rw [mem_atBot_sets] at hs
rcases hs with ⟨l, hl⟩
have hl' : Iio l ⊆ s := fun x hx => hl x (le_of_lt hx)
refine lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx => hg' x <| (hl' hx).2) hfbot hgbot hdiv <;> intro x hx <;>
apply_assumption <;>
first
| exact (hl' hx).1.1
| exact (hl' hx).1.2
