Splitting `analysis.special_functions.exp_log`

Stream: maths

[Yury G. Kudryashov]

I'm going to split this files in two:

• a file that knows nothing about derivatives;
• a file that states differentiability of exp and log.
  How should I name these two files?

[Sebastien Gouezel]

exp_log and exp_log_deriv?

[Yury G. Kudryashov]

#9882 (WIP)

[Rémy Degenne]

For your information, I've already done this split and the similar one for all other functions in the special_functions folder in branch#pow_split while trying to get the definition of rpow derivative-free. I had absolutely no time for mathlib in the last two weeks so the branch has gone a bit stale and I've not PRed it but I should be able to do it next week.
That branch also has mean inequalites and Lp spaces that don't import derivatives.

Feel free to go on with that PR if you need it now, but if if you plan on doing a more general refactor of the special_functions folder, you could have a look at that branch.

[Rémy Degenne]

I see that your PR splits the file into 4 files, which I prefer over my split into 2. So definitely go ahead with that PR, but I'd appreciate if you could give me some time to PR my stuff before doing other big changes to the organization of the folder :)

[Yury G. Kudryashov]

I don't need other splits (at least in the next few weeks).

[Yury G. Kudryashov]

My goal was to have continuous complex.exp in analysis.complex.circle.