# Zulip Chat Archive

## Stream: new members

### Topic: Generalized Rolle theorem

#### 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 $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 (Aug 02 2020 at 20:03):

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

- Why do you need
`n > 0`

? - 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. - Another way is to assume that there exists
`s : finset ℝ`

,`s.card = n + 2`

etc. - Would it be hard to prove a version with a
`multiset`

instead of a`finset`

? - Your version requires that the
`(n+1)`

st derivative is continuous. I think that this is not required.

#### 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
```

#### Jalex Stark (Aug 03 2020 at 00:04):

`revert`

is adjoint to `intro`

and is often useful right before calling an induction lemma

#### 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!

#### 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

#### 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
```

#### 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
```

#### Reid Barton (Aug 03 2020 at 02:28):

`revert f`

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

#### Dan Stanescu (Aug 03 2020 at 02:28):

I get an error if I do that.

#### Dan Stanescu (Aug 03 2020 at 02:29):

Not the same.

#### Reid Barton (Aug 03 2020 at 02:31):

revert `x`

too

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

#### 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.

#### 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.

#### Dan Stanescu (Aug 04 2020 at 20:32):

Thank you, @Sebastien Gouezel !

#### Dan Stanescu (Aug 04 2020 at 21:22):

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

#### Dan Stanescu (Aug 04 2020 at 21:22):

Can this be extended to `Icc a b`

? Must confess currently I wouldn't know how.

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

@maintainers Will you please provide write access to a branch of `mathlib`

for @A. Stone Olguin ?

#### Bryan Gin-ge Chen (Aug 12 2020 at 21:34):

What's their github username?

#### A. Stone Olguin (Aug 12 2020 at 21:43):

Hi, my GitHub username is StoneOlguin

#### Bryan Gin-ge Chen (Aug 12 2020 at 21:57):

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

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

#### 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.

#### Alex J. Best (Aug 12 2020 at 22:43):

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

#### Dan Stanescu (Aug 12 2020 at 23:03):

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

#### 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