English
For empty index sets, the NN-norm of the constant map built from x in G equals the NN-norm of x, mirroring the corresponding norm equality.
Русский
Для пустого множества индексов NN-норма константного отображения, заданного x ∈ G, равна NN-норме x.
LaTeX
$$$\|\mathrm{constOfIsEmpty}_{\mathbb{K}}(E,x)\|_{\mathrm{nn}} = \|x\|_{\mathrm{nn}}$$$
Lean4
@[simp]
theorem nnnorm_smulRight (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) : ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊ :=
by
refine le_antisymm ?_ ?_
· refine opNNNorm_le_iff.2 fun m => (nnnorm_smul_le _ _).trans ?_
rw [mul_right_comm]
gcongr
exact le_opNNNorm _ _
· obtain hz | hz := eq_zero_or_pos ‖z‖₊
· simp [hz]
rw [← le_div_iff₀ hz, opNNNorm_le_iff]
intro m
rw [div_mul_eq_mul_div, le_div_iff₀ hz]
refine le_trans ?_ ((f.smulRight z).le_opNNNorm m)
rw [smulRight_apply, nnnorm_smul]
