L'Hôpital's rule for 0/0 indeterminate forms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
Tags #
L'Hôpital's rule, L'Hopital's rule
Interval-based versions #
We start by proving statements where all conditions (derivability, g' ≠ 0) have
to be satisfied on an explicitly-provided interval.
theorem
has_deriv_at.lhopital_zero_right_on_Ioo
{a b : ℝ}
(hab : a < b)
{l : filter ℝ}
{f f' g g' : ℝ → ℝ}
(hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x)
(hgg' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x)
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → g' x ≠ 0)
(hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0))
(hga : filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x)
(hgg' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x)
(hcf : continuous_on f (set.Ico a b))
(hcg : continuous_on g (set.Ico a b))
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → g' x ≠ 0)
(hfa : f a = 0)
(hga : g a = 0)
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x)
(hgg' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x)
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → g' x ≠ 0)
(hfb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds 0))
(hgb : filter.tendsto g (nhds_within b (set.Iio b)) (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at f (f' x) x)
(hgg' : ∀ (x : ℝ), x ∈ set.Ioo a b → has_deriv_at g (g' x) x)
(hcf : continuous_on f (set.Ioc a b))
(hcg : continuous_on g (set.Ioc a b))
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → g' x ≠ 0)
(hfb : f b = 0)
(hgb : g b = 0)
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ (x : ℝ), x ∈ set.Ioi a → has_deriv_at f (f' x) x)
(hgg' : ∀ (x : ℝ), x ∈ set.Ioi a → has_deriv_at g (g' x) x)
(hg' : ∀ (x : ℝ), x ∈ set.Ioi a → g' x ≠ 0)
(hftop : filter.tendsto f filter.at_top (nhds 0))
(hgtop : filter.tendsto g filter.at_top (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ (x : ℝ), x ∈ set.Iio a → has_deriv_at f (f' x) x)
(hgg' : ∀ (x : ℝ), x ∈ set.Iio a → has_deriv_at g (g' x) x)
(hg' : ∀ (x : ℝ), x ∈ set.Iio a → g' x ≠ 0)
(hfbot : filter.tendsto f filter.at_bot (nhds 0))
(hgbot : filter.tendsto g filter.at_bot (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : differentiable_on ℝ f (set.Ioo a b))
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → deriv g x ≠ 0)
(hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0))
(hga : filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : differentiable_on ℝ f (set.Ioo a b))
(hcf : continuous_on f (set.Ico a b))
(hcg : continuous_on g (set.Ico a b))
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → deriv g x ≠ 0)
(hfa : f a = 0)
(hga : g a = 0)
(hdiv : 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 : ℝ → ℝ}
(hdf : differentiable_on ℝ f (set.Ioo a b))
(hg' : ∀ (x : ℝ), x ∈ set.Ioo a b → deriv g x ≠ 0)
(hfb : filter.tendsto f (nhds_within b (set.Iio b)) (nhds 0))
(hgb : filter.tendsto g (nhds_within b (set.Iio b)) (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : differentiable_on ℝ f (set.Ioi a))
(hg' : ∀ (x : ℝ), x ∈ set.Ioi a → deriv g x ≠ 0)
(hftop : filter.tendsto f filter.at_top (nhds 0))
(hgtop : filter.tendsto g filter.at_top (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : differentiable_on ℝ f (set.Iio a))
(hg' : ∀ (x : ℝ), x ∈ set.Iio a → deriv g x ≠ 0)
(hfbot : filter.tendsto f filter.at_bot (nhds 0))
(hgbot : filter.tendsto g filter.at_bot (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ᶠ (x : ℝ) in nhds_within a (set.Ioi a), has_deriv_at f (f' x) x)
(hgg' : ∀ᶠ (x : ℝ) in nhds_within a (set.Ioi a), has_deriv_at g (g' x) x)
(hg' : ∀ᶠ (x : ℝ) in nhds_within a (set.Ioi a), g' x ≠ 0)
(hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0))
(hga : filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ᶠ (x : ℝ) in nhds_within a (set.Iio a), has_deriv_at f (f' x) x)
(hgg' : ∀ᶠ (x : ℝ) in nhds_within a (set.Iio a), has_deriv_at g (g' x) x)
(hg' : ∀ᶠ (x : ℝ) in nhds_within a (set.Iio a), g' x ≠ 0)
(hfa : filter.tendsto f (nhds_within a (set.Iio a)) (nhds 0))
(hga : filter.tendsto g (nhds_within a (set.Iio a)) (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ᶠ (x : ℝ) in nhds_within a {a}ᶜ, has_deriv_at f (f' x) x)
(hgg' : ∀ᶠ (x : ℝ) in nhds_within a {a}ᶜ, has_deriv_at g (g' x) x)
(hg' : ∀ᶠ (x : ℝ) in nhds_within a {a}ᶜ, g' x ≠ 0)
(hfa : filter.tendsto f (nhds_within a {a}ᶜ) (nhds 0))
(hga : filter.tendsto g (nhds_within a {a}ᶜ) (nhds 0))
(hdiv : filter.tendsto (λ (x : ℝ), f' x / g' x) (nhds_within a {a}ᶜ) l) :
filter.tendsto (λ (x : ℝ), f x / g x) (nhds_within a {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' : ℝ → ℝ}
(hff' : ∀ᶠ (x : ℝ) in nhds a, has_deriv_at f (f' x) x)
(hgg' : ∀ᶠ (x : ℝ) in nhds a, has_deriv_at g (g' x) x)
(hg' : ∀ᶠ (x : ℝ) in nhds a, g' x ≠ 0)
(hfa : filter.tendsto f (nhds a) (nhds 0))
(hga : filter.tendsto g (nhds a) (nhds 0))
(hdiv : filter.tendsto (λ (x : ℝ), f' x / g' x) (nhds a) l) :
filter.tendsto (λ (x : ℝ), f x / g x) (nhds_within a {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' : ℝ → ℝ}
(hff' : ∀ᶠ (x : ℝ) in filter.at_top, has_deriv_at f (f' x) x)
(hgg' : ∀ᶠ (x : ℝ) in filter.at_top, has_deriv_at g (g' x) x)
(hg' : ∀ᶠ (x : ℝ) in filter.at_top, g' x ≠ 0)
(hftop : filter.tendsto f filter.at_top (nhds 0))
(hgtop : filter.tendsto g filter.at_top (nhds 0))
(hdiv : 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' : ℝ → ℝ}
(hff' : ∀ᶠ (x : ℝ) in filter.at_bot, has_deriv_at f (f' x) x)
(hgg' : ∀ᶠ (x : ℝ) in filter.at_bot, has_deriv_at g (g' x) x)
(hg' : ∀ᶠ (x : ℝ) in filter.at_bot, g' x ≠ 0)
(hfbot : filter.tendsto f filter.at_bot (nhds 0))
(hgbot : filter.tendsto g filter.at_bot (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : ∀ᶠ (x : ℝ) in nhds_within a (set.Ioi a), differentiable_at ℝ f x)
(hg' : ∀ᶠ (x : ℝ) in nhds_within a (set.Ioi a), deriv g x ≠ 0)
(hfa : filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0))
(hga : filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : ∀ᶠ (x : ℝ) in nhds_within a (set.Iio a), differentiable_at ℝ f x)
(hg' : ∀ᶠ (x : ℝ) in nhds_within a (set.Iio a), deriv g x ≠ 0)
(hfa : filter.tendsto f (nhds_within a (set.Iio a)) (nhds 0))
(hga : filter.tendsto g (nhds_within a (set.Iio a)) (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : ∀ᶠ (x : ℝ) in nhds_within a {a}ᶜ, differentiable_at ℝ f x)
(hg' : ∀ᶠ (x : ℝ) in nhds_within a {a}ᶜ, deriv g x ≠ 0)
(hfa : filter.tendsto f (nhds_within a {a}ᶜ) (nhds 0))
(hga : filter.tendsto g (nhds_within a {a}ᶜ) (nhds 0))
(hdiv : filter.tendsto (λ (x : ℝ), deriv f x / deriv g x) (nhds_within a {a}ᶜ) l) :
filter.tendsto (λ (x : ℝ), f x / g x) (nhds_within a {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 : ℝ → ℝ}
(hdf : ∀ᶠ (x : ℝ) in nhds a, differentiable_at ℝ f x)
(hg' : ∀ᶠ (x : ℝ) in nhds a, deriv g x ≠ 0)
(hfa : filter.tendsto f (nhds a) (nhds 0))
(hga : filter.tendsto g (nhds a) (nhds 0))
(hdiv : filter.tendsto (λ (x : ℝ), deriv f x / deriv g x) (nhds a) l) :
filter.tendsto (λ (x : ℝ), f x / g x) (nhds_within a {a}ᶜ) l
L'Hôpital's rule for approaching a real, deriv version
theorem
deriv.lhopital_zero_at_top
{l : filter ℝ}
{f g : ℝ → ℝ}
(hdf : ∀ᶠ (x : ℝ) in filter.at_top, differentiable_at ℝ f x)
(hg' : ∀ᶠ (x : ℝ) in filter.at_top, deriv g x ≠ 0)
(hftop : filter.tendsto f filter.at_top (nhds 0))
(hgtop : filter.tendsto g filter.at_top (nhds 0))
(hdiv : 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 : ℝ → ℝ}
(hdf : ∀ᶠ (x : ℝ) in filter.at_bot, differentiable_at ℝ f x)
(hg' : ∀ᶠ (x : ℝ) in filter.at_bot, deriv g x ≠ 0)
(hfbot : filter.tendsto f filter.at_bot (nhds 0))
(hgbot : filter.tendsto g filter.at_bot (nhds 0))
(hdiv : 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