Theorem I.4 — three-quarter approximation for two-player submodular welfare

Proved

DoubleGreedyUSM.Randomized.two_player_welfare

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

approximation-algorithmsp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1randomized-algorithmssubmodular-functionssubmodular-welfare

Let two players value subsets of a finite ground set by nonnegative, normalized, monotone submodular functions $f_1$ and $f_2$ . An allocation is determined by the first player's set $S$ ; the second receives $\mathcal N\setminus S$ . Put $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$ and run Algorithm 2 on $g$ in any order. Then

3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].

The maximum on the left is exactly the optimum welfare over two-player partitions.

Formalization Note This is Proof (2) of Theorem I.4, which applies Algorithm 2 to $g$ . The statement does not encode its two-oracle-query implementation or running time.

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_NonmonotoneSubmod_Shared_OPT
import Definitions.Def_DoubleGreedyUSM_Randomized_Algorithm2

Formal statement

namespace DoubleGreedyUSM.Randomized

/-- Theorem I.4, Proof (2) (PDF pp. 2, 7): Algorithm 2 on the two-player welfare
objective is a three-quarter approximation. -/
theorem two_player_welfare {X : Type} [Fintype X] [DecidableEq X]
    (f₁ f₂ : Finset X → ℝ)
    (hsub₁ : NonmonotoneSubmod.Shared.Submodular f₁)
    (hsub₂ : NonmonotoneSubmod.Shared.Submodular f₂)
    (hmono₁ : ∀ A B : Finset X, A ⊆ B → f₁ A ≤ f₁ B)
    (hmono₂ : ∀ A B : Finset X, A ⊆ B → f₂ A ≤ f₂ B)
    (hnonneg₁ : ∀ S : Finset X, 0 ≤ f₁ S)
    (hnonneg₂ : ∀ S : Finset X, 0 ≤ f₂ S)
    (hnorm₁ : f₁ ∅ = 0) (hnorm₂ : f₂ ∅ = 0)
    (l : List X) (hl : l.Nodup) (hcov : ∀ x : X, x ∈ l) :
    let g : Finset X → ℝ := fun S => f₁ S + f₂ Sᶜ
    3 * NonmonotoneSubmod.Shared.OPT g ≤
      4 * expect (state g l l.length) (fun s => g s.1) := by sorry

end DoubleGreedyUSM.Randomized

Source

Buchbinder, Feldman, Naor, Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012 version, Theorem I.4 (PDF p. 2), §IV preamble (PDF p. 6), Proof (2) (PDF p. 7)

Human review

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

View graph