Zulip Chat Archive

Stream: new members

Topic: L'Hopital's rule


view this post on Zulip Anatole Dedecker (Jun 27 2020 at 17:13):

(deleted)

view this post on Zulip Anatole Dedecker (Jun 27 2020 at 17:14):

(deleted)

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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 ?

view this post on Zulip Johan Commelin (Jun 27 2020 at 19:25):

Both (-;

view this post on Zulip Johan Commelin (Jun 27 2020 at 19:25):

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

view this post on Zulip Anatole Dedecker (Jun 27 2020 at 19:25):

No it isn't

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:50):

You can shorten things using Icc_subset_Ico_right and its friends.

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Jun 27 2020 at 21:36):

It is indeed

view this post on Zulip Anatole Dedecker (Jun 27 2020 at 21:36):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jun 28 2020 at 17:29):

The thing I know in this direction is docs#continuous_if

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Jul 04 2020 at 14:26):

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

view this post on Zulip Patrick Massot (Jul 04 2020 at 14:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 04 2020 at 15:07):

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

view this post on Zulip Patrick Massot (Jul 04 2020 at 15:07):

since it starts with listing assumptions

view this post on Zulip Anatole Dedecker (Jul 04 2020 at 15:08):

Indeed :laughing:

view this post on Zulip Anatole Dedecker (Jul 04 2020 at 15:42):

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

view this post on Zulip Anatole Dedecker (Jul 04 2020 at 19:22):

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

view this post on Zulip 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 !

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 06 2020 at 18:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 19:19):

@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

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 19:19):

The legal way x)

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:00):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:06):

Under which assumptions?

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:08):

Where is that?

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:08):

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

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:08):

Oh

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:08):

It's in "historical reference"

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:09):

So no concrete math here (p 288)

view this post on Zulip 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)

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:10):

Yup

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:10):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:15):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:20):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:20):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:23):

Of course on paper there is nothing to say, you can just redefine ff to vanish at aa and bb and the conclusion of the theorem is unaffected while the assumption become standard.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:26):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:26):

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

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:26):

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

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:28):

But yeah that could simplify a lot of things indeed

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:29):

That probably have more useful lemmas already proved

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:29):

Such as the continuous_if you already mentioned...

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:33):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:34):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:35):

except we need another special case of course.

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:37):

A bit like my continuous_on_Ico_of_extend_continuous_Ioo ?

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:37):

With ite rather than cond of course

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:38):

(in lemmas.lean)

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:39):

yes

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:43):

Oh this is a nice one.

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:45):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:46):

Which means mine also doesn't help.

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:47):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:48):

Notice how it doesn't assume any differentiability.

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 20:48):

Yup, I did notice

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:55):

Yeah, let's git blame that one.

view this post on Zulip Sebastien Gouezel (Jul 06 2020 at 20:56):

I guess Yury.

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:57):

If not you then certainly Yury

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:57):

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

view this post on Zulip Patrick Massot (Jul 06 2020 at 20:58):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 06 2020 at 21:02):

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

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 21:11):

x)

view this post on Zulip 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 ff' exists on (a,b)(a, b) and ff tends to zero at aa and bb?

Why "ff tends to zero at aa and bb" ? I mean in my case that's what I need, but in general ff tends to the same lRl\in\mathbb{R} at aa and bb should suffice, no ?

view this post on Zulip Patrick Massot (Jul 06 2020 at 21:20):

Sure, that's what I meant

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jul 06 2020 at 21:57):

Maybe yes, maybe not.

view this post on Zulip Anatole Dedecker (Jul 06 2020 at 22:15):

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

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Jul 09 2020 at 21:46):

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

view this post on Zulip Patrick Massot (Jul 09 2020 at 21:51):

Note this is what Sébastien announced.

view this post on Zulip Patrick Massot (Jul 09 2020 at 21:51):

It does look very fishy.

view this post on Zulip Patrick Massot (Jul 09 2020 at 21:52):

But I can totally see the proof.

view this post on Zulip Patrick Massot (Jul 09 2020 at 21:52):

This is insane.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 21:59):

This is just nuts

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Jul 09 2020 at 22:02):

I'm definitely going to mention this on Twitter

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jul 09 2020 at 22:04):

Kevin, you're a completely failed cabalist.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: )

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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