Lemma 2.2 — random subsets of a set, one sample

Proved

NonmonotoneSubmod.Nonadaptive.lemma_2_2_sample_subset

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

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

Let $g : 2^X \to \mathbb{R}$ be submodular, let $A \subseteq X$ , and let $A(p)$ be the random subset of $A$ in which each element of $A$ appears independently with probability $p \in [0,1]$ . Then

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

The expected value of a submodular function on a random subset of $A$ is at least the corresponding average of its values at the two extreme subsets $\emptyset$ and $A$ . It is the basic probabilistic property of submodular functions on which all the sampling estimates of the paper rest.

Formalization Note The expectation is the exact finite sum $\sum_{T \subseteq A} p^{|T|}(1-p)^{|A \setminus T|}\, g(T)$ . The hypothesis $0 \le p \le 1$ is implicit in "with probability $p$ " and is stated explicitly; the lemma fails for $p$ outside $[0,1]$ . No sign condition on $g$ is assumed, as on the page.

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular

Formal statement

namespace NonmonotoneSubmod.Nonadaptive

/-- 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.Nonadaptive

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

This theorem uses:

a finite type $X$ with decidable equality;
a set function $g : 2^X \to \mathbb{R}$ that satisfies the predicate NonmonotoneSubmod.Shared.Submodular (an external definition whose body is not shown; its name indicates submodularity);
an arbitrary subset $A \subseteq X$ ;
a real number $p$ with $0 \le p \le 1$ .

It asserts

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

The right side is written explicitly as a finite sum over all subsets $T$ of $A$ , with weight $p^{|T|}(1-p)^{|A\setminus T|}$ . No probability measure appears in the statement. Only $g(\emptyset)$ , $g(A)$ and the values of $g$ on subsets of $A$ occur in the inequality, but the submodularity hypothesis is imposed on $g$ over all of $2^X$ .

Degenerate cases, with the convention $0^0 = 1$ :

$p = 0$ : only the $T = \emptyset$ term survives, so both sides equal $g(\emptyset)$ .
$p = 1$ : only the $T = A$ term survives, so both sides equal $g(A)$ .
$A = \emptyset$ , including the case $X$ empty: the sum has the single term $g(\emptyset)$ and the left side is $g(\emptyset)$ , so the inequality is an equality.
Values of $p$ : the hypotheses allow every $p$ in the closed interval $[0,1]$ . They are always satisfiable.

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