L'HΓ΄pital's rule for 0/0 indeterminate forms #
In this file, we prove several forms of "L'HΓ΄pital's rule" for computing 0/0
indeterminate forms. The proof of HasDerivAt.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,
atTop or atBot. In fact, we give a slightly stronger statement by
allowing it to be any filter on β.
Each statement is available in a HasDerivAt form and a deriv form, which
is denoted by each statement being in either the HasDerivAt 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
HasDerivAt.lhopital_zero_right_on_Ioo
{a b : β}
{l : Filter β}
{f f' g g' : β β β}
(hab : a < b)
(hff' : β x β Set.Ioo a b, HasDerivAt f (f' x) x)
(hgg' : β x β Set.Ioo a b, HasDerivAt g (g' x) x)
(hg' : β x β Set.Ioo a b, g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
theorem
HasDerivAt.lhopital_zero_right_on_Ico
{a b : β}
{l : Filter β}
{f f' g g' : β β β}
(hab : a < b)
(hff' : β x β Set.Ioo a b, HasDerivAt f (f' x) x)
(hgg' : β x β Set.Ioo a b, HasDerivAt g (g' x) x)
(hcf : ContinuousOn f (Set.Ico a b))
(hcg : ContinuousOn g (Set.Ico a b))
(hg' : β x β Set.Ioo a b, g' x β 0)
(hfa : f a = 0)
(hga : g a = 0)
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
theorem
HasDerivAt.lhopital_zero_left_on_Ioo
{a b : β}
{l : Filter β}
{f f' g g' : β β β}
(hab : a < b)
(hff' : β x β Set.Ioo a b, HasDerivAt f (f' x) x)
(hgg' : β x β Set.Ioo a b, HasDerivAt g (g' x) x)
(hg' : β x β Set.Ioo a b, g' x β 0)
(hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds 0))
(hgb : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin b (Set.Iio b)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin b (Set.Iio b)) l
theorem
HasDerivAt.lhopital_zero_left_on_Ioc
{a b : β}
{l : Filter β}
{f f' g g' : β β β}
(hab : a < b)
(hff' : β x β Set.Ioo a b, HasDerivAt f (f' x) x)
(hgg' : β x β Set.Ioo a b, HasDerivAt g (g' x) x)
(hcf : ContinuousOn f (Set.Ioc a b))
(hcg : ContinuousOn g (Set.Ioc a b))
(hg' : β x β Set.Ioo a b, g' x β 0)
(hfb : f b = 0)
(hgb : g b = 0)
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin b (Set.Iio b)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin b (Set.Iio b)) l
theorem
HasDerivAt.lhopital_zero_atTop_on_Ioi
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : β x β Set.Ioi a, HasDerivAt f (f' x) x)
(hgg' : β x β Set.Ioi a, HasDerivAt g (g' x) x)
(hg' : β x β Set.Ioi a, g' x β 0)
(hftop : Filter.Tendsto f Filter.atTop (nhds 0))
(hgtop : Filter.Tendsto g Filter.atTop (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) Filter.atTop l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atTop l
theorem
HasDerivAt.lhopital_zero_atBot_on_Iio
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : β x β Set.Iio a, HasDerivAt f (f' x) x)
(hgg' : β x β Set.Iio a, HasDerivAt g (g' x) x)
(hg' : β x β Set.Iio a, g' x β 0)
(hfbot : Filter.Tendsto f Filter.atBot (nhds 0))
(hgbot : Filter.Tendsto g Filter.atBot (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) Filter.atBot l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atBot l
theorem
deriv.lhopital_zero_right_on_Ioo
{a b : β}
{l : Filter β}
{f g : β β β}
(hab : a < b)
(hdf : DifferentiableOn β f (Set.Ioo a b))
(hg' : β x β Set.Ioo a b, deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
theorem
deriv.lhopital_zero_right_on_Ico
{a b : β}
{l : Filter β}
{f g : β β β}
(hab : a < b)
(hdf : DifferentiableOn β f (Set.Ioo a b))
(hcf : ContinuousOn f (Set.Ico a b))
(hcg : ContinuousOn g (Set.Ico a b))
(hg' : β x β Set.Ioo a b, deriv g x β 0)
(hfa : f a = 0)
(hga : g a = 0)
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
theorem
deriv.lhopital_zero_left_on_Ioo
{a b : β}
{l : Filter β}
{f g : β β β}
(hab : a < b)
(hdf : DifferentiableOn β f (Set.Ioo a b))
(hg' : β x β Set.Ioo a b, deriv g x β 0)
(hfb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds 0))
(hgb : Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin b (Set.Iio b)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin b (Set.Iio b)) l
theorem
deriv.lhopital_zero_atTop_on_Ioi
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : DifferentiableOn β f (Set.Ioi a))
(hg' : β x β Set.Ioi a, deriv g x β 0)
(hftop : Filter.Tendsto f Filter.atTop (nhds 0))
(hgtop : Filter.Tendsto g Filter.atTop (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) Filter.atTop l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atTop l
theorem
deriv.lhopital_zero_atBot_on_Iio
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : DifferentiableOn β f (Set.Iio a))
(hg' : β x β Set.Iio a, deriv g x β 0)
(hfbot : Filter.Tendsto f Filter.atBot (nhds 0))
(hgbot : Filter.Tendsto g Filter.atBot (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) Filter.atBot l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atBot l
Generic versions #
The following statements no longer any explicit interval, as they only require conditions holding eventually.
theorem
HasDerivAt.lhopital_zero_nhdsGT
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
L'HΓ΄pital's rule for approaching a real from the right, HasDerivAt version
@[deprecated HasDerivAt.lhopital_zero_nhdsGT (since := "2025-03-02")]
theorem
HasDerivAt.lhopital_zero_nhds_right
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
Alias of HasDerivAt.lhopital_zero_nhdsGT.
L'HΓ΄pital's rule for approaching a real from the right, HasDerivAt version
theorem
HasDerivAt.lhopital_zero_nhdsLT
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Iio a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a (Set.Iio a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Iio a)) l
L'HΓ΄pital's rule for approaching a real from the left, HasDerivAt version
@[deprecated HasDerivAt.lhopital_zero_nhdsLT (since := "2025-03-02")]
theorem
HasDerivAt.lhopital_zero_nhds_left
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Iio a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a (Set.Iio a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Iio a)) l
Alias of HasDerivAt.lhopital_zero_nhdsLT.
L'HΓ΄pital's rule for approaching a real from the left, HasDerivAt version
theorem
HasDerivAt.lhopital_zero_nhdsNE
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhdsWithin a {a}αΆ, HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhdsWithin a {a}αΆ, HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in nhdsWithin a {a}αΆ, g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a {a}αΆ) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a {a}αΆ) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a {a}αΆ) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a {a}αΆ) l
L'HΓ΄pital's rule for approaching a real, HasDerivAt version. This
does not require anything about the situation at a
@[deprecated HasDerivAt.lhopital_zero_nhdsNE (since := "2025-03-02")]
theorem
HasDerivAt.lhopital_zero_nhds'
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhdsWithin a {a}αΆ, HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhdsWithin a {a}αΆ, HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in nhdsWithin a {a}αΆ, g' x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a {a}αΆ) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a {a}αΆ) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) (nhdsWithin a {a}αΆ) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a {a}αΆ) l
Alias of HasDerivAt.lhopital_zero_nhdsNE.
L'HΓ΄pital's rule for approaching a real, HasDerivAt version. This
does not require anything about the situation at a
theorem
HasDerivAt.lhopital_zero_nhds
{a : β}
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in nhds a, HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in nhds a, HasDerivAt 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 (fun (x : β) => f' x / g' x) (nhds a) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a {a}αΆ) l
L'HΓ΄pital's rule for approaching a real, HasDerivAt version
theorem
HasDerivAt.lhopital_zero_atTop
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in Filter.atTop, HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in Filter.atTop, HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in Filter.atTop, g' x β 0)
(hftop : Filter.Tendsto f Filter.atTop (nhds 0))
(hgtop : Filter.Tendsto g Filter.atTop (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) Filter.atTop l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atTop l
L'HΓ΄pital's rule for approaching +β, HasDerivAt version
theorem
HasDerivAt.lhopital_zero_atBot
{l : Filter β}
{f f' g g' : β β β}
(hff' : βαΆ (x : β) in Filter.atBot, HasDerivAt f (f' x) x)
(hgg' : βαΆ (x : β) in Filter.atBot, HasDerivAt g (g' x) x)
(hg' : βαΆ (x : β) in Filter.atBot, g' x β 0)
(hfbot : Filter.Tendsto f Filter.atBot (nhds 0))
(hgbot : Filter.Tendsto g Filter.atBot (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => f' x / g' x) Filter.atBot l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atBot l
L'HΓ΄pital's rule for approaching -β, HasDerivAt version
theorem
deriv.lhopital_zero_nhdsGT
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), DifferentiableAt β f x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
L'HΓ΄pital's rule for approaching a real from the right, deriv version
@[deprecated deriv.lhopital_zero_nhdsGT (since := "2025-03-02")]
theorem
deriv.lhopital_zero_nhds_right
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), DifferentiableAt β f x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Ioi a), deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Ioi a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a (Set.Ioi a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Ioi a)) l
Alias of deriv.lhopital_zero_nhdsGT.
L'HΓ΄pital's rule for approaching a real from the right, deriv version
theorem
deriv.lhopital_zero_nhdsLT
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in nhdsWithin a (Set.Iio a), DifferentiableAt β f x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Iio a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a (Set.Iio a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Iio a)) l
L'HΓ΄pital's rule for approaching a real from the left, deriv version
@[deprecated deriv.lhopital_zero_nhdsLT (since := "2025-03-02")]
theorem
deriv.lhopital_zero_nhds_left
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in nhdsWithin a (Set.Iio a), DifferentiableAt β f x)
(hg' : βαΆ (x : β) in nhdsWithin a (Set.Iio a), deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a (Set.Iio a)) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a (Set.Iio a)) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a (Set.Iio a)) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a (Set.Iio a)) l
Alias of deriv.lhopital_zero_nhdsLT.
L'HΓ΄pital's rule for approaching a real from the left, deriv version
theorem
deriv.lhopital_zero_nhdsNE
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in nhdsWithin a {a}αΆ, DifferentiableAt β f x)
(hg' : βαΆ (x : β) in nhdsWithin a {a}αΆ, deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a {a}αΆ) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a {a}αΆ) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a {a}αΆ) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a {a}αΆ) l
L'HΓ΄pital's rule for approaching a real, deriv version. This
does not require anything about the situation at a
@[deprecated deriv.lhopital_zero_nhdsNE (since := "2025-03-02")]
theorem
deriv.lhopital_zero_nhds'
{a : β}
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in nhdsWithin a {a}αΆ, DifferentiableAt β f x)
(hg' : βαΆ (x : β) in nhdsWithin a {a}αΆ, deriv g x β 0)
(hfa : Filter.Tendsto f (nhdsWithin a {a}αΆ) (nhds 0))
(hga : Filter.Tendsto g (nhdsWithin a {a}αΆ) (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) (nhdsWithin a {a}αΆ) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a {a}αΆ) l
Alias of deriv.lhopital_zero_nhdsNE.
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, DifferentiableAt β 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 (fun (x : β) => deriv f x / deriv g x) (nhds a) l)
:
Filter.Tendsto (fun (x : β) => f x / g x) (nhdsWithin a {a}αΆ) l
L'HΓ΄pital's rule for approaching a real, deriv version
theorem
deriv.lhopital_zero_atTop
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in Filter.atTop, DifferentiableAt β f x)
(hg' : βαΆ (x : β) in Filter.atTop, deriv g x β 0)
(hftop : Filter.Tendsto f Filter.atTop (nhds 0))
(hgtop : Filter.Tendsto g Filter.atTop (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) Filter.atTop l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atTop l
L'HΓ΄pital's rule for approaching +β, deriv version
theorem
deriv.lhopital_zero_atBot
{l : Filter β}
{f g : β β β}
(hdf : βαΆ (x : β) in Filter.atBot, DifferentiableAt β f x)
(hg' : βαΆ (x : β) in Filter.atBot, deriv g x β 0)
(hfbot : Filter.Tendsto f Filter.atBot (nhds 0))
(hgbot : Filter.Tendsto g Filter.atBot (nhds 0))
(hdiv : Filter.Tendsto (fun (x : β) => deriv f x / deriv g x) Filter.atBot l)
:
Filter.Tendsto (fun (x : β) => f x / g x) Filter.atBot l
L'HΓ΄pital's rule for approaching -β, deriv version