Proof of Theorem 2.6 — $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$

Proved

NonmonotoneSubmod.Nonadaptive.expect_union_upper

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1probabilitysubmodular-functions

Let $X$ be a nonempty finite ground set with $n = |X|$ elements, let $f : 2^X \to \mathbb{R}_{\ge 0}$ be nonnegative and submodular with optimum $OPT = \max_{S\subseteq X} f(S)$ , let $R = X(1/2)$ be a uniformly random subset of $X$ , and let $\omega$ be as in Definition 2.4. Let $B \subseteq X$ be a set with

\omega(x) \le \frac{OPT}{n^2} \quad \text{for every } x \in B .

Then for every $C \subseteq X$ ,

\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + \frac{OPT}{2n}.

Adding to the random set the elements of $B$ , whose averaged marginal values are at most $OPT/n^2$ , can increase the expected value by at most $OPT/(2n)$ . In the proof of Theorem 2.6 this lets the analysis replace $\mathbf{E}[f(R)]$ by $\mathbf{E}[f(R \cup (B \cap C))]$ at a cost of $OPT/(2n)$ .

Formalization Note Both expectations are exact uniform averages over the $2^n$ subsets of $X$ . The ground set is assumed nonempty so that $n \ge 1$ and $OPT/n^2$ , $OPT/(2n)$ are not the Lean junk value of division by zero. Nonnegativity of $f$ (the paper's standing assumption) gives $OPT \ge 0$ , used in the last step $|B \cap C| \cdot OPT/(2n^2) \le OPT/(2n)$ .

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_NonmonotoneSubmod_Shared_OPT
import Definitions.Def_NonmonotoneSubmod_Shared_F
import Definitions.Def_NonmonotoneSubmod_Nonadaptive_omega

Formal statement

namespace NonmonotoneSubmod.Nonadaptive

/-- Proof of Theorem 2.6 (Feige–Mirrokni–Vondrák 2011, p. 1139, third and fourth displays).
Let `f` be nonnegative and submodular on a nonempty ground set of `n` elements, `R = X(1/2)`.
If `ω(x) ≤ OPT/n²` for every `x ∈ B`, then for every `C ⊆ X`,
`E[f(R ∪ (B ∩ C))] ≤ E[f(R)] + OPT/(2n)`. -/
theorem expect_union_upper {X : Type} [Fintype X] [DecidableEq X] [Nonempty X]
    (f : Finset X → ℝ) (hf0 : ∀ S, 0 ≤ f S) (hf : NonmonotoneSubmod.Shared.Submodular f) (B C : Finset X)
    (hB : ∀ x ∈ B, omega f x ≤ NonmonotoneSubmod.Shared.OPT f / (Fintype.card X : ℝ) ^ 2) :
    NonmonotoneSubmod.Shared.F (fun S => f (S ∪ (B ∩ C))) (fun _ => 1 / 2) ≤
      NonmonotoneSubmod.Shared.F f (fun _ => 1 / 2) + NonmonotoneSubmod.Shared.OPT f / (2 * (Fintype.card X : ℝ)) := by sorry

end NonmonotoneSubmod.Nonadaptive

Source

Feige, Mirrokni, Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, p. 1139, §2, proof of Theorem 2.6, third and fourth displays (and the sentence before them)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

This theorem uses:

a finite, nonempty type $X$ with decidable equality, with $n = |X| \ge 1$ (as a real number);
a set function $f : 2^X \to \mathbb{R}$ with $f(S) \ge 0$ for all $S$ , which also satisfies the external predicate NonmonotoneSubmod.Shared.Submodular (body not shown);
two arbitrary subsets $B, C \subseteq X$ .

The statement uses three external objects whose bodies are not shown:

$\mathrm{OPT}(f)$ (NonmonotoneSubmod.Shared.OPT f): a real number determined by $f$ . Its name suggests the maximum of $f$ , but the code does not show this.
$F(h, \tfrac12)$ (NonmonotoneSubmod.Shared.F): a real number determined by a set function $h$ and the constant function $\tfrac12$ on $X$ .
$\omega_f(x)$ (omega f x): defined as $F\big(S \mapsto f(S \cup \{x\}) - f(S \setminus \{x\}),\ \tfrac12\big)$ .

Hypothesis: for every $x \in B$ ,

\omega_f(x) \;\le\; \frac{\mathrm{OPT}(f)}{n^2}.

Conclusion:

F\big(S \mapsto f(S \cup (B \cap C)),\ \tfrac12\big) \;\le\; F\big(f,\ \tfrac12\big) + \frac{\mathrm{OPT}(f)}{2n}.

$B$ is not required to be the complement of any particular set. It is only the set over which the hypothesis on $\omega_f$ is imposed.

Degenerate cases:

Division: since $n \ge 1$ , the divisions $\mathrm{OPT}(f)/n^2$ and $\mathrm{OPT}(f)/(2n)$ are genuine divisions, not division by zero.
$B = \emptyset$ : the hypothesis is vacuous, and the conclusion becomes $F(S \mapsto f(S),\tfrac12) \le F(f,\tfrac12) + \mathrm{OPT}(f)/(2n)$ .
$B \cap C = \emptyset$ : the same conclusion results, with the hypothesis still imposed on $B$ .
$|X| = 1$ : $n = 1$ and the bounds are $\mathrm{OPT}(f)$ and $\mathrm{OPT}(f)/2$ .
Satisfiability: whether the hypothesis can hold for nonempty $B$ depends on the unshown definitions of $F$ and $\mathrm{OPT}$ .

Human review

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

View graph

Proof of Theorem 2.6 — E[f(R∪(B∩C))]≤E[f(R)]+OPT/(2n)\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)E[f(R∪(B∩C))]≤E[f(R)]+OPT/(2n)

Proof of Theorem 2.6 — $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$