Topic: Derivative of Matrix
Shi Zhengyu (Mar 28 2022 at 21:10):
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?
Heather Macbeth (Mar 28 2022 at 21:11):
Heather Macbeth (Mar 28 2022 at 21:12):
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 (Mar 28 2022 at 21:14):
The lemma you want can be built from two applications of docs#has_deriv_at_pi
Eric Wieser (Mar 28 2022 at 23:01):
Is there any way we can start teaching mathlib matrix derivative results without having to repeat ourselves for each choice of norm?
Eric Wieser (Mar 28 2022 at 23:03):
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 (Mar 29 2022 at 00:08):
Thanks! I'll check that out :D
Last updated: Aug 03 2023 at 10:10 UTC