Аналіз I, Глава 10.5 #
I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.
Main constructions and results of this section:
- L'Hôpital's rule
theorem
Filter.Tendsto.of_div
{X : Set ℝ}
{f g : ℝ → ℝ}
{x₀ f'x₀ g'x₀ : ℝ}
(hfx₀ : f x₀ = 0)
(hgx₀ : g x₀ = 0)
(hg_non : g'x₀ ≠ 0)
(hf'x₀ : HasDerivWithinAt f f'x₀ X x₀)
(hg'x₀ : HasDerivWithinAt g g'x₀ X x₀)
:
Твердження 10.5.1 (L'Hôpital's rule, I) / Вправа 10.5.1
theorem
Filter.Tendsto.of_div'
{a b L : ℝ}
(hab : a < b)
{f g f' g' : ℝ → ℝ}
(hf : DifferentiableOn ℝ f (Set.Icc a b))
(hg : DifferentiableOn ℝ g (Set.Icc a b))
(hf' : f' = derivWithin f (Set.Icc a b))
(hg' : g' = derivWithin g (Set.Icc a b))
(hfa : f a = 0)
(hga : g a = 0)
(hgnon : ∀ x ∈ Set.Icc a b, g' x ≠ 0)
(hderiv : Tendsto (fun (x : ℝ) => f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L))
:
Твердження 10.5.2 (L'Hôpital's rule, II)