Proof of Theorem 2.1, display — $\mathbf{E}[f(R)] \ge \frac14 f(\emptyset) + \frac14 f(S) + \frac14 f(\bar S) + \frac14 f(X)$

Proved

NonmonotoneSubmod.RandomSet.uniform_four_corners

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

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

Let $X$ be a finite ground set, $f : 2^X \to \mathbb{R}$ submodular (of any sign), and let $R = X(1/2)$ be a uniformly random subset of $X$ , containing each element independently with probability $\tfrac12$ . For every $S \subseteq X$ , with complement $\bar S = X \setminus S$ ,

\mathbf{E}[f(R)] \ge \tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(\bar S) + \tfrac14 f(X).

This is the display in the proof of Theorem 2.1: writing $R = S(1/2) \cup \bar S(1/2)$ as the union of independent half-samples of $S$ and of $\bar S$ and applying Lemma 2.3 with $p = q = \tfrac12$ . Theorem 2.1 follows from it by taking $S$ optimal and discarding the nonnegative terms.

Formalization Note $\mathbf{E}[f(R)]$ is the multilinear extension $F$ at the constant vector $\tfrac12$ , i.e. $2^{-|X|} \sum_{S \subseteq X} f(S)$ . The statement holds for every $S \subseteq X$ ; optimality of $S$ is used only in Theorem 2.1. The identity between $X(1/2)$ and $S(1/2) \cup \bar S(1/2)$ is part of what this statement asserts.

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_NonmonotoneSubmod_Shared_F

Formal statement

namespace NonmonotoneSubmod.RandomSet

/-- Display in the proof of Theorem 2.1 (Feige–Mirrokni–Vondrák 2011, p. 1138). For a submodular
`f : 2^X → ℝ` and any `S ⊆ X`, the uniformly random subset `R = X(1/2) = S(1/2) ∪ S̄(1/2)` satisfies
`E[f(R)] ≥ ¼ f(∅) + ¼ f(S) + ¼ f(S̄) + ¼ f(X)`. -/
theorem uniform_four_corners {X : Type} [Fintype X] [DecidableEq X]
    (f : Finset X → ℝ) (hf : NonmonotoneSubmod.Shared.Submodular f) (S : Finset X) :
    (1 / 4) * f ∅ + (1 / 4) * f S + (1 / 4) * f Sᶜ + (1 / 4) * f Finset.univ ≤
      NonmonotoneSubmod.Shared.F f (fun _ => 1 / 2) := by sorry

end NonmonotoneSubmod.RandomSet

Source

Feige, Mirrokni, Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, p. 1138, §2, proof of Theorem 2.1, display

Read-back

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

Setting. Let $X$ be a finite type with decidable equality. Let $f : 2^X \to \mathbb{R}$ be any real-valued function on the subsets of $X$ , and let $S \subseteq X$ .

The statement uses two sets built from $X$ :

$S^{c} = X \setminus S$ is the complement of $S$ in $X$ .
$X$ itself appears as the set of all elements.

Hypothesis. $f$ satisfies the predicate $\mathrm{Submodular}(f)$ from the imported file Definitions.Def_NonmonotoneSubmod_Shared_Submodular. Its definition is not in the code given to me, so I cannot say what it requires. No other condition on $f$ is assumed.

Conclusion.

\tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(S^{c}) + \tfrac14 f(X) \;\le\; F\big(f,\ x \mapsto \tfrac12\big).

Here $\tfrac14$ is the real number $0.25$ . $F$ is an operator from the imported file Definitions.Def_NonmonotoneSubmod_Shared_F. It takes $f$ and a function that assigns the value $\tfrac12$ to every element of $X$ . The definition of $F$ is not in the code given to me, so I cannot say what $F(f, \cdot)$ computes. For the same reason, I cannot say what kind of number the constant $\tfrac12$ is. In particular, nothing here shows that $F$ is an expectation, a weighted sum over subsets, or any other particular quantity.

Degenerate cases. Whether each resulting inequality is trivial or restrictive depends entirely on the unseen definition of $F$ .

$S=\emptyset$ : then $S^{c}=X$ , and the left side is $\tfrac12 f(\emptyset)+\tfrac12 f(X)$ .
$S=X$ : the left side is also $\tfrac12 f(\emptyset)+\tfrac12 f(X)$ .
Empty $X$ : then $\emptyset = S = S^{c} = X$ , and the left side is $f(\emptyset)$ . The claim becomes $f(\emptyset) \le F(f, x\mapsto\tfrac12)$ .

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.1, display — E[f(R)]≥14f(∅)+14f(S)+14f(Sˉ)+14f(X)\mathbf{E}[f(R)] \ge \frac14 f(\emptyset) + \frac14 f(S) + \frac14 f(\bar S) + \frac14 f(X)E[f(R)]≥41​f(∅)+41​f(S)+41​f(Sˉ)+41​f(X)

Proof of Theorem 2.1, display — $\mathbf{E}[f(R)] \ge \frac14 f(\emptyset) + \frac14 f(S) + \frac14 f(\bar S) + \frac14 f(X)$