# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: fderiv is 0 if derivative is 0

#### Patrick Lutz (Jul 15 2020 at 20:57):

If I know the derivative of a function is 0 everywhere is there a succinct way to conclude its `fderiv`

is 0 everywhere? I can do it as follows

```
import analysis.calculus.deriv analysis.calculus.fderiv topology.algebra.module
example (f : ℝ → ℝ) (hf : differentiable ℝ f) (hf' : deriv f = 0) : fderiv ℝ f = 0 :=
begin
ext,
rw (show x_1 = x_1*1, by rw mul_one),
rw (show (fderiv ℝ f x) (x_1*1) = x_1*(fderiv ℝ f x 1), from continuous_linear_map.map_smul x_1 (fderiv ℝ f x) 1),
rw fderiv_deriv,
rw hf',
norm_num,
end
```

But that seems pretty annoying. Is there a one line way to do this? The reason I am interested is that I would like to use `is_const_of_fderiv_eq_zero`

from #analysis.calculus.mean_value which requires that `fderiv \R f = 0`

but I only know that `deriv f = 0`

.

#### Heather Macbeth (Jul 15 2020 at 21:03):

`deriv`

is by definition an `fderiv`

! docs#deriv

#### Heather Macbeth (Jul 15 2020 at 21:05):

Oh, sorry, you know this, and you want to know if there's a lemma shortening your proof.

#### Patrick Lutz (Jul 15 2020 at 21:07):

Yeah, the problem is that `deriv`

is `fderiv`

at 1. So if I know that `deriv f`

is 0 everywhere then I only by definition know that `fderiv f x 1`

is 0 for any `x`

. In one dimension this implies that `fderiv`

is 0 eveywhere, but I was wondering if mathlib has some lemma like this already or if my proof above is necessary

#### Sebastien Gouezel (Jul 15 2020 at 21:08):

```
import analysis.calculus.deriv analysis.calculus.fderiv topology.algebra.module
example (f : ℝ → ℝ) (hf : differentiable ℝ f) (hf' : deriv f = 0) : fderiv ℝ f = 0 :=
by { ext, simp [←deriv_fderiv, hf'] }
```

#### Sebastien Gouezel (Jul 15 2020 at 21:09):

The idea is to rewrite `fderiv`

in terms of `deriv`

, then replace the deriv by `0`

, and let `simp`

do all the cleaning.

#### Patrick Lutz (Jul 15 2020 at 21:10):

ah, that makes sense. It's easier than writing `deriv`

in terms of `fderiv`

I guess

#### Sebastien Gouezel (Jul 15 2020 at 21:12):

There are formulas to go both directions. If you know that `deriv`

is `0`

, it is a better idea to rewrite `fderiv`

in terms of `deriv`

to deduce that it is also `0`

.

Last updated: May 19 2021 at 02:10 UTC