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

Proved

NonmonotoneSubmod.Nonadaptive.expect_inter_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 \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C).

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

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

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. 1140, third display).
For a nonnegative submodular `f`, `R = X(1/2)` and any `B, C ⊆ X`:
`E[f(R ∩ (B ∪ C))] ≥ ¼ f(C) + ¼ f(B ∪ C)`. -/
theorem expect_inter_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 C + (1 / 4) * f (B ∪ 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. 1140, §2, proof of Theorem 2.6, third 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(C) + \tfrac14\, f(B \cup C) \;\le\; F\big(S \mapsto f(S \cap (B \cup C)),\ \tfrac12\big).

$B$ is arbitrary. It is not required to be the complement of any set.

Degenerate cases:

$B \cup C = X$ : the right side is $F(S \mapsto f(S), \tfrac12)$ , and the left side is $\tfrac14 f(C) + \tfrac14 f(X)$ .
$B = C = \emptyset$ : the claim is $\tfrac12 f(\emptyset) \le F(S \mapsto f(\emptyset), \tfrac12)$ .
$X$ empty: the claim is also $\tfrac12 f(\emptyset) \le F(S \mapsto f(\emptyset), \tfrac12)$ . Its strength depends on the unshown definition of $F$ .
Hypotheses: there are no hypotheses beyond nonnegativity and the submodularity predicate.

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

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