Zulip Chat Archive

Stream: new members

Topic: Generalized Rolle theorem


view this post on Zulip Dan Stanescu (Aug 02 2020 at 14:27):

Trying to reproduce in Lean some results in numerical analysis that have been obtained in Coq, article by T. Coquand and B. Spitters here. To do so I need a generalized version of Rolle's theorem: if ff is nn-times differentiable and has (n+1)(n+1) zeroes in [a,b][a,b] then fnf^n has at least one zero in (a,b)(a,b). I basically have the proof of one version of this ready, so I'm looking for input on the way I formulated the statement in case this ends up in mathlib. A slightly stronger version which would be enough for my purpose and roughly correspond to exists_has_deriv_at_eq_zero, would be:

theorem general_rolle (n : ) (A B : ) (hAB : A < B) :
     (f :   ), times_cont_diff_on  (n+1) f (Icc A B) 
    ( (x : fin(n+2)  ),
         (i j : fin (n+2)), x i  (Icc A B)  f (x i) = 0  (i < j  x i < x j) ) 
     c  Ioo A B, iterated_deriv (n+1) f c = 0 := sorry

while relaxing to times_cont_diff_on ℝ n would correspond to exists_deriv_eq_zero. Unless I'm wrong, the latter can be used for example to produce a point c \in Ioo -1 1 where deriv abs is zero, which is not surprising since deriv is set to zero wherever not defined.
@Yury G. Kudryashov wrote the standard versions so in particular I'm pinging him here for guidance.

view this post on Zulip Yury G. Kudryashov (Aug 02 2020 at 20:03):

A few comments. I'll try to leave more later tonight.

  1. Why do you need n > 0?
  2. You should make x an argument and separate ∀ i, x i ∈ Icc A B, ∀ i, f (x i) = 0 and strict_mono x into different assumptions.
  3. Another way is to assume that there exists s : finset ℝ, s.card = n + 2 etc.
  4. Would it be hard to prove a version with a multiset instead of a finset?
  5. Your version requires that the (n+1)st derivative is continuous. I think that this is not required.

view this post on Zulip Dan Stanescu (Aug 02 2020 at 20:28):

Thank you Yury! My feedback:
(5) You're right about (5) and I mentioned that in my original post. See also the weaker variant below. I thought we should have both, just like the two standard versions.
(1) Not sure I understand (1); n=0 is allowed and it folds back onto the standard Rolle in mathlib. Again, see below.
(2) Great idea. I'm slowly getting used to the many tools in mathlib.
(4) Not sure about multiset, didn't use it before, but I see no advantage in having to worry about duplicates. Also related to (3), it seemed to me that out of all variants, the fin \to \R is the best to work with because of easy coercions.

One more thing that I didn't mention before: when I got started I had (f : ℝ → ℝ) before the colon, but I was having trouble with that when in the induction proof I needed to move the induction hypothesis from f to deriv f. There may be some way to do that, but it was easier to use the universal quantifier after the colon.

theorem weak_general_rolle (n : ) (A B : ) (hAB : A < B) :
     (f :   ), times_cont_diff_on  n f (Icc A B) 
    ( (x : fin(n+2)  ),
         (i j : fin (n+2)), x i  (Icc A B)  f (x i) = 0  (i < j  x i < x j) ) 
     c  Ioo A B, iterated_deriv (n+1) f c = 0 := sorry

view this post on Zulip Jalex Stark (Aug 03 2020 at 00:04):

revert is adjoint to intro and is often useful right before calling an induction lemma

view this post on Zulip Dan Stanescu (Aug 03 2020 at 00:15):

Thanks Jalex, I tried using revert in this case with no success. It may just be me though!

view this post on Zulip Reid Barton (Aug 03 2020 at 00:53):

I'm not sure I follow, but the usual pattern is to revert stuff that "varies" in the induction (like f here), use induction, then intro the things you reverted again--now you have the same goal as originally but the induction hypothesis is more general

view this post on Zulip Dan Stanescu (Aug 03 2020 at 02:17):

Here's a MWE to show what I mean, and I'll also post the other scenario:

import analysis.calculus.local_extr
import analysis.calculus.iterated_deriv
import tactic
open set

theorem general_rolle (n : ) (A B : ) (hAB : A < B) :
     (f :   ), times_cont_diff_on  n f (Icc A B) 
    ( (x : fin(n+2)  ),
         (i j : fin (n+2)), x i  (Icc A B)  f (x i) = 0  (i < j  x i < x j) ) 
     c  Ioo A B, iterated_deriv (n+1) f c = 0 :=
begin
    induction n with d hd,
    { -- base case, unfolds to plain Rolle `exists_deriv_eq_zero`
      sorry,
    },
    { -- induction step
        -- the derivative is in Cᵈ
        intros f hf hxf,
        set g := deriv f with hg,
        have hder : times_cont_diff_on  d g (Icc A B), sorry,
        have hdg := hd g hder, clear hd, --apply hd to g = deriv f; works here
        sorry,
    },
    done
end

view this post on Zulip Dan Stanescu (Aug 03 2020 at 02:27):

Here's the way I started but couldn't make it work:

theorem general_rolle (n : ) (A B : ) (hAB : A < B) (f :   )
   (hf : times_cont_diff_on  n f (Icc A B) ) (x : fin(n+2)  )
   (hx :   (i j : fin (n+2)), x i  (Icc A B)  f (x i) = 0  (i < j  x i < x j) )  :
     c  Ioo A B, iterated_deriv (n+1) f c = 0 :=
