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: Dec 20 2023 at 11:08 UTC