convexBodySumFun_apply — Mathlib

English

For any x in the mixed space, convexBodySumFun x equals the finite sum over places of the place-wise multiplicities times the place-norms of x.

Русский

Для любого x из смешанного пространства convexBodySumFun x равна сумме по местам различной кратности, умноженной на нормы x на соответствующих местах.

LaTeX

$$\$ \\text{convexBodySumFun}(x) = \\sum_{w} \\operatorname{mult}(w) \\cdot \\|x_w\\| \$$$

Lean4

theorem convexBodySumFun_apply (x : mixedSpace K) : convexBodySumFun x = ∑ w, mult w * normAtPlace w x :=
  rfl

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