Theorem 2.1 — (Nemhauser et al.) v is non-decreasing submodular iff v(T) ≤ v(S) + Σ_{g∈T∖S} v(g | S)

Proved

RoundRobinEq.SubmodularEF1.theorem_2_1

by mikedeng1 · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1set-functionssubmodular

Let $M$ be a finite set of goods and $v:2^M\to\mathbb R_{\ge0}$ a non-negative set function, with marginal values $v(g\mid S)=v(S\cup\{g\})-v(S)$ . Then $v$ is non-decreasing and submodular if and only if

v(T)\ \le\ v(S)+\sum_{g\in T\setminus S} v(g\mid S)\qquad\text{for all } S,T\subseteq M .

This characterization of monotone submodular functions, due to Nemhauser, Wolsey and Fisher, is the first step of the closing bound in the proof of Theorem 4.4, where it bounds the value of a bundle by the value of agent $i$ 's deviation bundle plus a sum of marginal values.

Formalization Note $v$ is a real-valued function on Finset M with the hypothesis $v(S)\ge0$ for all $S$ (the paper's codomain $\mathbb R_{\ge0}$ ); normalization $v(\emptyset)=0$ is not assumed, as in the paper's statement. "Submodular" is the marginal form of p. 5 (IsSubmodular).

Preamble

import Mathlib
import Definitions.Def_RoundRobinEq_SubmodularEF1_Setting

Formal statement

namespace RoundRobinEq.SubmodularEF1

/-- Theorem 2.1 (Nemhauser et al.), p. 5: a function `v : 2^M → ℝ≥0` is non-decreasing and
submodular iff `v(T) ≤ v(S) + ∑_{g ∈ T \ S} v(g | S)` for all `S, T ⊆ M`. -/
theorem theorem_2_1 {M : Type} [Fintype M] [DecidableEq M] (v : Finset M → ℝ)
    (hv : ∀ S, 0 ≤ v S) :
    (IsNonDecreasing v ∧ IsSubmodular v) ↔
      ∀ S T : Finset M, v T ≤ v S + ∑ g ∈ T \ S, marginal v {g} S := by sorry

end RoundRobinEq.SubmodularEF1

Source

Amanatidis et al., Round-Robin Beyond Additive Agents, arXiv:2301.13652v1, p. 5, Theorem 2.1

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph