Lemma 2.1 — swapping $S_i$ and $S_j$ does not increase $v(X_i)v(X_j)$

import Mathlib

namespace NSWBetter

/-- **Lemma 2.1 (swap lemma).**
Viswanathan, *A Better-than-e^{1/e} Approximation Algorithm for Nash Social Welfare under Additive Valuations*, arXiv:2607.13340 (held version, sha256 08811cb4…), Lemma 2.1, p.9: "Given a fair allocation instance where all agents have the same valuation function v, let X be an allocation and let i, j ∈ N be two agents. Let Si ⊆ Xi and Sj ⊆ Xj be two sets of goods such that v(Sj) ≥ v(Si) and v(Xi \ Si) ≥ v(Xj \ Sj). Let Y be an allocation constructed by starting at X and swapping the sets of goods Si and Sj; that is, Yi = (Xi \ Si) ∪ Sj and Yj = (Xj \ Sj) ∪ Si. Then, v(Yi)v(Yj) ≤ v(Xi)v(Xj). Moreover, equality holds if and only if v(Sj) = v(Si) or v(Xi \ Si) = v(Xj \ Sj)."

**Formalization Note.** Only the two bundles `X_i`, `X_j` of the allocation matter; they are disjoint sets of goods. The common additive valuation is `v : Fin m → ℝ`, `v ≥ 0`. -/
theorem lemma_2_1 {m : ℕ} (v : Fin m → ℝ) (hv : ∀ g, 0 ≤ v g) (Xi Xj Si Sj : Finset (Fin m))
    (hdisj : Disjoint Xi Xj) (hSi : Si ⊆ Xi) (hSj : Sj ⊆ Xj)
    (h1 : ∑ g ∈ Si, v g ≤ ∑ g ∈ Sj, v g) (h2 : ∑ g ∈ Xj \ Sj, v g ≤ ∑ g ∈ Xi \ Si, v g) :
    (∑ g ∈ (Xi \ Si) ∪ Sj, v g) * (∑ g ∈ (Xj \ Sj) ∪ Si, v g) ≤
        (∑ g ∈ Xi, v g) * (∑ g ∈ Xj, v g) ∧
      ((∑ g ∈ (Xi \ Si) ∪ Sj, v g) * (∑ g ∈ (Xj \ Sj) ∪ Si, v g) =
          (∑ g ∈ Xi, v g) * (∑ g ∈ Xj, v g) ↔
        ∑ g ∈ Sj, v g = ∑ g ∈ Si, v g ∨ ∑ g ∈ Xi \ Si, v g = ∑ g ∈ Xj \ Sj, v g) := by sorry

end NSWBetter

• Endorsed by Shuze Chen · Nov 6, 2026

  Confirmed by the moderator at approval.

• Endorsed by iris · Nov 6, 2026

  Confirmed by the mission captain (proposal self-audit).