lhopital_zero_left_on_Ioc — Mathlib

English

Let a<b. If f,g are differentiable on Ioo(a,b) with nonzero derivative ratio on the left side of a, and f and g satisfy boundary conditions at a with continuity on Ioc(a,b), then the derivative ratio limit implies the quotient limit near a from the left.

Русский

Пусть a<b. Если f,g дифференцируемы на Ioo(a,b) с ненулевым отношением производных слева к a, и на границе соблюдены условия непрерывности на Ioc(a,b), то предел отношения производных приводит к пределу f/g слева от a.

LaTeX

$$$$ a

Lean4

theorem lhopital_zero_left_on_Ioc (hab : a < b) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) (hcf : ContinuousOn f (Ioc a b)) (hcg : ContinuousOn g (Ioc a b))
    (hg' : ∀ x ∈ Ioo a b, g' x ≠ 0) (hfb : f b = 0) (hgb : g b = 0) (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l) :
    Tendsto (fun x => f x / g x) (𝓝[<] b) l :=
  by
  refine lhopital_zero_left_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv
  · rw [← hfb, ← nhdsWithin_Ioo_eq_nhdsLT hab]
    exact ((hcf b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto
  · rw [← hgb, ← nhdsWithin_Ioo_eq_nhdsLT hab]
    exact ((hcg b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Похожие утверждения