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