mathlib documentation

analysis.​calculus.​lhopital

analysis.​calculus.​lhopital

L'HΓ΄pital's rule for 0/0 indeterminate forms

In this file, we prove several forms of "L'Hopital's rule" for computing 0/0 indeterminate forms. The proof of has_deriv_at.lhopital_zero_right_on_Ioo is based on the one given in the corresponding Wikibooks chapter, and all other statements are derived from this one by composing by carefully chosen functions.

Note that the filter f'/g' tends to isn't required to be one of 𝓝 a, at_top or at_bot. In fact, we give a slightly stronger statement by allowing it to be any filter on ℝ.

Each statement is available in a has_deriv_at form and a deriv form, which is denoted by each statement being in either the has_deriv_at or the deriv namespace.

Interval-based versions

We start by proving statements where all conditions (derivability, g' β‰  0) have to be satisfied on an explicitely-provided interval.

theorem has_deriv_at.​lhopital_zero_right_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

theorem has_deriv_at.​lhopital_zero_right_on_Ico {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ continuous_on f (set.Ico a b) β†’ continuous_on g (set.Ico a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ f a = 0 β†’ g a = 0 β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

theorem has_deriv_at.​lhopital_zero_left_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ filter.tendsto f (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto g (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within b (set.Iio b)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within b (set.Iio b)) l

theorem has_deriv_at.​lhopital_zero_left_on_Ioc {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ continuous_on f (set.Ioc a b) β†’ continuous_on g (set.Ioc a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ f b = 0 β†’ g b = 0 β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within b (set.Iio b)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within b (set.Iio b)) l

theorem has_deriv_at.​lhopital_zero_at_top_on_Ioi {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ g' x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

theorem has_deriv_at.​lhopital_zero_at_bot_on_Iio {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Iio a β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Iio a β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Iio a β†’ g' x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

theorem deriv.​lhopital_zero_right_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioo a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

theorem deriv.​lhopital_zero_right_on_Ico {a b : ℝ} (hab : a < b) {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioo a b) β†’ continuous_on f (set.Ico a b) β†’ continuous_on g (set.Ico a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ deriv g x β‰  0) β†’ f a = 0 β†’ g a = 0 β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

theorem deriv.​lhopital_zero_left_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioo a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ deriv g x β‰  0) β†’ filter.tendsto f (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto g (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within b (set.Iio b)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within b (set.Iio b)) l

theorem deriv.​lhopital_zero_at_top_on_Ioi {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioi a) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ deriv g x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

theorem deriv.​lhopital_zero_at_bot_on_Iio {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Iio a) β†’ (βˆ€ (x : ℝ), x ∈ set.Iio a β†’ deriv g x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

Generic versions

The following statements no longer any explicit interval, as they only require conditions holding eventually.

theorem has_deriv_at.​lhopital_zero_nhds_right {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

L'HΓ΄pital's rule for approaching a real from the right, has_deriv_at version

theorem has_deriv_at.​lhopital_zero_nhds_left {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Iio a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Iio a)) l

L'HΓ΄pital's rule for approaching a real from the left, has_deriv_at version

theorem has_deriv_at.​lhopital_zero_nhds' {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.univ \ {a})) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, has_deriv_at version. This does not require anything about the situation at a

theorem has_deriv_at.​lhopital_zero_nhds {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds a, has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds a, has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds a, g' x β‰  0) β†’ filter.tendsto f (nhds a) (nhds 0) β†’ filter.tendsto g (nhds a) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds a) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, has_deriv_at version

theorem has_deriv_at.​lhopital_zero_at_top {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_top, has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_top, has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_top, g' x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

L'Hôpital's rule for approaching +∞, has_deriv_at version

theorem has_deriv_at.​lhopital_zero_at_bot {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_bot, has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_bot, has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_bot, g' x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

L'Hôpital's rule for approaching -∞, has_deriv_at version

theorem deriv.​lhopital_zero_nhds_right {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

L'HΓ΄pital's rule for approaching a real from the right, deriv version

theorem deriv.​lhopital_zero_nhds_left {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Iio a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Iio a)) l

L'HΓ΄pital's rule for approaching a real from the left, deriv version

theorem deriv.​lhopital_zero_nhds' {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.univ \ {a})) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, deriv version. This does not require anything about the situation at a

theorem deriv.​lhopital_zero_nhds {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds a, differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds a, deriv g x β‰  0) β†’ filter.tendsto f (nhds a) (nhds 0) β†’ filter.tendsto g (nhds a) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds a) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, deriv version

theorem deriv.​lhopital_zero_at_top {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_top, differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_top, deriv g x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

L'Hôpital's rule for approaching +∞, deriv version

theorem deriv.​lhopital_zero_at_bot {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_bot, differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_bot, deriv g x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

L'Hôpital's rule for approaching -∞, deriv version