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

Proved

NonmonotoneSubmod.Nonadaptive.expect_inter_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$ , let $R = X(1/2)$ be a uniformly random subset of $X$ , and let $\omega$ be as in Definition 2.4. Let $A \subseteq X$ be a set with

\omega(x) \ge -\frac{OPT}{n^2} \quad \text{for every } x \in A,

and let $B = X \setminus A$ . Then for every $C \subseteq X$ ,

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

Removing from the random set the elements of $A \setminus C$ , whose averaged marginal values are at least $-OPT/n^2$ , can increase the expected value by at most $OPT/(2n)$ . It is the mirror image of the upper estimate for $\mathbf{E}[f(R \cup (B \cap C))]$ .

Formalization Note $B$ is the complement Aᶜ of $A$ ; both expectations are exact uniform averages over the $2^n$ subsets of $X$ . The ground set is assumed nonempty so that the divisions by $n$ are genuine. Nonnegativity of $f$ gives $OPT \ge 0$ , used in the step $-|A \setminus C|\,OPT/(2n^2) \ge -OPT/(2n)$ . The page writes " $=$ " before $-|A\setminus C|\,OPT/(2n^2)$ ; since each summand is only bounded below by $-OPT/(2n^2)$ , the correct relation is " $\ge$ ", and the statement here is the inequality the argument proves.

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. 1140, first two 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 ∈ A`, and `B = X \ A`, then for every `C ⊆ X`,
`E[f(R)] ≥ E[f(R ∩ (B ∪ C))] − OPT/(2n)`. -/
theorem expect_inter_upper {X : Type} [Fintype X] [DecidableEq X] [Nonempty X]
    (f : Finset X → ℝ) (hf0 : ∀ S, 0 ≤ f S) (hf : NonmonotoneSubmod.Shared.Submodular f) (A C : Finset X)
    (hA : ∀ x ∈ A, -(NonmonotoneSubmod.Shared.OPT f / (Fintype.card X : ℝ) ^ 2) ≤ omega f x) :
    NonmonotoneSubmod.Shared.F (fun S => f (S ∩ (Aᶜ ∪ C))) (fun _ => 1 / 2) - NonmonotoneSubmod.Shared.OPT f / (2 * (Fintype.card X : ℝ)) ≤
      NonmonotoneSubmod.Shared.F f (fun _ => 1 / 2) := by sorry

end NonmonotoneSubmod.Nonadaptive

Source

Feige, Mirrokni, Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, p. 1140, §2, proof of Theorem 2.6, first and second displays

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$ ;
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 $A, C \subseteq X$ .

Write $A^c = X \setminus A$ . The statement uses three external objects whose bodies are not shown:

$\mathrm{OPT}(f)$ (NonmonotoneSubmod.Shared.OPT): a real number determined by $f$ .
$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)$ : defined as $F\big(S \mapsto f(S \cup \{x\}) - f(S \setminus \{x\}),\ \tfrac12\big)$ .

Hypothesis: for every $x \in A$ ,

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

Conclusion:

F\big(S \mapsto f(S \cap (A^c \cup C)),\ \tfrac12\big) - \frac{\mathrm{OPT}(f)}{2n} \;\le\; F\big(f,\ \tfrac12\big).

Degenerate cases:

Division: since $n \ge 1$ , no division by zero occurs.
$A = \emptyset$ : the hypothesis is vacuous and $A^c \cup C = X$ . The conclusion becomes $F(S \mapsto f(S), \tfrac12) - \mathrm{OPT}(f)/(2n) \le F(f, \tfrac12)$ .
$A = X$ : $A^c = \emptyset$ , so the left-hand function is $S \mapsto f(S \cap C)$ , and the hypothesis is required at every element of $X$ .
$C = X$ : the left-hand function is $S \mapsto f(S)$ for every $A$ .
Satisfiability: whether the hypothesis is satisfiable for nonempty $A$ depends on the unshown definitions.

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)]≥E[f(R∩(B∪C))]−OPT/(2n)\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)E[f(R)]≥E[f(R∩(B∪C))]−OPT/(2n)

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