L'Hopital's rule

Stream: new members

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

(deleted)

[Anatole Dedecker]

Ok so after the harmonic series thing, which I still have to PR, I've been working on proving L'Hopital's rule, which is also one of the 100 theorems. I based myself upon the proof given here https://fr.wikiversity.org/wiki/Fonctions_d%27une_variable_r%C3%A9elle/D%C3%A9rivabilit%C3%A9#Th%C3%A9or%C3%A8mes_sur_la_d%C3%A9rivation (in French), and I got this. Of course there is still a lot to do :

• get rid of the "continuity on [a,b[" hypothesis by extending the functions
• prove the case where we take the limit at the right bound of derivability interval
• deduce the case where we take the limit in the middle of derivability interval
• and others...

Here is the current proof, I'll take any advice !

import analysis.calculus.deriv
import analysis.calculus.mean_value

import tactic.cancel_denoms

open filter set dense_inducing

attribute [instance] classical.prop_decidable

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type*} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α → β) :
    (∀ x ∈ s, f x = g x) → tendsto f (nhds_within a s) l → tendsto g (nhds_within a s) l :=
λ h, (tendsto_congr' (mem_inf_sets_of_right (by exact h))).1

lemma tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {α β : Type*} [topological_space β] {b : β} {l : filter α} {s : set β} (f : α → β)
    (h1 : tendsto f l (nhds b)) (h2 : ∀ᶠ x in l, f x ∈ s) : tendsto f l (nhds_within b s) :=
begin
  unfold nhds_within,
  rw tendsto_inf,
  split,
  exact h1,
  exact tendsto_principal.2 h2,
end

theorem lhopital_right {a b : ℝ} {hab : a < b} (f g : ℝ → ℝ) {l : filter ℝ}
  (hdf : differentiable_on ℝ f (Ioo a b)) (hdg : differentiable_on ℝ g (Ioo a b))
  (hcf : continuous_on f (Ico a b)) (hcg : continuous_on g (Ico a b))
  (hg : ∀ x ∈ (Ioo a b), g x ≠ 0) (hg' : ∀ x ∈ (Ioo a b), (deriv g) x ≠ 0)
  (hfa : f a = 0) (hga : g a = 0)
  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (nhds_within a (Ioi a)) l) :
  tendsto (λ x, (f x) / (g x)) (nhds_within a (Ioi a)) l :=
begin
  have sub1 : ∀ x ∈ Ioo a b, Icc a x ⊆ Ico a b,
    { intros x hx,
      rw mem_Ioo at hx,
      intros y hy,
      rw mem_Icc at hy,
      rw mem_Ico,
      split, linarith, linarith},
  have sub2 : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b,
    { intros x hx,
      rw mem_Ioo at hx,
      intros y hy,
      rw mem_Ioo at hy,
      rw mem_Ioo,
      split, linarith, linarith},
  have : ∀ x, ∃ c, (x ∉ Ioo a b ∨ (c ∈ Ioo a x ∧ (f x) * ((deriv g) c) = (g x) * ((deriv f) c))),
  { intros x,
    by_cases hx : x ∈ Ioo a b,
    rw (show f x = f x - f a, by linarith),
    rw (show g x = g x - g a, by linarith),
    have := exists_ratio_deriv_eq_ratio_slope g _ _ _ f _ _,
    cases this with c hc,
    cases hc with hca hcb,
    use c,
    right,
    split, exact hca, exact hcb,
    { rw mem_Ioo at hx, linarith },
    exact continuous_on.mono hcg (sub1 x hx),
    exact differentiable_on.mono hdg (sub2 x hx),
    exact continuous_on.mono hcf (sub1 x hx),
    exact differentiable_on.mono hdf (sub2 x hx),
    use 0,
    left,
    exact hx },
  choose c hc using this,
  have : ∀ x ∈ Ioo a b, ((λ x', ((deriv f) x') / ((deriv g) x')) ∘ c) x = f x / g x,
  { intros x hx,
    unfold function.comp,
    cases hc x,
    exfalso, exact h hx,
    cases h with ha hb,
    field_simp [hg x hx, hg' (c x) ((sub2 x hx) ha)],
    symmetry,
    rwa mul_comm (deriv f (c x)) (g x) },
  have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x,
  { intros x hx,
    specialize hc x,
    cases hc,
    exfalso,
    exact hc hx,
    exact hc.1 },
  rw ← nhds_within_Ioo_eq_nhds_within_Ioi hab,
  apply tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within,
  exact this,
  change tendsto ((λ (x : ℝ), deriv f x / deriv g x) ∘ c) (nhds_within a (Ioo a b)) l,
  apply tendsto.comp,
  exact hdiv,
  apply tendsto_nhds_within_of_tendsto_nhds_of_eventually_within,
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le',
  exact tendsto_const_nhds,
  exact tendsto_nhds_within_of_tendsto_nhds tendsto_id,
  repeat
  { use univ,
    split,
    apply univ_sets,
    use Ioo a b,
    split,
    apply mem_principal_self,
    rw univ_inter,
    intros x hx,
    rw mem_set_of_eq,
    have := cmp x hx,
    try {rw mem_Ioi},
    try {unfold id},
    linarith },
end

[Johan Commelin]

Cool! It's really nice to see this being done!
(However, don't forget to PR to mathlib. It's not easy, I know. But if you don't do it, your code will rot away.)

[Johan Commelin]

One thing that I don't know (analysis is not my strongest point)... is there "one l'Hopital to rule them all"? A generalisation of the infty and -infty, and 0, cases?

[Anatole Dedecker]

Johan Commelin said:

Cool! It's really nice to see this being done!
(However, don't forget to PR to mathlib. It's not easy, I know. But if you don't do it, your code will rot away.)

Do you talk about PR-ing this or the harmonic series ?

[Johan Commelin]

Both (-;

[Johan Commelin]

But this is maybe not completely ready? I didn't look carefully

[Anatole Dedecker]

No it isn't

[Patrick Massot]

You don't have to assume that g doesn't vanish onIoo a b, it follows from the assumption on g a (provided you modify g by insisting g a = 0) , the assumption on g'` and Rolle.

[Patrick Massot]

You can shorten things using Icc_subset_Ico_right and its friends.

[Patrick Massot]

Also, the end of the proof would be easier using

lemma eventually_nhds_with_of_forall
  {α : Type*} [topological_space α] {a : α} {s : set α} {p : α → Prop}
  (h : ∀ x ∈ s, p x) : ∀ᶠ x in nhds_within a s, p x :=
mem_inf_sets_of_right h

[Anatole Dedecker]

It is indeed

[Anatole Dedecker]

Do you think L'Hopital's rule is useful enough to get into Mathlib ?

[Patrick Massot]

It doesn't have to be that useful to get into mathlib. And the fact that it needs several new lemmas about nhds_within is good.

[Kevin Buzzard]

If this is on Freek's list then mathlib will almost surely find a place for it

[Anatole Dedecker]

Do we have a canonical way to extend functions ? Right now, my strategy to get rid of the "continuous on [a,b[" hypothesis is to use the functions (λ x, cond (x ∈ Ioo a b) (f x) 0) and (λ x, cond (x ∈ Ioo a b) (g x) 0), but proving all the hypothesis to use the original lemma are true is a nightmare, and I'm still struggling to prove that these are continuous on [a,b[. So I feel like, maybe, there is something better I should be using ?

[Anatole Dedecker]

Now I'm really hoping there isn't cause I managed to do it with this. Btw this made me state and prove a few lemmas about continuous_within_at

[Patrick Massot]

The thing I know in this direction is docs#continuous_if

[Anatole Dedecker]

Ok so I managed to prove the rule for the cases where we wanna compute the limit of f/g at some real value, and I'm now working on the case where we're interested in the limit at +inf. I have a paper proof on the following lemma :

import analysis.calculus.mean_value

open filter set

theorem lhopital_zero_at_top_nhds {a : ℝ} (f g : ℝ → ℝ) {l : ℝ}
  (hdf : differentiable_on ℝ f (Ioi a)) (hdg : differentiable_on ℝ g (Ioi a))
  (hg' : ∀ x ∈ (Ioi a), (deriv g) x ≠ 0)
  (hftop : tendsto f at_top (nhds 0)) (hgtop : tendsto g at_top (nhds 0))
  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) at_top (nhds l)) :
  tendsto (λ x, (f x) / (g x)) at_top (nhds l) := sorry

which you can see here : https://drive.google.com/file/d/1nEaHw6D1B_diIVgHWxDyJu0XZo754RPq/view?usp=sharing
But I am struggling writing this in term of filters, especially because of the epsilon / 2, because you can't divide a neighborhood set x)

[Anatole Dedecker]

Maybe there's a more direct proof working for all filters, not only nhds l. I managed to do this for the finite case, but I can't wrap my head around how I should do this here

[Anatole Dedecker]

(Btw sorry for my writing, I was too lazy to make a Latex doc)

[Patrick Massot]

What you wrote on "paper" doesn't seem to match your formal statement, and seems weird.

[Anatole Dedecker]

Oh I forgot to write down a few things that were in my head, I'll reupload it soon

[Anatole Dedecker]

Is this https://drive.google.com/file/d/1c768NAsdmsuoFfQNmU-1CVBkQlIlNGJN/view?usp=sharing any better ? I thought of that "proof" at 1am, so it may be completely wrong

[Patrick Massot]

I don't have time to read the details now but it certainly looks much better

[Patrick Massot]

since it starts with listing assumptions

[Anatole Dedecker]

Indeed :laughing:

[Anatole Dedecker]

Hmmm this still doesn't seem satisfying to me so I'll try another approach

[Anatole Dedecker]

That was definitely a good idea. I should never listen to 1am me

[Anatole Dedecker]

Before I go further, either by writing a PR or working on cases where g -> infinity, I'd like to know your thoughts on what I already did, which is here : https://gitlab.com/Someody42/lhopital (sorry, I just realized there's no lean syntax highlighting on Gitlab, if someone knows about Ruby we can maybe fix that). Again, this is just me being nervous about PR-ing some absolute nonsense or anything like that, so thanks in advance for your help !

[Patrick Massot]

I had a quick look. I'm not sure we can avoid stating many variations, but certainly the proofs shouldn't be repeated like that.

[Patrick Massot]

I think a good starting point is to state and prove more general versions of Rolle.

[Patrick Massot]

You should need to assume continuity on the closed interval, and also need the version where the interval is infinite.

[Patrick Massot]

Does anyone has Bourbaki "Fonction d'une variable réelle" at hand? If they cover this L'Hopital rule we can certainly take inspiration.

[Anatole Dedecker]

Patrick Massot said:

I had a quick look. I'm not sure we can avoid stating many variations, but certainly the proofs shouldn't be repeated like that.

I hope so. I thought I'd avoid it by reducing every other case to the first one using composition, but 1) it ends up being almost as long as if I just copy-pasted the whole proof, and 2) there is also some parts of the composition mess that I ended up copy-pasting, so I would say my objective wasn't really fulfilled

[Kevin Buzzard]

Patrick Massot said:

Does anyone has Bourbaki "Fonction d'une variable réelle" at hand? If they cover this L'Hopital rule we can certainly take inspiration.

I do, but I've glanced through chapter 1 and I can't see it in there.

[Sebastien Gouezel]

Patrick Massot said:

Does anyone has Bourbaki "Fonction d'une variable réelle" at hand? If they cover this L'Hopital rule we can certainly take inspiration.

I am sure you know about this, but probably some young people don't. Since it's not completely legal though, I won't mention libgen here.

[Kevin Buzzard]

My home ISP has blocked it! But actually Imperial gives me access to all Bourbaki online via our libary :D

[Sebastien Gouezel]

I am sure you know about this, but probably some young people don't. Since it's completely legal, let me say that you can use another DNS than your provider's, for instance Google's. It could unblock some things that are blocked just at the DNS level by your provider.

[Carl Friedrich Bolz-Tereick]

That, or the Wikipedia entry usually contains up-to-date info how to reach it (same for sci-hub which should also not be mentioned)

[Anatole Dedecker]

@Patrick Massot https://universiteparissud.focus.universite-paris-saclay.fr/primo-explore/fulldisplay?docid=33UDPS_SFX1000000000282794&context=L&vid=33UDPS_VU1&lang=fr_FR&search_scope=default_scope&adaptor=Local%20Search%20Engine&tab=default_tab&query=any,contains,fonctions%20d%27une%20variable%20r%C3%A9elle%20bourbaki&offset=0&pcAvailability=false

[Anatole Dedecker]

The legal way x)

[Patrick Massot]

All those almost legal ways are still much less convenient that having the book in your hand, right? Bu thanks anyway

[Patrick Massot]

Did anyone found what we are looking for in all those pdfs?

[Anatole Dedecker]

I didn't :oh_no: In mine it is just evoked as a special application of series expansion

[Patrick Massot]

Under which assumptions?

[Patrick Massot]

Where is that?

[Anatole Dedecker]

Actually this is more of an historical reference, they don't even state it rigorously

[Anatole Dedecker]

Oh

[Anatole Dedecker]

It's in "historical reference"

[Anatole Dedecker]

So no concrete math here (p 288)

[Patrick Massot]

That's probably assuming differentiability at the point where you take the limit (which is of course the trivial case)

[Anatole Dedecker]

Yup

[Patrick Massot]

So it seems they didn't care about the non-trivial case.

[Patrick Massot]

They don't even state several version of Rolle. Of course all variations are mathematically obviously equivalent to what they state.

[Patrick Massot]

The wiki webpage that you cited a long time ago is actually extremely sloppy here. They write the usual version of Rolle and then seem to apply it without having the required assumptions.

[Anatole Dedecker]

It works for the trivial case, but it soon starts to fail yes

[Patrick Massot]

Did you try to state and prove a version of Rolle where you assume $f'$ exists on $(a, b)$ and $f$ tends to zero at $a$ and $b$?

[Patrick Massot]

beware of the stupid international notation for $\left]a, b\right[$

[Anatole Dedecker]

(still more logical than the whole "non increasing" nonsense :laughing: ). Jokes aside I didn't, I'll look at it

[Patrick Massot]

Of course on paper there is nothing to say, you can just redefine $f$ to vanish at $a$ and $b$ and the conclusion of the theorem is unaffected while the assumption become standard.

[Patrick Massot]

But in Lean this could be painful. I don't even know if it would be easier to redo the proof or use the existing lemma.

[Anatole Dedecker]

I did work with redefining for lhopital_zero_at_left_of_Ioo, and it was quite painful indeed

[Patrick Massot]

Oh, why did you work with cond instead of if?

[Patrick Massot]

cond is the bool version, this is for programming, not math.

[Anatole Dedecker]

Well... I didn't know about if yet :sweat_smile:

[Anatole Dedecker]

But yeah that could simplify a lot of things indeed

[Patrick Massot]

It probably wouldn't change much, but you can write λ x, if x ∈ Ioo a b then f x else 0

[Patrick Massot]

That probably have more useful lemmas already proved

[Anatole Dedecker]

Such as the continuous_if you already mentioned...

[Patrick Massot]

continuous_if is not enough because it assumes too much. We need the version I wrote for the sphere eversion project.

[Patrick Massot]

https://github.com/leanprover-community/sphere-eversion/blob/master/src/gluing.lean#L107-L111

[Patrick Massot]

and its special case https://github.com/leanprover-community/sphere-eversion/blob/master/src/gluing.lean#L168-L170

[Patrick Massot]

except we need another special case of course.

[Anatole Dedecker]

A bit like my continuous_on_Ico_of_extend_continuous_Ioo ?

[Anatole Dedecker]

With ite rather than cond of course

[Anatole Dedecker]

(in lemmas.lean)

[Patrick Massot]

yes

[Reid Barton]

When I wanted to prove something like this I used continuous_subtype_is_closed_cover. We should probably have a version for two subsets.

[Patrick Massot]

Oh this is a nice one.

[Patrick Massot]

Wait, it doesn't help at all here, right?

[Patrick Massot]

Which means mine also doesn't help.

[Patrick Massot]

:lol: the statement of docs#exists_deriv_eq_zero is really cute.

[Patrick Massot]

Notice how it doesn't assume any differentiability.

[Anatole Dedecker]

Yup, I did notice

[Patrick Massot]

Because deriv f is defined to be zero at x if f is not differentiable at x.

[Sebastien Gouezel]

This is much more evil than 1/0. I suggest Kevin doesn't mention this on twitter.

[Patrick Massot]

Yeah, let's git blame that one.

[Sebastien Gouezel]

I guess Yury.

[Patrick Massot]

If not you then certainly Yury

[Patrick Massot]

GitHub says Yury but also https://github.com/leanprover-community/mathlib/pull/1807#pullrequestreview-334554896

[Patrick Massot]

Oh, I just found a way to put emoji reactions to my own messages.

[Sebastien Gouezel]

In fact, the assumptions of the theorem are too strong; you just need to assume continuity within Icc a b at the endpoints, not in the middle.

[Patrick Massot]

Who would have guess we could make such huge progress on this classic theorem!

[Reid Barton]

Why not just define the derivative of a function that doesn't satisfy Rolle's theorem to be 0 and be done with it

[Anatole Dedecker]

x)

[Anatole Dedecker]

Patrick Massot said:

Did you try to state and prove a version of Rolle where you assume $f'$ exists on $(a, b)$ and $f$ tends to zero at $a$ and $b$?

Why "$f$ tends to zero at $a$ and $b$" ? I mean in my case that's what I need, but in general $f$ tends to the same $l\in\mathbb{R}$ at $a$ and $b$ should suffice, no ?

[Patrick Massot]

Sure, that's what I meant

[Anatole Dedecker]

Sebastien Gouezel said:

In fact, the assumptions of the theorem are too strong; you just need to assume continuity within Icc a b at the endpoints, not in the middle.

That's actually quite a big problem, because it means I cannot use it by redefining the function at a and b : it won't be continuous on Icc a b if it wasn't originally on Ioo a b

[Anatole Dedecker]

Guess I'll have to make variations of exists_Ioo_extr_on_Icc and exists_local_extr_Ioo too

[Patrick Massot]

Maybe yes, maybe not.

[Anatole Dedecker]

Rah, congr lemmas are really lacking sometimes. Anyway, I'll continue tomorrow

[Anatole Dedecker]

Okay so, back after a 2-day lean break, I finally managed to prove this stronger Rolle :

theorem exists_deriv_eq_zero' (f : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
  (hfa : tendsto f (nhds_within a $ Ioo a b) (nhds l)) (hfb : tendsto f (nhds_within b $ Ioo a b) (nhds l)) :
  ∃ c ∈ Ioo a b, deriv f c = 0 := sorry

[Anatole Dedecker]

Funny how we don't even need continuity for this one to work x)

[Patrick Massot]

Note this is what Sébastien announced.

[Patrick Massot]

It does look very fishy.

[Patrick Massot]

But I can totally see the proof.

[Patrick Massot]

This is insane.

[Patrick Massot]

I claim that Lean damaged Sébastien's mind. Otherwise he wouldn't have immediately seen this statement.

[Patrick Massot]

You're part of our secret society now, you must swear not to tell anyone about this lemma outside this place, even (especially?) in your family.

[Kevin Buzzard]

This is just nuts

[Kevin Buzzard]

The point is just that if it's not math-differentiable on the interval then the lean derivative is zero?

[Anatole Dedecker]

Patrick Massot said:

You're part of our secret society now, you must swear not to tell anyone about this lemma outside this place, even (especially?) in your family.

I want to know what my father would say if I tell him what Sebastien told me to prove :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

I'm definitely going to mention this on Twitter

[Patrick Massot]

Yes Kevin, if there is any point in the interior where f is not continuous then it's also not differentiable there, hence you can pick that point and the derivative there is zero by definition.

[Patrick Massot]

Kevin, you're a completely failed cabalist.

[Patrick Massot]

If you really want to do that you should prepare explanation about about you still need the reasonable assumptions as soon as you want to deduce anything non empty from this.

[Patrick Massot]

I want to know what my father would say if I tell him what Sebastien told me to prove :grinning_face_with_smiling_eyes:

For those who didn't get this: Anatole's father is a mathematician who wrote several papers with Sébastien. Now I'm sure he'll blame Covid for not allowing Anatole to return to my university in September.

[Anatole Dedecker]

I wouldn't say "several" though, I do only count 4 on my father's homepage (though it's a bit outdated, I'm supposed to work on that too :laughing: )

[Anatole Dedecker]

Little progress update : I have proven a similar version of Cauchy's mean value theorem :

theorem exists_ratio_deriv_eq_ratio_slope' (f g : ℝ → ℝ) {a b lfa lga lfb lgb : ℝ} (hab : a < b) (hdf : differentiable_on ℝ f $ Ioo a b)
  (hdg : differentiable_on ℝ g $ Ioo a b) (hfa : tendsto f (nhds_within a $ Ioo a b) (nhds lfa)) (hga : tendsto g (nhds_within a $ Ioo a b) (nhds lga))
  (hfb : tendsto f (nhds_within b $ Ioo a b) (nhds lfb)) (hgb : tendsto g (nhds_within b $ Ioo a b) (nhds lgb)) :
∃ c ∈ Ioo a b, (lgb - lga) * (deriv f c) = (lfb - lfa) * (deriv g c) := sorry

Thus I can now prove

theorem lhopital_zero_at_left_of_Ioo {a b : ℝ} {hab : a < b} (f g : ℝ → ℝ) {l : filter ℝ}
  (hdf : differentiable_on ℝ f (Ioo a b)) (hdg : differentiable_on ℝ g (Ioo a b))
  (hg' : ∀ x ∈ (Ioo a b), (deriv g) x ≠ 0)
  (hfa : tendsto f (nhds_within a (Ioi a)) (nhds 0)) (hga : tendsto g (nhds_within a (Ioi a)) (nhds 0))
  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (nhds_within a (Ioi a)) l) :
  tendsto (λ x, (f x) / (g x)) (nhds_within a (Ioi a)) l :=

without doing all the if-then-else stuff here, and most importantly without relying on the Ico version as I did before

[Anatole Dedecker]

Which means the Ico version proof is now down to :

theorem lhopital_zero_at_left_of_Ico' {a b : ℝ} {hab : a < b} (f g : ℝ → ℝ) {l : filter ℝ}
  (hdf : differentiable_on ℝ f (Ioo a b)) (hdg : differentiable_on ℝ g (Ioo a b))
  (hcf : continuous_on f (Ico a b)) (hcg : continuous_on g (Ico a b))
  (hg' : ∀ x ∈ (Ioo a b), (deriv g) x ≠ 0)
  (hfa : f a = 0) (hga : g a = 0)
  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (nhds_within a (Ioi a)) l) :
  tendsto (λ x, (f x) / (g x)) (nhds_within a (Ioi a)) l :=
begin
  apply lhopital_zero_at_left_of_Ioo f g hdf hdg hg',
  rw [← hfa, ← nhds_within_Ioo_eq_nhds_within_Ioi],
  exact continuous_within_at.tendsto (continuous_within_at.mono (hcf a $ left_mem_Ico.mpr hab) Ioo_subset_Ico_self),
  exact hab,
  rw [← hga, ← nhds_within_Ioo_eq_nhds_within_Ioi],
  exact continuous_within_at.tendsto (continuous_within_at.mono (hcg a $ left_mem_Ico.mpr hab) Ioo_subset_Ico_self),
  exact hab,
  exact hdiv,
  exact hab
end

[Anatole Dedecker]

I just noticed both Rolle and Cauchy were originally written using has_deriv, should I do that too ?

[Patrick Massot]

I think you can go back and forth between stating stuff with has_deriv and differentiable_at.

[Patrick Massot]

Anatole Dedecker said:

Okay so, back after a 2-day lean break, I finally managed to prove this stronger Rolle :

theorem exists_deriv_eq_zero' (f : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
  (hfa : tendsto f (nhds_within a $ Ioo a b) (nhds l)) (hfb : tendsto f (nhds_within b $ Ioo a b) (nhds l)) :
  ∃ c ∈ Ioo a b, deriv f c = 0 := sorry

I wanted to come back to this in case Kevin can't keep a secret. For the record, here is a proof that this statement contains the reasonable statement:

theorem rolle (f : ℝ → ℝ) {a b l : ℝ} (hab : a < b)
  (hfa : tendsto f (nhds_within a $ Ioo a b) (nhds l)) (hfb : tendsto f (nhds_within b $ Ioo a b) (nhds l))
  (h : ∀ x ∈ Ioo a b, differentiable_at ℝ f x):
  ∃ c ∈ Ioo a b, is_o (λ x, f x - f c) (λ x, x - c) (𝓝 c) :=
begin
  rcases exists_deriv_eq_zero' f hab hfa hfb with ⟨c, c_in, hc⟩,
  use [c, c_in],
  convert differentiable_at.has_deriv_at (h c c_in),
  ext x, simp [hc],
end