feat(Distribution): make parameters implicit in favor of type ascription

[ADedecker]

Expanding on a suggestion by @faenuccio in an earlier PR, I make the regularity parameters of TestFunction.fderivCLM (and similar constructions) implicit.

This is a bit controversial, because it is essentially forcing type ascription in a lot of contexts. The rationale is that
"the differentiation operator from 𝓓^{n} to 𝓓^{k}" matches mathematical practice, and is easier to parse than "the differentiation operator with parameters n and k".

To make this even more convenient, I introduce notations like 𝓓^{n} to be used when the spaces can be inferred but the regularity cannot.

---

[github-actions]

PR summary 18a09f9093

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

@ADedecker I'm not too convinced. This looks worse to me. Moreover, it's not even like if it were fully applied, then it would be determined. The only way Lean will be able to figure this out is if it knows the expected type. That seems quite unfortunate.

[faenuccio]

@ADedecker I'm not too convinced. This looks worse to me. Moreover, it's not even like if it were fully applied, then it would be determined. The only way Lean will be able to figure this out is if it knows the expected type. That seems quite unfortunate.

Well, if it were fully applied at least the regularity conditions in the domain would be fully determined. I believe a good judgment can only be given a posteriori, because if in most use-cases the type of the output can be inferred, I would prefer this lighter notation at the small cost of adding a (k := k) from time to time. On the other hand, I wonder what happens if we try to define a coercion from n-times differentiable functions to (n-j)-times differentiable ones which AFAICT is not there but might land later on.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.