Zulip Chat Archive

Stream: Is there code for X?

Topic: fderiv is 0 if derivative is 0


view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Jul 15 2020 at 21:03):

deriv is by definition an fderiv! docs#deriv

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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'] }

view this post on Zulip 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.

view this post on Zulip Patrick Lutz (Jul 15 2020 at 21:10):

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

view this post on Zulip 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