energy_le_one — Mathlib

English

The energy of any partition with respect to any graph is at most 1.

Русский

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

LaTeX

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

Lean4

theorem energy_le_one : P.energy G ≤ 1 :=
  div_le_of_le_mul₀ (sq_nonneg _) zero_le_one <|
    calc
      ∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2 ≤ #P.parts.offDiag • (1 : ℚ) :=
        sum_le_card_nsmul _ _ 1 fun _ _ => (sq_le_one_iff₀ <| G.edgeDensity_nonneg _ _).2 <| G.edgeDensity_le_one _ _
      _ = #P.parts.offDiag := (Nat.smul_one_eq_cast _)
      _ ≤ _ := by
        rw [offDiag_card, one_mul]
        norm_cast
        rw [sq]
        exact tsub_le_self

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