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_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

L'Hôpital's rule for approaching a real from the right, HasDerivAt version

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

L'Hôpital's rule for approaching a real from the left, HasDerivAt version

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

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_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

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 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

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

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