energy_nonneg

Mathlib.Combinatorics.SimpleGraph.Regularity.Energy

URI: https://scilib.ai/kg/mathlib#Finpartition.energy_nonneg

English

The energy of any partition with respect to any graph is always nonnegative.

Русский

Энергия любого разбиения по отношению к графу всегда неотрицательна.

LaTeX

$$$0 \\le E(P,G)$$$

Lean4

theorem energy_nonneg : 0 ≤ P.energy G := by exact div_nonneg (Finset.sum_nonneg fun _ _ => sq_nonneg _) <| sq_nonneg _

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

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

Разделы

Аффилиация

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