Prove2Me

Proof of Theorem I.1 — the telescoped bound f(OPT0)−f(OPTn)≤f(Xn)+f(Yn)f(OPT_0) - f(OPT_n) \le f(X_n) + f(Y_n)

Proved
DoubleGreedyUSM.Deterministic.telescoped

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→R≥0f : 2^{\mathcal N} \to \mathbb R_{\ge 0} a nonnegative submodular function, OPTOPT an optimal solution, 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) with X0=∅X_0 = \emptyset, Y0=NY_0 = \mathcal N, and let OPTi=(OPT∪Xi)∩YiOPT_i = (OPT \cup X_i) \cap Y_i. Then

f(OPT0)−f(OPTn)≤[f(Xn)−f(X0)]+[f(Yn)−f(Y0)]≤f(Xn)+f(Yn).f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n).

This is the sum of Lemma II.2 over 1≤i≤n1 \le i \le n after telescoping, followed by dropping f(X0),f(Y0)≥0f(X_0), f(Y_0) \ge 0. Together with OPT0=OPTOPT_0 = OPT and OPTn=Xn=YnOPT_n = X_n = Y_n it gives f(Xn)≥f(OPT)/3f(X_n) \ge f(OPT)/3.

Formalization Note Both inequalities are stated. The first uses only submodularity; nonnegativity of ff is assumed because the second inequality needs it.

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 telescoped {X : Type} [Fintype X] [DecidableEq X] (f : Finset X → ℝ)
    (hf0 : ∀ S, 0 ≤ f S) (hf : NonmonotoneSubmod.Shared.Submodular f) (O : Finset X)
    (hO : ∀ S, f S ≤ f O) (l : List X) (hl : l.Nodup) (hcov : ∀ x, x ∈ l) :
    f (optI O (state f l 0)) - f (optI O (state f l l.length)) ≤
        (f (state f l l.length).1 - f (state f l 0).1) +
          (f (state f l l.length).2 - f (state f l 0).2) ∧
      (f (state f l l.length).1 - f (state f l 0).1) +
          (f (state f l l.length).2 - f (state f l 0).2) ≤
        f (state f l l.length).1 + f (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, proof of Theorem I.1, second display (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