convexBodySum — Mathlib

English

An element x from the base field K lies in convexBodySum K B exactly when the finite sum of weighted place-norms is bounded by B.

Русский

Элемент x поля K принадлежит convexBodySum K B тогда и только тогда, когда конечная взвешенная сумма норм на местах не превышает B.

LaTeX

$$x ∈ convexBodySum K B \\Longleftrightarrow \\sum_{w} (mult w) · w.val x ≤ B$$

Lean4

/-- The convex body equal to the set of points `x : mixedSpace K` such that
  `∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B`. -/
abbrev convexBodySum : Set (mixedSpace K) :=
  {x | convexBodySumFun x ≤ B}

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