Prove2Me

§II — OPTiOPT_i agrees with Xi,YiX_i, Y_i on u1..uiu_1..u_i and with OPTOPT after; OPT0=OPTOPT_0 = OPT, OPTn=Xn=YnOPT_n = X_n = Y_n

Proved
DoubleGreedyUSM.Deterministic.opt_endpoints

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

approximation-algorithmsgreedy-algorithmsp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1submodular-functions

Let N\mathcal N be a finite ground set, f:2N→Rf : 2^{\mathcal N} \to \mathbb R a set function, OPT⊆NOPT \subseteq \mathcal N an optimal solution (a set maximizing ff), and u1,…,unu_1, \dots, u_n an enumeration of N\mathcal N. Run Algorithm 1 in this order, producing the states (Xi,Yi)(X_i, Y_i), and define

OPTi=(OPT∪Xi)∩Yi,0≤i≤n.OPT_i = (OPT \cup X_i) \cap Y_i, \qquad 0 \le i \le n.

Then:

  1. for every 0≤i≤n0 \le i \le n, the set OPTiOPT_i coincides with XiX_i and with YiY_i on the elements u1,…,uiu_1, \dots, u_i, and coincides with OPTOPT on the elements ui+1,…,unu_{i+1}, \dots, u_n;
  2. OPT0=OPTOPT_0 = OPT;
  3. the output of the algorithm is OPTn=Xn=YnOPT_n = X_n = Y_n.

The sequence OPT0,…,OPTnOPT_0, \dots, OPT_n thus starts at the optimum and ends at the algorithm's output; the proof of Theorem I.1 bounds the loss of value along it.

Formalization Note "Coincides on uju_j" is stated as: uj∈OPTiu_j \in OPT_i if and only if uj∈Xiu_j \in X_i (respectively YiY_i, respectively OPTOPT), for uju_j = l[j] with 0-based index j. Optimality of OPTOPT is kept as a hypothesis because the page introduces OPTOPT as an optimal solution, although the statement holds for every set. No property of ff is needed.

Preamble
import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_NonmonotoneSubmod_Shared_OPT
import Definitions.Def_DoubleGreedyUSM_Deterministic_Algorithm1
Formal statement
namespace DoubleGreedyUSM.Deterministic

theorem opt_endpoints {X : Type} [Fintype X] [DecidableEq X] (f : Finset X → ℝ)
    (O : Finset X) (hO : ∀ S, f S ≤ f O) (l : List X) (hl : l.Nodup) (hcov : ∀ x, x ∈ l) :
    (∀ i (hi : i ≤ l.length),
      (∀ j (hj : j < i),
        (l[j]'(by omega) ∈ optI O (state f l i) ↔ l[j]'(by omega) ∈ (state f l i).1) ∧
        (l[j]'(by omega) ∈ optI O (state f l i) ↔ l[j]'(by omega) ∈ (state f l i).2)) ∧
      (∀ j (hj : j < l.length), i ≤ j →
        (l[j] ∈ optI O (state f l i) ↔ l[j] ∈ O))) ∧
    optI O (state f l 0) = O ∧
    optI O (state f l l.length) = (state f l l.length).1 ∧
    (state f l l.length).1 = (state f l l.length).2 := by sorry

end DoubleGreedyUSM.Deterministic
Source
Buchbinder, Feldman, Naor, Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012 version, §II, paragraph after Lemma II.1 (PDF p. 3)
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