fderiv is 0 if derivative is 0

Stream: Is there code for X?

[Patrick Lutz]

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]

deriv is by definition an fderiv! docs#deriv

[Heather Macbeth]

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

[Patrick Lutz]

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]

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]

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]

ah, that makes sense. It's easier than writing deriv in terms of fderiv I guess

[Sebastien Gouezel]

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.