Lemma 2.2 — $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$

Proved

NonmonotoneSubmod.RandomSet.lemma_2_2_sample_subset

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 and $g : 2^X \to \mathbb{R}$ a submodular function (of any sign). Let $A \subseteq X$ and $p \in [0,1]$ , and let $A(p)$ be the random subset of $A$ in which each element of $A$ appears independently with probability $p$ . Then

\mathbf{E}[g(A(p))] \ge (1-p)\, g(\emptyset) + p\, g(A).

In words: on a random sample of a fixed set, a submodular function does at least as well as the linear interpolation between its values at the empty set and at the full set. This is the basic probabilistic property of submodular functions on which Lemma 2.3 and the analysis of Algorithm RS rest.

Formalization Note The expectation is the exact finite sum $\mathbf{E}[g(A(p))] = \sum_{T \subseteq A} p^{|T|} (1-p)^{|A \setminus T|}\, g(T)$ . The hypothesis $0 \le p \le 1$ is added explicitly; the paper implies it by calling $p$ a probability. It is necessary: for $A = \{a, b\}$ and $g$ equal to $1$ on $\{a\}$ and $\{b\}$ and $0$ on $\emptyset$ and $A$ (submodular), the difference of the two sides is $p(1-p)\cdot 2$ , which is negative for $p = 2$ .

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular

Formal statement

namespace NonmonotoneSubmod.RandomSet

/-- Lemma 2.2 (Feige–Mirrokni–Vondrák 2011, p. 1137). Let `g : 2^X → ℝ` be submodular, `A ⊆ X`,
and let `A(p)` be the random subset of `A` containing each element of `A` independently with
probability `p ∈ [0,1]`. Then `E[g(A(p))] ≥ (1 - p) g(∅) + p g(A)`. The expectation is written as
the exact finite sum over `T ⊆ A` with weight `p^|T| (1-p)^|A \ T|`. -/
theorem lemma_2_2_sample_subset {X : Type} [Fintype X] [DecidableEq X]
    (g : Finset X → ℝ) (hg : NonmonotoneSubmod.Shared.Submodular g) (A : Finset X) (p : ℝ)
    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    (1 - p) * g ∅ + p * g A ≤
      ∑ T ∈ A.powerset, p ^ T.card * (1 - p) ^ (A \ T).card * g T := by sorry

end NonmonotoneSubmod.RandomSet

Source

Feige, Mirrokni, Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011, p. 1137, Lemma 2.2

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 $g$ be any real-valued function on the finite subsets of $X$ , $g : 2^X \to \mathbb{R}$ . Let $A \subseteq X$ be a finite set and let $p$ be a real number.

Hypotheses.

$g$ satisfies the predicate $\mathrm{Submodular}(g)$ . This predicate comes from the imported file Definitions.Def_NonmonotoneSubmod_Shared_Submodular. Its definition is not in the code given to me, so I cannot say exactly what it requires. Nothing else is assumed about $g$ : no nonnegativity, no monotonicity, and no normalization such as $g(\emptyset)=0$ , unless the predicate itself imposes them.
$0 \le p$ and $p \le 1$ .

Conclusion.

(1-p)\,g(\emptyset) + p\,g(A) \;\le\; \sum_{T \subseteq A} p^{|T|}\,(1-p)^{|A\setminus T|}\,g(T).

The sum runs over all $2^{|A|}$ subsets $T$ of $A$ . The statement makes no claim about probability or expectation. It is exactly this finite weighted sum.

Degenerate cases. Powers use the convention $0^0 = 1$ .

$A = \emptyset$ : the only term is $T=\emptyset$ , with weight $p^0(1-p)^0 = 1$ . The right side is $g(\emptyset)$ and the left side is $(1-p)g(\emptyset)+p\,g(\emptyset) = g(\emptyset)$ , so the claim holds with equality for every $g$ .
$p = 0$ : only $T=\emptyset$ has nonzero weight, which is $1$ . Both sides equal $g(\emptyset)$ .
$p = 1$ : only $T=A$ has nonzero weight, which is $1$ . Both sides equal $g(A)$ .
Empty $X$ : then $A=\emptyset$ , and the first case applies.
Assumption not used: the finiteness of $X$ does not appear anywhere in the inequality.

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

Lemma 2.2 — E[g(A(p))]≥(1−p) g(∅)+p g(A)\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)E[g(A(p))]≥(1−p)g(∅)+pg(A)

Lemma 2.2 — $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$