convexBodySumFun_nonneg

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.convexBodySumFun_nonneg

← MathLib Explorer

English

For every x in the mixed space, convexBodySumFun x is nonnegative.

Русский

Для каждого x из смешанного пространства convexBodySumFun x неотрицательно.

LaTeX

$$0 \\le convexBodySumFun(x)$$

Lean4

theorem convexBodySumFun_nonneg (x : mixedSpace K) : 0 ≤ convexBodySumFun x :=
  Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru