Operator norm for `(Fin n → ℝ) →L[ℝ] (Fin n → ℝ)`

Stream: Is there code for X?

[ohhaimark]

My questions:

• Is the norm for maps like f : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) the operator norm
• Is there a version LinearMap.transpose (say LinearMap.transpose') that operates like ·.toMatrix'.transpose.toLin'. In other words one that uses a non-canonical equiv from (Fin n → ℝ) ≃ₗ Module.Dual (Fin n → ℝ) using the obvious basis
• Is there a formalization of: the operator norm is the max eigenvalue of f.transpose' ∘L f, or a version free of a choice of basis to avoid the above
• Is there an easier way to calculate the operator norms that I am missing (XY problem)
• Is this an XY problem in general (see https://github.com/badly-drawn-wizards/noperthedron for what I am doing)

[ohhaimark]

Just realize it is far easier to just calculate the operator norm directly, though I am still interested in the answers to these questions.

[Sébastien Gouëzel]

Yes, the norm is the operator norm. Beware that the norm on Fin n → ℝ is the L^\infty norm, not the L^2 norm, which means that your second question is very highly non-canonical (and as far as I can tell we don't have that in mathlib) and I'm not even sure that your third question is true (while it would be true, up to a square root, for the L^2 norm). In general, the simplest way to calculate an operator norm is to come back to the definition, i.e., use docs#NormedAddGroupHom.opNorm_le_bound.

[ohhaimark]

Ah. There is ContinuousLinearMap.norm_adjoint_comp_self.

[ohhaimark]

Not what I specified, but useful.