p-norms on Matrices

Stream: maths

[Hououin Kyouma]

image.png
Are there any pre-defined matrix norms in mathlib4 as defined in the figure? Or how should I define it?

[Eric Wieser]

We have this only for $p=\infty$ at the moment

[Eric Wieser]

The easiest path would be to generalize docs#Matrix.toEuclideanLin away from $p=2$ (which is trivial, you could call it Matrix.toLpLin), and then use the operator norm which is already in mathlib

[Eric Wieser]

docs#ContinuousLinearMap.sSup_sphere_eq_norm is then the theorem (skipping the middle part) for your equation

[Hououin Kyouma]

Eric Wieser said:

docs#ContinuousLinearMap.sSup_sphere_eq_norm is then the theorem (skipping the middle part) for your equation

[image.png](/user_uploads/3121/yu3gcTkHf5ph4LJyzqRieNaL/image.png)

[Hououin Kyouma]

I cannot find this theorem on mathlib, but I have found sSup_sphere_eq_norm. Should I use this theorem?

[Eric Wieser]

I don't know what you mean by "this" (the image in that message is misformatted).

[Hououin Kyouma]

theorem sSup_sphere_eq_norm [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) :

sSup ((fun x => ‖f x‖) '' Metric.sphere 0 1) = ‖f‖ := by

simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_sphere_eq_nnnorm

[Hououin Kyouma]

Eric Wieser said:

I don't know what you mean by "this" (the image in that message is misformatted).

I have posted this theorem in the topic.

[Eric Wieser]

I meant which is the one you said you couldn't find? (The first "this", not the second, sorry)

[Eric Wieser]

The one you pasted there is the one I pointed you to above

[Hououin Kyouma]

Eric Wieser said:

I meant which is the one you said you couldn't find? (The first "this", not the second, sorry)

The second theorem. And you have already told me that this is the theorem I need. Thanks a lot, I'll try again.

[Bhavik Mehta]

Eric Wieser said:

We have this only for $p=\infty$ at the moment

We have this for $p=2$ as well, see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/CStarAlgebra/Matrix.html#Matrix.instL2OpNormedRing