# Zulip Chat Archive

## 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 `x`

.

#### 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