## Stream: new members

### Topic: L'Hopital's rule

(deleted)

(deleted)

#### Anatole Dedecker (Jun 27 2020 at 17:16):

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 (Jun 27 2020 at 17:40):

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 (Jun 27 2020 at 17:41):

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 (Jun 27 2020 at 19:12):

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 ?

Both (-;

#### Johan Commelin (Jun 27 2020 at 19:25):

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

No it isn't

#### Patrick Massot (Jun 27 2020 at 20:50):

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 (Jun 27 2020 at 20:50):

You can shorten things using Icc_subset_Ico_right and its friends.

#### Patrick Massot (Jun 27 2020 at 21:29):

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

It is indeed

#### Anatole Dedecker (Jun 27 2020 at 21:36):

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

#### Patrick Massot (Jun 27 2020 at 21:42):

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 (Jun 28 2020 at 04:31):

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

#### Anatole Dedecker (Jun 28 2020 at 12:26):

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 (Jun 28 2020 at 15:18):

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 (Jun 28 2020 at 17:29):

The thing I know in this direction is docs#continuous_if

#### Anatole Dedecker (Jul 04 2020 at 14:24):

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 (Jul 04 2020 at 14:25):

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 (Jul 04 2020 at 14:26):

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

#### Patrick Massot (Jul 04 2020 at 14:38):

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

#### Anatole Dedecker (Jul 04 2020 at 14:41):

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

#### Anatole Dedecker (Jul 04 2020 at 14:58):

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 (Jul 04 2020 at 15:07):

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

#### Patrick Massot (Jul 04 2020 at 15:07):

since it starts with listing assumptions

#### Anatole Dedecker (Jul 04 2020 at 15:08):

Indeed :laughing:

#### Anatole Dedecker (Jul 04 2020 at 15:42):

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

#### Anatole Dedecker (Jul 04 2020 at 19:22):

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

#### Anatole Dedecker (Jul 06 2020 at 13:39):

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 (Jul 06 2020 at 18:11):

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 (Jul 06 2020 at 18:11):

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

#### Patrick Massot (Jul 06 2020 at 18:13):

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

#### Patrick Massot (Jul 06 2020 at 18:13):

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 (Jul 06 2020 at 18:20):

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 (Jul 06 2020 at 19:05):

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 (Jul 06 2020 at 19:08):

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 (Jul 06 2020 at 19:10):

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

#### Sebastien Gouezel (Jul 06 2020 at 19:14):

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 (Jul 06 2020 at 19:15):

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)

The legal way x)

#### Patrick Massot (Jul 06 2020 at 20:00):

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

#### Patrick Massot (Jul 06 2020 at 20:00):

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

#### Anatole Dedecker (Jul 06 2020 at 20:05):

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

#### Patrick Massot (Jul 06 2020 at 20:06):

Under which assumptions?

Where is that?

#### Anatole Dedecker (Jul 06 2020 at 20:08):

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

Oh

#### Anatole Dedecker (Jul 06 2020 at 20:08):

It's in "historical reference"

#### Anatole Dedecker (Jul 06 2020 at 20:09):

So no concrete math here (p 288)

#### Patrick Massot (Jul 06 2020 at 20:09):

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

Yup

#### Patrick Massot (Jul 06 2020 at 20:10):

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

#### Patrick Massot (Jul 06 2020 at 20:11):

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

#### Patrick Massot (Jul 06 2020 at 20:12):

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 (Jul 06 2020 at 20:15):

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

#### Patrick Massot (Jul 06 2020 at 20:20):

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 (Jul 06 2020 at 20:20):

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

#### Anatole Dedecker (Jul 06 2020 at 20:22):

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

#### Patrick Massot (Jul 06 2020 at 20:23):

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 (Jul 06 2020 at 20:24):

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 (Jul 06 2020 at 20:25):

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

#### Patrick Massot (Jul 06 2020 at 20:26):

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

#### Patrick Massot (Jul 06 2020 at 20:26):

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

#### Anatole Dedecker (Jul 06 2020 at 20:26):

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

#### Anatole Dedecker (Jul 06 2020 at 20:28):

