Derivative rules

Stream: new members

[Bjørn Kjos-Hanssen]

How come the basic rules for derivatives in Lean like f'+g'=(f+g)' are always stated at a point, like f'(x)+g'(x)=(f+g)'(x)?

[Eric Wieser]

Can you link to a lemma that demonstrates what you're thinking of?

[Jireh Loreaux]

If I had to guess, docs#deriv_sum?

[Eric Wieser]

I guess docs#deriv_add

[Eric Wieser]

It needs to be applied due to the differentiable_at arguments

[Anatole Dedecker]

I think one of the reasons we don’t also have a non applied version is because the API for deriv is copied from the one of fderiv and, except for basics things like addition, such rules tend to be really hard to write non applied in the context of fderiv

[Anatole Dedecker]

For example the composition rule would be really awkward to write in this way, you’d have to mix pointwise composition of linear maps with composition for the point you’re evaluating fderiv at

[Bjørn Kjos-Hanssen]

OK thanks @Anatole Dedecker. Sounds like a non-applied version for deriv could still be added.