English
Let F, E, G be normed spaces over a nontrivial normed field 𝕜, and let ι be a finite index set. Suppose f is a multilinear alternating map in the sense that, for every x ∈ F and every m : ι → E, we have ‖f(x, m)‖ ≤ C · ‖x‖ · ∏i ‖m(i)‖. Then the induced continuous linear map mkContinuousLinear f C H has operator norm at most C, i.e. ‖mkContinuousLinear f C H‖ ≤ C.
Русский
Пусть F, E, G — нормированные пространства над ненулевым нормированным полем 𝕜, и пусть ι — конечное множество индексов. Пусть f является многолинейным чередующим отображением в смысле, что для любого x ∈ F и любого m : ι → E выполняется ‖f(x, m)‖ ≤ C · ‖x‖ · ∏i ‖m(i)‖. Тогда индуцированное непрерывное линейное отображение mkContinuousLinear f C H удовлетворяет ‖mkContinuousLinear f C H‖ ≤ C.
LaTeX
$$$\\\\|\\\\ mkContinuousLinear f C H \\\\| \\\\le C \\, \\\\text{ whenever } \\\\forall x \\\\in F, \\\\forall m \\\\in (\\\\ι \\\\to E), \\\\| f x m \| \\\\le C \\\\|x\\\\| \\\\prod_i \\\\|m_i\\\\|.$$$
Lean4
theorem mkContinuousLinear_norm_le (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) {C : ℝ} (hC : 0 ≤ C)
(H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C :=
(mkContinuousLinear_norm_le_max f C H).trans_eq (max_eq_left hC)