But yeah that could simplify a lot of things indeed

#### Patrick Massot (Jul 06 2020 at 20:28):

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

#### Patrick Massot (Jul 06 2020 at 20:29):

That probably have more useful lemmas already proved

#### Anatole Dedecker (Jul 06 2020 at 20:29):

Such as the continuous_if you already mentioned...

#### Patrick Massot (Jul 06 2020 at 20:33):

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

#### Patrick Massot (Jul 06 2020 at 20:33):

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

#### Patrick Massot (Jul 06 2020 at 20:35):

except we need another special case of course.

#### Anatole Dedecker (Jul 06 2020 at 20:37):

A bit like my continuous_on_Ico_of_extend_continuous_Ioo ?

#### Anatole Dedecker (Jul 06 2020 at 20:37):

With ite rather than cond of course

(in lemmas.lean)

yes

#### Reid Barton (Jul 06 2020 at 20:42):

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 (Jul 06 2020 at 20:43):

Oh this is a nice one.

#### Patrick Massot (Jul 06 2020 at 20:45):

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

#### Patrick Massot (Jul 06 2020 at 20:46):

Which means mine also doesn't help.

#### Patrick Massot (Jul 06 2020 at 20:47):

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

#### Patrick Massot (Jul 06 2020 at 20:48):

Notice how it doesn't assume any differentiability.

#### Anatole Dedecker (Jul 06 2020 at 20:48):

Yup, I did notice

#### Patrick Massot (Jul 06 2020 at 20:48):

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

#### Sebastien Gouezel (Jul 06 2020 at 20:55):

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

#### Patrick Massot (Jul 06 2020 at 20:55):

Yeah, let's git blame that one.

I guess Yury.

#### Patrick Massot (Jul 06 2020 at 20:57):

If not you then certainly Yury

#### Patrick Massot (Jul 06 2020 at 20:57):

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

#### Patrick Massot (Jul 06 2020 at 20:58):

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

#### Sebastien Gouezel (Jul 06 2020 at 21:01):

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 (Jul 06 2020 at 21:02):

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

#### Reid Barton (Jul 06 2020 at 21:11):

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

x)

#### Anatole Dedecker (Jul 06 2020 at 21:20):

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 (Jul 06 2020 at 21:20):

Sure, that's what I meant

#### Anatole Dedecker (Jul 06 2020 at 21:52):

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 (Jul 06 2020 at 21:56):

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

#### Patrick Massot (Jul 06 2020 at 21:57):

Maybe yes, maybe not.

#### Anatole Dedecker (Jul 06 2020 at 22:15):

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

#### Anatole Dedecker (Jul 09 2020 at 21:44):

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 (Jul 09 2020 at 21:46):

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

#### Patrick Massot (Jul 09 2020 at 21:51):

Note this is what Sébastien announced.

#### Patrick Massot (Jul 09 2020 at 21:51):

It does look very fishy.

#### Patrick Massot (Jul 09 2020 at 21:52):

But I can totally see the proof.

This is insane.

#### Patrick Massot (Jul 09 2020 at 21:55):

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

#### Patrick Massot (Jul 09 2020 at 21:59):

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 (Jul 09 2020 at 21:59):

This is just nuts

#### Kevin Buzzard (Jul 09 2020 at 22:00):

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

#### Anatole Dedecker (Jul 09 2020 at 22:00):

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 (Jul 09 2020 at 22:02):

I'm definitely going to mention this on Twitter

#### Patrick Massot (Jul 09 2020 at 22:03):

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 (Jul 09 2020 at 22:04):

Kevin, you're a completely failed cabalist.

#### Patrick Massot (Jul 09 2020 at 22:05):

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 (Jul 09 2020 at 22:06):

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 (Jul 09 2020 at 22:11):

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 (Jul 10 2020 at 14:46):

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 (Jul 10 2020 at 15:01):

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 (Jul 10 2020 at 15:02):

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

#### Patrick Massot (Jul 10 2020 at 16:06):

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

#### Patrick Massot (Jul 10 2020 at 16:10):

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

Last updated: May 14 2021 at 00:42 UTC