lhopital_zero_atTop_on_Ioi — Mathlib

English

Let a real a. If f is differentiable on Iio(a) and g' ≠ 0 there, with suitable boundary behavior near a from the left, then the L'Hôpital limit holds from the left toward a.

Русский

Пусть a есть некое число. Если f дифференцируема на Iio(a) и g'(x) ≠ 0 там, с удовлетворяющими условиями на границе слева от a, то результат Лопитал по левой стороне у a выполняется.

LaTeX

$$$$ a,\\; \\text{f differentiable on } Iio(a),\\; \\frac{f'(x)}{g'(x)}\\to l\\ (x\\to a^-)\; \\Rightarrow\\; \\lim_{x\\to a^-} \\frac{f(x)}{g(x)} = l. $$$$

Lean4

theorem lhopital_zero_atTop_on_Ioi (hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x) (hg' : ∀ x ∈ Ioi a, 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
  obtain ⟨a', haa', ha'⟩ : ∃ a', a < a' ∧ 0 < a' :=
    ⟨1 + max a 0, ⟨lt_of_le_of_lt (le_max_left a 0) (lt_one_add _), lt_of_le_of_lt (le_max_right a 0) (lt_one_add _)⟩⟩
  have fact1 : ∀ x : ℝ, x ∈ Ioo 0 a'⁻¹ → x ≠ 0 := fun _ hx => (ne_of_lt hx.1).symm
  have fact2 (x) (hx : x ∈ Ioo 0 a'⁻¹) : a < x⁻¹ := lt_trans haa' ((lt_inv_comm₀ ha' hx.1).mpr hx.2)
  have hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x := fun x hx =>
    comp x (hff' x⁻¹ <| fact2 x hx) (hasDerivAt_inv <| fact1 x hx)
  have hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x := fun x hx =>
    comp x (hgg' x⁻¹ <| fact2 x hx) (hasDerivAt_inv <| fact1 x hx)
  have :=
    lhopital_zero_right_on_Ioo (inv_pos.mpr ha') hdnf hdng
      (by
        intro x hx
        refine mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)
        exact hg' _ (fact2 x hx))
      (hftop.comp tendsto_inv_nhdsGT_zero) (hgtop.comp tendsto_inv_nhdsGT_zero)
      (by
        refine (tendsto_congr' ?_).mp (hdiv.comp tendsto_inv_nhdsGT_zero)
        filter_upwards [self_mem_nhdsWithin] with x (hx : 0 < x)
        simp only [Function.comp_def]
        rw [mul_div_mul_right]
        exact neg_ne_zero.mpr (by positivity))
  have := this.comp tendsto_inv_atTop_nhdsGT_zero
  unfold Function.comp at this
  simpa only [inv_inv]

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