norm_restr — Mathlib

English

If a multilinear map f is built via a constructor with a nonnegative bound C, then the operator norm of the constructed map f.mkContinuous is bounded by C. This is a standard bound for the construction of continuous multilinear maps.

Русский

Если отображение f строится конструктором с неотрицательной границей C, то норма оператора сконструированного отображения f.mkContinuous не превосходит C.

LaTeX

$$$\|f.mkContinuous\| \le C \quad\text{when } C \ge 0$$$

Lean4

theorem norm_restr {k n : ℕ} (f : G [×n]→L[𝕜] G') (s : Finset (Fin n)) (hk : #s = k) (z : G) :
    ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k) :=
  by
  apply MultilinearMap.mkContinuous_norm_le
  exact mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)

Похожие утверждения