norm_alternatizeUncurryFin_le — Mathlib

English

The operator norm of the resulting alternating map grows at most by a factor of n+1 relative to f.

Русский

Операторная норма полученной чередующей формы возрастает не более чем в множитель n+1 по отношению к f.

LaTeX

$$$\\| \\text{alternatizeUncurryFin} f \\| \\le (n + 1) \\| f \\|$$$

Lean4

theorem norm_alternatizeUncurryFin_le (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) : ‖alternatizeUncurryFin f‖ ≤ (n + 1) * ‖f‖ :=
  (alternatizeUncurryFinCLM 𝕜 E F).le_of_opNorm_le norm_alternatizeUncurryFinCLM_le f

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