Stream: Is there code for X?
Topic: Partial derivatives
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?
Yury G. Kudryashov (Aug 22 2020 at 16:35):
What definition do you have in mind?
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
Nicolò Cavalleri (Aug 22 2020 at 17:53):
I did not really think if this is indeed a sensible idea
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
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.
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
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?
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