Proof of Theorem 2.6 — $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B\cap C) + \tfrac14 f(C)$

Proved

NonmonotoneSubmod.Nonadaptive.expect_union_lower

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

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

Let $f : 2^X \to \mathbb{R}_{\ge 0}$ be nonnegative and submodular on a finite ground set $X$ , let $R = X(1/2)$ be a uniformly random subset of $X$ , and let $B, C \subseteq X$ be arbitrary. Then

\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C).

In the proof of Theorem 2.6, $C$ is an optimal set and the right-hand side is $\beta/4 + OPT/4$ with $\beta = f(B\cap C)$ ; the bound comes from applying Lemma 2.3 to the submodular function $g(R) = f(R \cup (B \cap C))$ with the split $R = C(1/2) \cup \bar C(1/2)$ .

Formalization Note The expectation is the exact uniform average over the $2^{|X|}$ subsets $S$ of $X$ of $f(S \cup (B \cap C))$ . Nonnegativity of $f$ is the paper's standing assumption and is used for the discarded terms $g(\bar C)$ and $g(X)$ .

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_NonmonotoneSubmod_Shared_F

Formal statement

namespace NonmonotoneSubmod.Nonadaptive

/-- Proof of Theorem 2.6 (Feige–Mirrokni–Vondrák 2011, p. 1139, last display).
For a nonnegative submodular `f`, `R = X(1/2)` and any `B, C ⊆ X`:
`E[f(R ∪ (B ∩ C))] ≥ ¼ f(B ∩ C) + ¼ f(C)`. -/
theorem expect_union_lower {X : Type} [Fintype X] [DecidableEq X]
    (f : Finset X → ℝ) (hf0 : ∀ S, 0 ≤ f S) (hf : NonmonotoneSubmod.Shared.Submodular f) (B C : Finset X) :
    (1 / 4) * f (B ∩ C) + (1 / 4) * f C ≤
      NonmonotoneSubmod.Shared.F (fun S => f (S ∪ (B ∩ C))) (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. 1139, §2, proof of Theorem 2.6, last display

Read-back

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

This theorem uses:

a finite type $X$ with decidable equality (possibly empty);
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 one external object, $F$ (NonmonotoneSubmod.Shared.F). It returns a real number from a set function and the constant function $\tfrac12$ on $X$ , and its body is not shown.

The theorem asserts

\tfrac14\, f(B \cap C) + \tfrac14\, f(C) \;\le\; F\big(S \mapsto f(S \cup (B \cap C)),\ \tfrac12\big).

$B$ enters only through $B \cap C$ .

Degenerate cases:

$B \cap C = \emptyset$ : the claim is $\tfrac14 f(\emptyset) + \tfrac14 f(C) \le F(f, \tfrac12)$ .
$X$ empty: every set is $\emptyset$ , and the claim is $\tfrac12 f(\emptyset) \le F(S \mapsto f(S), \tfrac12)$ . How this compares with $f(\emptyset)$ depends on the unshown definition of $F$ .
Hypotheses: there are no hypotheses besides nonnegativity and the submodularity predicate. The inequality is claimed for all $B$ and $C$ .

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))]≥14f(B∩C)+14f(C)\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B\cap C) + \tfrac14 f(C)E[f(R∪(B∩C))]≥41​f(B∩C)+41​f(C)

Proof of Theorem 2.6 — $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B\cap C) + \tfrac14 f(C)$