Zulip Chat Archive

Stream: maths

Topic: How to calculate derivatives


Moritz Doll (Jul 01 2022 at 18:23):

Say you have a function λ x, f x * g x / c and the derivatives of f and g and you want to prove that it has derivative λ x, h x + h' x, what is the most efficient way to do that? My idea would be to first show has_deriv_at (λ x, f x * g x / c) (..) x0, where (..) is the expression coming from using has_deriv_at.div_const and has_deriv_at.mul and then use uniqueness of the derivative to convert the rest to (annoying) algebraic calculations. This sounds extremely tedious and not elegant to me, so is there a better way?

Heather Macbeth (Jul 01 2022 at 18:27):

Maybe something like

convert (hf.mul hg).div_const,
[...algebraic calculations...]

Heather Macbeth (Jul 01 2022 at 18:28):

I don't think that uses the uniqueness of the derivative?

Moritz Doll (Jul 01 2022 at 18:44):

thanks, you are of course right, that this does not need the uniqueness

Violeta Hernández (Jul 02 2022 at 00:32):

Yeah, it's quite odd that the Taylor polynomial isn't a polynomial

Eric Wieser (Jul 02 2022 at 10:16):

Wrong thread?


Last updated: Dec 20 2023 at 11:08 UTC