English
On the space of continuous (semi)linear maps, there is a natural seminorm called the operator seminorm, defined by the worst-case ratio of output to input norms.
Русский
На множестве непрерывных линейных отображений существует естественная семинормa, называемая операторной семинормой, заданная максимальным отношением нормы вывода к норме входа.
LaTeX
$$$ \|f\|_{\mathrm{op}} = \sup_{x \neq 0} \frac{\|f x\|}{\|x\|} = \sup_{\|x\|=1} \|f x\| $$$
Lean4
/-- Operator seminorm on the space of continuous (semi)linear maps, as `Seminorm`.
We use this seminorm to define a `SeminormedGroup` structure on `E →SL[σ] F`,
but we have to override the projection `UniformSpace`
so that it is definitionally equal to the one coming from the topologies on `E` and `F`. -/
protected noncomputable def seminorm : Seminorm 𝕜₂ (E →SL[σ₁₂] F) :=
.ofSMulLE norm opNorm_zero opNorm_add_le opNorm_smul_le
