Derivative of Matrix

Stream: general

[Shi Zhengyu]

Hi all,
My apologies first because I feel like I am spamming quite a bit of questions in this day ...
I am trying to find the Fréchet derivative of a linear map A: ℝ -> (matrix (fin n) (fin n) ℝ).
How should I define the norm of vector space of matrices of size n*n, such that I can prove the Fréchet derivative D(A)(t0)(1) for any t0: ℝ corresponds to the matrix formed by entrywise derivative dA[i][j] / dt?
Thanks!

[Heather Macbeth]

@Shi Zhengyu In this case, you don't need the Fréchet derivative (docs#has_fderiv_at), since the domain is 1-dimensional. You can just use docs#has_deriv_at.

[Heather Macbeth]

But, indeed, you do need a norm on matrices. It's not provided by default (because there are many norms you could choose), but for your purposes any sensible norm will probably work, and you can bring it in by writing

local attribute [instance] matrix.normed_group matrix.normed_space

[Heather Macbeth]

The lemma you want can be built from two applications of docs#has_deriv_at_pi

[Eric Wieser]

Is there any way we can start teaching mathlib matrix derivative results without having to repeat ourselves for each choice of norm?

[Eric Wieser]

When I looked at this before, it wasn't clear to me whether docs#derivation was all that useful for non-commutative rings; otherwise maybe it could help generalize

[Shi Zhengyu]

Thanks! I'll check that out :D