§5.1, p. 7 — a swap-local optimum $S$ of $\psi$ has $g(S)+\ell(S) \ge (1-e^{-1})g(O)+\ell(O)$ for every base $O$

Proved

CurvatureSubmod.LocalSearch.local_opt_bound

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

local-searchmatroidp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1submodular

Let $X$ be a finite set, $g : 2^X \to \mathbb{R}_{\ge 0}$ monotone increasing and submodular, $\ell(A) = \sum_{j \in A} w(j)$ linear with arbitrary real weights, and $\psi = (1 - e^{-1}) h + \ell$ with $h$ the Filmus–Ward potential of $g$ . Let $\mathcal M$ be a matroid on $X$ and $S$ a base of $\mathcal M$ that is locally optimal for $\psi$ under single-element exchanges: $\psi(S - a + b) \le \psi(S)$ whenever $a \in S$ , $b \notin S$ and $S - a + b$ is a base. Then for every base $O$ of $\mathcal M$ ,

g(S) + \ell(S) \ \ge\ (1 - e^{-1})\, g(O) + \ell(O).

This is the exact ( $\delta = 0$ ) form of the guarantee required by Theorem 3.1, obtained from the local search of §5.

Formalization Note "Locally optimal" is Figure 4's stopping rule with $\delta = 0$ (IsSwapLocalOpt). As in Lemma 5.2, $g$ is monotone and nonnegative.

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_CurvatureSubmod_LocalSearch_Setting

Formal statement

namespace CurvatureSubmod.LocalSearch

/-- §5.1, p. 7 (paragraph after the proof of Lemma 5.2): a swap-local optimum `S` of `ψ`
satisfies `g(S) + ℓ(S) ≥ (1 − e^{−1}) g(O) + ℓ(O)` for every base `O`. -/
theorem local_opt_bound {X : Type} [Fintype X] [DecidableEq X] (g : Finset X → ℝ)
    (hg0 : ∀ A, 0 ≤ g A) (hgmono : MonoInc g) (hgsub : NonmonotoneSubmod.Shared.Submodular g)
    (w : X → ℝ) (M : Matroid X) (S : Finset X) (hS : IsSwapLocalOpt M (psi g w) S)
    (O : Finset X) (hO : M.IsBase (↑O : Set X)) :
    (1 - Real.exp (-1)) * g O + linFun w O ≤ g S + linFun w S := by sorry

end CurvatureSubmod.LocalSearch

Source

Sviridenko, Vondrák, Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature (SODA 2015 version, Oct. 9, 2014), p. 7, §5.1, paragraph after the proof of Lemma 5.2

Human review

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

View graph

§5.1, p. 7 — a swap-local optimum SSS of ψ\psiψ has g(S)+ℓ(S)≥(1−e−1)g(O)+ℓ(O)g(S)+\ell(S) \ge (1-e^{-1})g(O)+\ell(O)g(S)+ℓ(S)≥(1−e−1)g(O)+ℓ(O) for every base OOO

§5.1, p. 7 — a swap-local optimum $S$ of $\psi$ has $g(S)+\ell(S) \ge (1-e^{-1})g(O)+\ell(O)$ for every base $O$