Partial derivatives

Stream: Is there code for X?

[Nicolò Cavalleri]

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]

What definition do you have in mind?

[Nicolò Cavalleri]

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]

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

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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

[Nicolò Cavalleri]

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]

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

[Thomas Pluck]

I'd like to reiterate the original question. Have working definitions and results been added to mathlib yet?

[Patrick Massot]

No, nobody needed that.

[Moritz Doll]

I have some code for partial derivatives, but most of the time partial derivatives are not the way to go.

[Thomas Pluck]

Moritz Doll said:

I have some code for partial derivatives, but most of the time partial derivatives are not the way to go.

Ah okay. Why aren't they usually the way to go? I was hoping to prove some things about Sobolev spaces in Lean and the only proofs that I know of involve partial derivatives in the definition of weak derivative.

[Moritz Doll]

cool, one more person that wants to do analysis :smile:

[Patrick Massot]

Thomas, you should know that Moritz and Anatole are currently working on the general theory of distributions so there is probably not much to gain from trying to do Sobolev spaces in a more elementary way.

[Moritz Doll]

the problems I ran into is that doing something like iterated partial derivatives is really annoying because of the way the usual derivative is defined at the moment. Actually I was about to ask questions about that. Is it ok if I hijack this thread for that?

[Moritz Doll]

defining the partial derivative is really easy: it's just

noncomputable def pderiv {d : ℕ} (j : fin d) (f : (fin d → 𝕜) → F) (x : fin d → 𝕜) : F :=
fderiv 𝕜 f x (linear_map.std_basis 𝕜 (λ (i : fin d), 𝕜) j 1)

and for the iterated partial derivative you do the same thing with a map to basis vectors and iterated_fderiv

[Yury G. Kudryashov]

If we want to have partial derivatives, then they should be defined as derivatives of compositions with line maps

[Yury G. Kudryashov]

This way you get the correct differentiability assumptions

[Yury G. Kudryashov]

Sometimes it is important

[Anatole Dedecker]

I agree with Yury, since it’s pretty much the only case where it’s more interesting to talk about partial derivatives than the Fréchet derivative

[Yury G. Kudryashov]

E.g., I have a real life example where we need $\frac{\partial^2 f}{\partial x\partial y}=\frac{\partial^2 f}{\partial y\partial x}$ but the function is not $C^2$

[Heather Macbeth]

Thomas Pluck said:

Ah okay. Why aren't they usually the way to go? I was hoping to prove some things about Sobolev spaces in Lean and the only proofs that I know of involve partial derivatives in the definition of weak derivative.

I usually work with Sobolev spaces on manifolds, so I'd really rather not fix a co-ordinate axis!

[Sebastien Gouezel]

Yury G. Kudryashov said:

E.g., I have a real life example where we need $\frac{\partial^2 f}{\partial x\partial y}=\frac{\partial^2 f}{\partial y\partial x}$ but the function is not $C^2$

Even in the Fréchet-differential language, you don't need C^2 for this, you just need differentiability on a neighborhood of 0, and differentiability of the differential at 0, without any continuity whatsoever. See docs#second_derivative_symmetric

[Sebastien Gouezel]

But of course there are even weaker versions if you are only interested in differentiating along horizontals and verticals.

[Yury G. Kudryashov]

In my case the mixed derivatives are continuous but $\frac{\partial^2 f}{\partial x^2}$ does not exist.

[Thomas Pluck]

Okay, this discussion has made it really clear why partial derivatives are unnecessary, thanks!

[Thomas Pluck]

Patrick Massot said:

Thomas, you should know that Moritz and Anatole are currently working on the general theory of distributions so there is probably not much to gain from trying to do Sobolev spaces in a more elementary way.

If @Moritz Doll and @Anatole Dedecker would like any help with their project, feel free to get in touch.

[Michael Lee]

Count me in as well, would definitely be interested in assisting if @Moritz Doll and @Anatole Dedecker are still working on this.

[Anatole Dedecker]

I am indeed working on this (after a ~1 year pause). At the moment I don't think there are a lot of parallelizable tasks to set up the really basic things, but after the basic things are defined there will be a lot of library to build in a lot of directions, so I'll let you know at that point!

[Moritz Doll]

I am not doing that much Lean stuff at the moment (I have a lot of informal maths to do), but I am still very much interested in this. One roadblock I ran into was that for tempered distributions we need that the weak dual and the strong dual are the same. This relies basically on the Arzela-Ascoli theorem and some juggling of limits and derivatives and a bit of abstract nonsense in functional analysis (I am afraid that 'a bit' might be a gross understatement). If you want to think about this, feel free but this is not really beginner friendly. The goal is to have the textbook characterization of convergence of tempered distributions for the strong dual of Schwartz space.

[Anatole Dedecker]

Are they really the same or is it only true for sequences? I know for general distributions this is only true for sequences, but I don't know about the case of tempered distributions.

[Moritz Doll]

btw I managed to smuggle the definition of partial derivatives into mathlib: docs#SchwartzMap.pderivCLM
It might be not too hard to prove that the distributional derivative of the Heaviside function is the Dirac delta. I imagine the most work is to prove that the Heaviside function is a tempered distribution (but we should have all the integration estimates now).

[Moritz Doll]

Anatole Dedecker said:

Are they really the same or is it only true for sequences? I know for general distributions this is only true for sequences, but I don't know about the case of tempered distributions.

I thought it was true in general, but I might be wrong. I actually only care about sequences, so maybe I should revise my claim.