norms on matrices

Stream: maths

[Yury G. Kudryashov]

Semi-offtopic: possibly, we should introduce a "canonical" norm on matrices and turn all other norms into docs#Seminorm

[Kevin Buzzard]

I guess we have a "canonical" norm on Pi types, and matrices are just Pi types of Pi types. But I rather foolishly hadn't thought about the definition of a derivative; where I see little-o and big-O is in things like the growth of analytic functions and these are typically $\R$-valued.

[Eric Wieser]

Kevin Buzzard said:

and matrices are just Pi types of Pi types

Typeclass search can't see this, that's an implementation detail! At any rate, we already have four or so non-canonical norms on matrices, so that's not the challenge

[Eric Wieser]

@loogle NormedSpace _ (Matrix _ _ _)

[loogle]

:search: Matrix.frobeniusNormedSpace, Matrix.linftyOpNormedSpace, and 2 more

[Yury G. Kudryashov]

I think that turning most of them into Seminorms will make it easier to mix them in a single statement (e.g., about estimates on one of them in terms of another one).

[Eric Wieser]

What's the spelling of NormedAlgebra in the seminorm setting?

[Yury G. Kudryashov]

The new condition is norm_mul_le, right?

[Yury G. Kudryashov]

Should we introduce AlgSeminorm?

[Notification Bot]

7 messages were moved here from #maths > generalizing deriv to TVS by Yury G. Kudryashov.

[Jireh Loreaux]

If you make an AlgSeminorm, please make sure it doesn't require an Algebra instance.

[Sébastien Gouëzel]

I'm not sure it makes sense to do this kind of refactor: we can use type synonyms to compare norms when needed, and there are so many things available when you have a norm that having another bundled way to say the same things will quickly get overwhelming.

[Eric Wieser]

Maybe it does make sense to declare the sup operator norm as canonical though

[Yury G. Kudryashov]

Introducing type synonyms is another option. It's better than the current letI/local attribute [instance] approach.

[Eric Wieser]

Type synonyms would require us to axiomatize matrix (and matrix-vector) multiplication

[Eric Wieser]

(or duplicate lemmas like docs#Matrix.mul_one for each synonym)

[Yury G. Kudryashov]

What about casting to matrix whenever we want to multiply? I don't know how often do we speak about matrix multiplication with a norm.

[Antoine Chambert-Loir]

How would you state that the operator norm is submultiplicative, aas well as the formula for the spectral radius?