Аналіз I, Розділ 10.5: Правило Лопіталя

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Правило Лопіталя.

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₀) : (∃ δ > 0, ∀ x ∈ X \ {x₀} ∩ Set.Ioo (x₀ - δ) (x₀ + δ), g x ≠ 0) ∧ Tendsto (fun (x : ℝ) => f x / g x) (nhdsWithin x₀ (X \ {x₀})) (nhds (f'x₀ / g'x₀))

Твердження 10.5.1 (Правило Лопіталя, 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)) : (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Tendsto (fun (x : ℝ) => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)

Твердження 10.5.2 (Правило Лопіталя, II)