convexBodySumFun — Mathlib

English

The function convexBodySumFun is defined by mapping each x in the mixed space to the infinite sum over places of the place-multiplicity times the place-norm of x.

Русский

Функция convexBodySumFun задаётся отображением каждого элемента x из смешанного пространства в бесконечную сумму по местам: сумма по местам — множитель mult w, умноженный на норму x на месте w.

LaTeX

$$\$\\text{convexBodySumFun}(x) = \\sum_w (\\operatorname{mult} w) \\cdot \\|x\\|_w\$$$

Lean4

/-- The function that sends `x : mixedSpace K` to `∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖`. It defines a
norm and it used to define `convexBodySum`. -/
noncomputable abbrev convexBodySumFun (x : mixedSpace K) : ℝ :=
  ∑ w, mult w * normAtPlace w x

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