Complement transport for symmetric pair energies

For a symmetric weight W on a finite type, the energy energy W A = (∑ a ∈ A, ∑ b ∈ A, W a b) / 2 of a set and that of its complement differ by a term depending on the row sums of W over A. When all row sums are equal, energy gaps between sets of the same size are invariant under complementation, and minimizers among sets of a given size correspond to minimizers among their complements; with zero diagonal, this property characterizes constant row sums.

Main results

• energy_compl_sub, energy_compl_regular.
• energy_gap_compl, minimizer_compl_iff.
• regular_iff_complement_gaps, regular_iff_complement_minimizers.

References

• N. Bushaw, B. Cody, C. Leffler, Sets of vertices with extremal energy, arXiv:2407.18785, Theorem 3.5.

noncomputable def MusicTheory.ComplementEnergy.energy {α : Type u_1} (W : α → α → ℝ) (A : Finset α) : ℝ

Half the ordered interaction sum. For symmetric W with zero diagonal this is the usual unordered all-pairs energy.

Equations

• MusicTheory.ComplementEnergy.energy W A = (∑ a ∈ A, ∑ b ∈ A, W a b) / 2

noncomputable def MusicTheory.ComplementEnergy.rowSum {α : Type u_1} [Fintype α] (W : α → α → ℝ) (a : α) : ℝ

The total interaction seen from one site.

Equations

• MusicTheory.ComplementEnergy.rowSum W a = ∑ b : α, W a b

def MusicTheory.ComplementEnergy.IsSymmetric {α : Type u_1} (W : α → α → ℝ) : Prop

Equations

• MusicTheory.ComplementEnergy.IsSymmetric W = ∀ (a b : α), W a b = W b a

def MusicTheory.ComplementEnergy.IsRegular {α : Type u_1} [Fintype α] (W : α → α → ℝ) : Prop

Equations

• MusicTheory.ComplementEnergy.IsRegular W = ∀ (a b : α), MusicTheory.ComplementEnergy.rowSum W a = MusicTheory.ComplementEnergy.rowSum W b

def MusicTheory.ComplementEnergy.IsMinimizer {α : Type u_1} (W : α → α → ℝ) (A : Finset α) : Prop

Global minimization among sets of the same cardinality.

Equations

• MusicTheory.ComplementEnergy.IsMinimizer W A = ∀ (B : Finset α), B.card = A.card → MusicTheory.ComplementEnergy.energy W A ≤ MusicTheory.ComplementEnergy.energy W B

theorem MusicTheory.ComplementEnergy.cross_sum_symm {α : Type u_1} (W : α → α → ℝ) (hW : IsSymmetric W) (A B : Finset α) : ∑ a ∈ A, ∑ b ∈ B, W a b = ∑ b ∈ B, ∑ a ∈ A, W b a

theorem MusicTheory.ComplementEnergy.energy_compl_sub {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) (A : Finset α) : energy W Aᶜ - energy W A = energy W Finset.univ - ∑ a ∈ A, rowSum W a

The complement identity before any regularity hypothesis.

theorem MusicTheory.ComplementEnergy.energy_compl_regular {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) (r : ℝ) (hr : ∀ (a : α), rowSum W a = r) (A : Finset α) : energy W Aᶜ - energy W A = energy W Finset.univ - ↑A.card * r

A constant weighted degree makes the complement correction depend only on cardinality.

theorem MusicTheory.ComplementEnergy.regular_has_constant {α : Type u_1} [Fintype α] (W : α → α → ℝ) (hW : IsRegular W) : ∃ (r : ℝ), ∀ (a : α), rowSum W a = r

theorem MusicTheory.ComplementEnergy.energy_gap_compl {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) (hr : IsRegular W) (A B : Finset α) (hcard : A.card = B.card) : energy W Aᶜ - energy W Bᶜ = energy W A - energy W B

Equal-cardinality energy differences survive complementation unchanged.

theorem MusicTheory.ComplementEnergy.energy_le_compl_iff {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) (hr : IsRegular W) (A B : Finset α) (hcard : A.card = B.card) : energy W Aᶜ ≤ energy W Bᶜ ↔ energy W A ≤ energy W B

theorem MusicTheory.ComplementEnergy.minimizer_compl_iff {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) (hr : IsRegular W) (A : Finset α) : IsMinimizer W Aᶜ ↔ IsMinimizer W A

Both directions of the global minimizer correspondence.

theorem MusicTheory.ComplementEnergy.regular_iff_complement_gaps {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) : IsRegular W ↔ ∀ (A B : Finset α), A.card = B.card → energy W Aᶜ - energy W Bᶜ = energy W A - energy W B

Regularity is exactly what makes all equal-cardinality energy gaps complement-invariant.

theorem MusicTheory.ComplementEnergy.energy_singleton {α : Type u_1} (W : α → α → ℝ) (hdiag : ∀ (a : α), W a a = 0) (a : α) : energy W {a} = 0

theorem MusicTheory.ComplementEnergy.singleton_minimizer {α : Type u_1} (W : α → α → ℝ) (hdiag : ∀ (a : α), W a a = 0) (a : α) : IsMinimizer W {a}

theorem MusicTheory.ComplementEnergy.regular_iff_complement_minimizers {α : Type u_1} [Fintype α] [DecidableEq α] (W : α → α → ℝ) (hW : IsSymmetric W) (hdiag : ∀ (a : α), W a a = 0) : IsRegular W ↔ ∀ (A : Finset α), IsMinimizer W A → IsMinimizer W Aᶜ

With zero diagonal, preserving all global minimizers forces constant weighted degree. The converse is witnessed already by complements of singleton sets.