norm_map_removeNth_le — Mathlib

English

For a multilinear map f and inputs m, the norm of f(m_i) applied to the rest of the coordinates is bounded by the operator norm of f times the product of norms of all coordinates.

Русский

Для отображения f и наборa координат m нормa функции при удалении i-го элемента координат ограничена и равна произведению норм ‖f‖ и произведения ‖m_j‖ остальных индексов.

LaTeX

$$$\|f(m_i)(i.removeNth m)\| \leq \|f\| \cdot \prod_j \|m_j\|$$$

Lean4

theorem norm_map_removeNth_le {i : Fin (n + 1)}
    (f : Ei i →L[𝕜] ContinuousMultilinearMap 𝕜 (fun j ↦ Ei (i.succAbove j)) G) (m : ∀ i, Ei i) :
    ‖f (m i) (i.removeNth m)‖ ≤ ‖f‖ * ∏ j, ‖m j‖ :=
  by
  rw [i.prod_univ_succAbove, ← mul_assoc]
  exact (f (m i)).le_of_opNorm_le (f.le_opNorm _) _

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