Zulip Chat Archive

Stream: Is there code for X?

Topic: Partial derivatives


view this post on Zulip Nicolò Cavalleri (Aug 22 2020 at 08:20):

What is the current state in mathlib of partial derivatives? Is anybody working on them / has suggestions on how to implement them?

view this post on Zulip Yury G. Kudryashov (Aug 22 2020 at 16:35):

What definition do you have in mind?

view this post on Zulip Nicolò Cavalleri (Aug 22 2020 at 17:52):

Well I'd want something that works on the charts of a manifold so my ideal definition would be for field valued function on a generic normed vector space and to define it as the total derivative in one variable of the function precomposed with a projection on a vector of a standard basis (a priori not necessarily orthonormal I'd say) but I'm open to any suggestion/generalization as I have no idea really

view this post on Zulip Nicolò Cavalleri (Aug 22 2020 at 17:53):

I did not really think if this is indeed a sensible idea

view this post on Zulip Yury G. Kudryashov (Aug 22 2020 at 19:36):

You can start with def vec_deriv f x v := deriv (λ t, f (x + t • v)) 0. Now that vec_deriv f x v = deriv f x v whenever f is differentiable at x.

view this post on Zulip Yury G. Kudryashov (Aug 22 2020 at 19:38):

If you do not care about partial derivatives of functions that are not differentiable, then deriv f x should work.

view this post on Zulip Yury G. Kudryashov (Aug 22 2020 at 19:39):

You can write this linear map in some basis but this is about linear algebra, not calculus

view this post on Zulip Nicolò Cavalleri (Aug 23 2020 at 09:47):

Ok I would also need to talk about derivatives of function defined on, say, a subset of the field only (I mean its coercion to subtype). I do not understand how to do this in mathlib as deriv_within assumes all the same the function to be defined on the whole field. Do you know how to do this?

view this post on Zulip Yury G. Kudryashov (Aug 23 2020 at 19:18):

The library is designed with total functions in mind. Can you just extend your function using garbage values outside of a set?


Last updated: May 17 2021 at 15:13 UTC