coe_energy — Mathlib

English

The energy value can be interpreted consistently in any field 𝕜 with the same underlying rational expression.

Русский

Значение энергии можно единообразно интерпретировать в любом поле 𝕜 с той же рациональной формулой.

LaTeX

$$$ (P.energy\\, G : 𝕜) = ( \\sum_{uv \\in P.parts.offDiag} (G.edgeDensity(u,v) : 𝕜)^2 ) / ( #P.parts : 𝕜)^2 $$$

Lean4

@[simp, norm_cast]
theorem coe_energy {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] :
    (P.energy G : 𝕜) = (∑ uv ∈ P.parts.offDiag, (G.edgeDensity uv.1 uv.2 : 𝕜) ^ 2) / (#P.parts : 𝕜) ^ 2 := by
  rw [energy]; norm_cast

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