Notation for `lineDeriv` in distribution theory

Stream: mathlib4

[Moritz Doll]

As in the case of the Fourier transform (see #31115 and #31114), I think we should embrace notation type-classes more for operators that appear in distribution theory. The refactor for the Fourier transform was rather simple and very obviously necessary, but now I have one which I would like to discuss beforehand since it is not as obvious: lineDeriv (aka partial derivatives). I experimented with the issue of the notation for integrals and partial derivatives colliding, but that is not the case: #31876 (see also this for the class and notation I am proposing).
This has the additional benefit that we usually define operators as CLMs, but then there might be a choice of the scalar multiplication, so this is bad for applied functions as lineDerivCLM R f is equal to lineDerivCLM R' f. Currently (and previously for the FT), we have simp-lemmas that go to the bare functions, but that is bad because we lose the information that these functions are very well-behaved (see docs#SchwartzMap.pderivCLM_apply or #30240 for a PR with a similar problem (fderivLM_apply) for examples).
The easiest thing would be keeping lineDeriv as it is and only use the notation only for distribution theory. Any opinions? (same question comes up for fderiv, but there I could't think of good notation..)
cc @Anatole Dedecker @Luigi Massacci @Jireh Loreaux

[Michael Rothgang]

Interesting idea: this could also become relevant for the weak derivative of classical distributions. :thinking:

[Moritz Doll]

Yes, this is the point, we will have lots of definitions for the derivative

[Michael Rothgang]

And proofs that they coincide for nice functions!

[Anatole Dedecker]

This sounds nice indeed (and I would definitely want the same for fderiv), but I am worried about naming. One could argue, for example, that docs#FourierModule.fourier_add is an overly-ambitious name, since it doesn't cover things like docs#VectorFourier.fourierIntegral_add. Similarly, how would you call the polymorphic analog of fderiv_add if you just call the generic notion "fderiv"?

[Anatole Dedecker]

So indeed I think that it would be like to keep separate the fully unbundled fderiv/lineDeriv/fourierIntegral form the associated operators between good function spaces. Maybe fderivOp/lineDerivOp/fourierOp is enough though!

[Moritz Doll]

Yeah, the naming is not easy. I was thinking of using just the namespace to distinguish _root_.fderiv_add from FDeriv.fderiv_add or something similar.
In the case of the Fourier transform it is convenient that the original definition is fourierIntegral, not fourier or fourierTransform, so this problem didn't come up

[Anatole Dedecker]

The issue with using namespacing as disambiguation is that we cannot put a specific declaration in a more specific namespace if it is about the specific differentiation operator on a specific space. So I would really prefer a disambiguation in the name itself, and the more I think about it the more I like fderivOp.

[Moritz Doll]

I think the only theorem that mentions the classic derivative should be something like fderiv_coe, but for derivatives I would be happy with fderivOp (I would like to stick with fourier for the Fourier transform, because I expect it also to be used for Fourier series and DFT and the FT on locally compact groups).

[Robert Maxton]

I am all for more concise, readable notations!