English
As x approaches a from the left inside the left-open interval Iio, with differentiability hypotheses and derivative ratio limit, the quotient tends to the same limit l.
Русский
При x слева от a внутри левой окрестности Iio, при выполнении условий производных и предела отношения производных, отношение f/g стремится к l.
LaTeX
$$$$ \\text{Under left-hand approach to } a, \\lim_{x\\to a^-} \\frac{f(x)}{g(x)} = l \\text{ given derivative conditions.} $$$$
Lean4
/-- L'Hôpital's rule for approaching a real from the left, `HasDerivAt` version -/
theorem lhopital_zero_nhdsLT (hff' : ∀ᶠ x in 𝓝[<] a, HasDerivAt f (f' x) x)
(hgg' : ∀ᶠ x in 𝓝[<] a, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in 𝓝[<] a, g' x ≠ 0) (hfa : Tendsto f (𝓝[<] a) (𝓝 0))
(hga : Tendsto g (𝓝[<] a) (𝓝 0)) (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] a) l) :
Tendsto (fun x => f x / g x) (𝓝[<] a) 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 ∈ 𝓝[<] a := inter_mem (inter_mem hs₁ hs₂) hs₃
rw [mem_nhdsLT_iff_exists_Ioo_subset] at hs
rcases hs with ⟨l, hal, hl⟩
refine lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv <;> intro x hx <;> apply_assumption <;>
first
| exact (hl hx).1.1
| exact (hl hx).1.2
| exact (hl hx).2