begin
    induction n with d hd,
    { -- base case, unfolds to plain Rolle `exists_deriv_eq_zero`
      sorry,
    },
    { -- induction step
        -- the derivative is in Cᵈ
        set g := deriv f with hg,
        have hder : times_cont_diff_on  d g (Icc A B), sorry,
        have hdg := hd g,  --apply hd to g = deriv f; can't do that here
        sorry,
    },
    done
end

view this post on Zulip Reid Barton (Aug 03 2020 at 02:28):

revert f first, then you should be in the same situation as in the first example

view this post on Zulip Dan Stanescu (Aug 03 2020 at 02:28):

I get an error if I do that.

view this post on Zulip Dan Stanescu (Aug 03 2020 at 02:29):

Not the same.

view this post on Zulip Reid Barton (Aug 03 2020 at 02:31):

revert x too

view this post on Zulip Dan Stanescu (Aug 03 2020 at 02:35):

I tried that too and couldn't make it work. Can someone do it on the MWE?
If I revert f I don't have deriv f any longer. To get it, I have to intro f and that places me in the same spot as before. Of course I may be missing something-:(

view this post on Zulip Dan Stanescu (Aug 04 2020 at 13:12):

I thought this, the last sorry in my main proof, was easy. It turns out I can't find an easy way, if there's one. Help appreciated!

import analysis.calculus.local_extr
import analysis.calculus.times_cont_diff
import analysis.calculus.iterated_deriv
import tactic
open set

example (a b : ) (hab : a < b) (f :   ) (n : ) (hf : times_cont_diff_on  (n+1) f (Ioo a b) ) :
    times_cont_diff_on  n (deriv f) (Ioo a b) := sorry

In my initial setup I have Icc instead in fact, which perfectly folds the induction base case onto the standard Rolle version in mathlib, but am not sure was a good decision.

view this post on Zulip Sebastien Gouezel (Aug 04 2020 at 19:54):

Here is a proof:

import analysis.calculus.local_extr
import analysis.calculus.times_cont_diff
import analysis.calculus.iterated_deriv
import tactic
open set

example (a b : ) (hab : a < b) (f :   ) (n : ) (hf : times_cont_diff_on  (n+1) f (Ioo a b) ) :
  times_cont_diff_on  n (deriv f) (Ioo a b) :=
begin
  have : deriv f = (λ u :  L[] , u 1)  (fderiv  f), by { ext x, refl },
  simp only [this],
  have : times_cont_diff_on  n (fderiv  f) (Ioo a b),
  { apply ((times_cont_diff_on_succ_iff_fderiv_within (unique_diff_on_Ioo a b)).1 hf).2.congr,
    assume x hx,
    calc fderiv  f x = fderiv_within  f univ x : by simp
    ... = fderiv_within  f (univ  Ioo a b) x :
      (fderiv_within_inter (Ioo_mem_nhds hx.1 hx.2) unique_diff_within_at_univ).symm
    ... = fderiv_within  f (Ioo a b) x : by simp },
  apply times_cont_diff.comp_times_cont_diff_on _ this,
  exact (is_bounded_bilinear_map_apply.is_bounded_linear_map_left _).times_cont_diff
end

We have essentially no specific results for smooth functions in one dimension, this is why it is a little bit painful.

view this post on Zulip Dan Stanescu (Aug 04 2020 at 20:32):

Thank you, @Sebastien Gouezel !

view this post on Zulip Dan Stanescu (Aug 04 2020 at 21:22):

So if I understand correctly we need more API in 1D.

view this post on Zulip Dan Stanescu (Aug 04 2020 at 21:22):

Can this be extended to Icc a b? Must confess currently I wouldn't know how.

view this post on Zulip Dan Stanescu (Aug 12 2020 at 21:31):

This proof is now ready. Submitting to mathlib still hinges on the lemma due to @Sebastien Gouezel above in this thread and a few other fin lemmas. Maybe I should also say there's some cleaning that needs to be done. Here's a link to the proof for anyone interested:

https://github.com/stanescuUW/numerical-analysis-with-Lean/blob/master/src/Interpolation/rolle_general-fin.lean

@maintainers Will you please provide write access to a branch of mathlib for @A. Stone Olguin ?

view this post on Zulip Bryan Gin-ge Chen (Aug 12 2020 at 21:34):

What's their github username?

view this post on Zulip A. Stone Olguin (Aug 12 2020 at 21:43):

Hi, my GitHub username is StoneOlguin

view this post on Zulip Bryan Gin-ge Chen (Aug 12 2020 at 21:57):

Invitation sent! https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Alex J. Best (Aug 12 2020 at 22:00):

How does this generalized Rolle compare with the result called higher order Rolle in https://gowers.wordpress.com/2014/02/11/taylors-theorem-with-the-lagrange-form-of-the-remainder/ ?

view this post on Zulip Dan Stanescu (Aug 12 2020 at 22:41):

The version that is proved here is the usual generalization on Wikipedia, because that's what's needed to obtain the truncation error for interpolation, see also the link to T. Coquand's paper in the first message in this thred:

https://en.wikipedia.org/wiki/Rolle%27s_theorem#Generalization

Will need to take a closer look at the link you point to @Alex J. Best, at first glance it seems an equivalent formulation that I have never seen used before.

view this post on Zulip Alex J. Best (Aug 12 2020 at 22:43):

Yeah this was just idle curiosity on my part, I'll check out Coquand thanks!

view this post on Zulip Dan Stanescu (Aug 12 2020 at 23:03):

No way! Instead, thank you for bringing it to my attention.

view this post on Zulip Sebastien Gouezel (Sep 01 2020 at 11:27):

One-dimensional iterated smoothness result PRed in #4017


Last updated: May 12 2021 at 04:19 UTC