Prove2Me

Greedy obtains a (1−1/e)(1-1/e) approximation for a monotone submodular objective

Proved
CustAssort.AugGreedy.greedy_approximation

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

approximation-algorithmgreedy-algorithmp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1submodular

Let gg be a monotone, submodular set function on a finite ground set PP, with g(∅)≥0g(\varnothing)\ge0. Greedy begins with the empty set, repeatedly adds an available element giving the largest next value, and stops when it reaches cardinality kk or exhausts PP. For every output Δ\Delta, including every tie-breaking choice, and every feasible comparison set S⊆PS\subseteq P with ∣S∣≤k|S|\le k,

g(Δ)≥(1−1/e) g(S).g(\Delta)\ge(1-1/e)\,g(S).

This is the classical bound cited for the truncated objective in the proof of Theorem 4.2.

Formalization Note The nonnegative empty-set value is needed for the multiplicative form. It holds with equality for the paper's truncated objective.

Preamble
import Mathlib
import Definitions.Def_CustAssort_AugGreedy_Setting
Formal statement
namespace CustAssort.AugGreedy

/-- The Nemhauser et al. (1978) cardinality-constrained greedy bound used on pp. 10 and 12. -/
theorem greedy_approximation {α : Type*} [DecidableEq α] (g : Finset α → ℝ)
    (P : Finset α) (k : ℕ) (Δ : Finset α)
    (hmono : ∀ A B : Finset α, A ⊆ B → B ⊆ P → g A ≤ g B)
    (hsub : SubmodularOn g P) (hzero : 0 ≤ g ∅)
    (hΔ : IsGreedyOutput g P k Δ) :
    ∀ S : Finset α, S ⊆ P → S.card ≤ k →
      (1 - Real.exp (-1)) * g S ≤ g Δ := by sorry

end CustAssort.AugGreedy
Source
El Housni & Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, https://ssrn.com/abstract=3830082 (version of December 7, 2021), §4.1, p. 10; proof of Theorem 4.2, p. 12, citing Nemhauser et al. (1978)
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