matrix norms

Stream: maths

[Eric Wieser]

In this thread, @Heather Macbeth suggests defining a matrix norm $\|A\| = \operatorname{sup}_i (\sum_j \|A_{ij}\|)$, (or in lean, ∥A∥₊ = (finset.univ : finset m).sup (λ i : m, ∑ j : n, ∥A i j∥₊)) which she referred to as either the "L1-L∞-norm" or the "L1-to-L∞ norm".

At a glance, I would have called this the L∞-L1-norm, since the infinity norm is on the outside. I wasn't able to find much about this norm online - does it have a canonical name?

[Eric Wieser]

(the context is choosing what to name things in #13518)

[Reid Barton]

I assume it's the norm of $A$ as a linear map if you give the input the $L^1$ norm and the output the $L^\infty$ norm. The formula is somehow not the definition.

[Eric Wieser]

If it helps confirm whether that's true, the norm satisfies ∥A.mul_vec v∥₊ ≤ ∥A∥₊ * ∥v∥₊where the left and right norm are both the $L^\infty$ norm (and the center norm is the one in question)

[Eric Wieser]

This seems to refer to the same norm: https://mathworld.wolfram.com/MaximumAbsoluteRowSumNorm.html, which it writes as $\|A\|_\infty$

[Jireh Loreaux]

Certainly in applied math textbooks (what little experience I have with them), I have seen notation like $\Vert A \Vert_{\infty}$ used to refer to row norms.

@Eric Wieser , is this norm the minimal constant satisfying this inequality for all v?

[Jireh Loreaux]

It is, see Wikipedia, so this is the $L^{\infty}-L^{\infty}$ operator norm.

[Eric Wieser]

Reid Barton said:

I assume it's the norm of $A$ as a linear map if you give the input the $L^1$ norm and the output the $L^\infty$ norm. The formula is somehow not the definition.

Actually proving something like this (I think ∥A∥₊ = Inf {c | ∀ x, ∥A.mul_vec x∥₊ ≤ c * ∥x∥₊}?) seems slightly painful, as the usual proof only works for matrices over a $\R$-algebra.

[Jireh Loreaux]

I think it might still make sense to call it something like linfty_op_norm, but I can be overruled.

[Eric Wieser]

That feels awfully verbose, I'd be tempted to just use infty_norm

[Jireh Loreaux]

wouldn't that be more natural to refer to the entrywise sup norm?

[Eric Wieser]

Although I guess that's ambiguous with the existing elementwise $L^\infty$ norm

[Eric Wieser]

Yeah, I guess linfty_op is only two characters longer than the current l1_linf

[Eric Wieser]

Alright, we now have three norms available on matrices, currently living in analysis/matrix:

• docs#matrix.normed_group
• docs#matrix.linfty_op_normed_group (once doc-gen rebuilds)
• docs#matrix.frobenius_normed_group

Should we rename the first one? Should we split these into separate files?