Zulip Chat Archive

Stream: general

Topic: Derivative of Matrix

Shi Zhengyu (Mar 28 2022 at 21:10):

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?

Heather Macbeth (Mar 28 2022 at 21:11):

@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 (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