feat: derivatives of matrix operations

[eric-wieser]

These are finally possible to state after #19108.

However, a lot of bundled ContinuousLinearMaps are missing.

---

• depends on: [Merged by Bors] - refactor: allow deriv to be used on topological vector spaces #19108

[github-actions]

PR summary 71948cdd47

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.Calculus.FDeriv.Matrix (new file)	1829
Mathlib.Analysis.Calculus.Deriv.Matrix (new file)	1832

---

Declarations diff

+ Differentiable.matrix_trace
+ Differentiable.matrix_transpose
+ DifferentiableAt.matrix_trace
+ DifferentiableAt.matrix_transpose
+ DifferentiableOn.matrix_trace
+ DifferentiableOn.matrix_transpose
+ DifferentiableWithinAt.matrix_trace
+ DifferentiableWithinAt.matrix_transpose
+ HasDerivAt.conjTranspose
+ HasDerivAt.matrix_hadamard
+ HasDerivAt.matrix_inv
+ HasDerivAt.matrix_kronecker
+ HasDerivAt.matrix_mul
+ HasDerivAt.trace
+ HasDerivAt.transpose
+ HasFDerivAt.matrix_conjTranspose
+ HasFDerivAt.matrix_mul
+ HasFDerivAt.matrix_trace
+ HasFDerivAt.matrix_transpose
+ HasFDerivAtFilter.matrix_conjTranspose
+ HasFDerivAtFilter.matrix_trace
+ HasFDerivAtFilter.matrix_transpose
+ HasFDerivWithinAt.matrix_trace
+ HasFDerivWithinAt.matrix_transpose
+ deriv_matrix
+ differentiableAt_matrix
+ differentiableOn_matrix
+ differentiableWithinAt_matrix
+ differentiable_matrix
+ hasDerivAt_matrix
+ hasFDerivAtFilter_matrix
+ hasFDerivAt_matrix
+ hasFDerivWithinAt_matrix

You can run this locally as follows

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

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

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

---

Increase in tech debt: (relative, absolute) = (5.04, 0.00)

Current number	Change	Type
4843	2	porting notes
1520	6	erw

Current commit 71948cdd47
Reference commit d4736a1fb2

You can run this locally as

./scripts/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).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor: allow deriv to be used on topological vector spaces #19108
  By Dependent Issues (🤖). Happy coding!