Generalized Rolle theorem

Stream: new members

[Dan Stanescu]

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 $f$ is $n$-times differentiable and has $(n+1)$ zeroes in $[a,b]$ then $f^n$ has at least one zero in $(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.

[Yury G. Kudryashov]

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.

[Dan Stanescu]

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

[Jalex Stark]

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

[Dan Stanescu]

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

[Reid Barton]

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

[Dan Stanescu]

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

[Dan Stanescu]

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

[Reid Barton]

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

[Dan Stanescu]

I get an error if I do that.

[Dan Stanescu]

Not the same.

[Reid Barton]

revert x too

[Dan Stanescu]

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

[Dan Stanescu]

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.

[Sebastien Gouezel]

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.

[Dan Stanescu]

Thank you, @Sebastien Gouezel !

[Dan Stanescu]

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

[Dan Stanescu]

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

[Dan Stanescu]

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 ?

[Bryan Gin-ge Chen]

What's their github username?

[A. Stone Olguin]

Hi, my GitHub username is StoneOlguin

[Bryan Gin-ge Chen]

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

[Alex J. Best]

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

[Dan Stanescu]

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.

[Alex J. Best]

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

[Dan Stanescu]

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

[Sebastien Gouezel]

One-dimensional iterated smoothness result PRed in #4017