Equivalent definitions of operator norms

Stream: Is there code for X?

[Eric Wieser]

As far as I can tell, we only have the first three of these (respectively the definition, docs#ContinuousLinearMap.sSup_closed_unit_ball_eq_norm and docs#ContinuousLinearMap.sSup_unit_ball_eq_norm), where the list is from wikipedia:

$$\begin{alignat}{10} \|A\|_{op} &= \inf &&\{ c \geq 0 ~&&:~ \| A v \| \leq c \| v \| ~&&~ \text{ for all } ~&&v \in V \} \\ &= \sup &&\{ \| Av \| ~&&:~ \| v \| \leq 1 ~&&~\text{ and } ~&&v \in V \} \\ &= \sup &&\{ \| Av \| ~&&:~ \| v \| < 1 ~&&~\text{ and } ~&&v \in V \} \\ &= \sup &&\{ \| Av \| ~&&:~ \| v \| \in \{0,1\} ~&&~\text{ and } ~&&v \in V \} \\ &= \sup &&\{ \| Av \| ~&&:~ \| v \| = 1 ~&&~\text{ and } ~&&v \in V \} \;\;\;\text{for nontrivial } V\\ &= \sup &&\bigg\{ \frac{\| Av \|}{\| v \|} ~&&:~ v \ne 0 ~&&~\text{ and } ~&&v \in V \bigg\} \;\;\;\text{for nontrivial } V. \\ \end{alignat}$$

I think the junk-value behavior of sSup means we don't even need the nontriviality condition.

Do we have the others somewhere else?

[Sébastien Gouëzel]

Note that (4) and (5) are not true in general: over a field which is not the real or complex numbers, you may have vector spaces in which there is no element of norm 1. (For instance $\mathbb{Q}_p$, in which the usual norm takes the values $p^n$, with a constant multiple of the usual norm by an irrational number).

[Sébastien Gouëzel]

Even (2) is not always true (fortunately, there is a DenselyNormedField assumption to make sure it holds, but this wouldn't suffice for (4) or (5)).

[Eric Wieser]

I think a reasonable statement of 4 is:

theorem sSup_unit_sphere_eq_nnnorm {𝕜 𝕜₂ E F : Type*} [SeminormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace ℝ E] [NormedSpace 𝕜 E] [NormedAlgebra ℝ 𝕜] [IsScalarTower ℝ 𝕜 E]
    [NormedSpace ℝ F] [NormedSpace 𝕜₂ F] [NormedAlgebra ℝ 𝕜₂] [IsScalarTower ℝ 𝕜₂ F]
    [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖₊) '' (sphere 0 1 ∪ norm ⁻¹' {0})) = ‖f‖₊ := by

[Jireh Loreaux]

@Eric Wieser note that we already have half of (5) in docs#ContinuousLinearMap.op_norm_le_of_unit_norm

[Jireh Loreaux]

Note also, that for continuous linear maps on a Hilbert space (to itself), there are yet other characterizations of the norm in terms of the inner product. I think I might have a branch with those lying around.