Lemma 2.3 — $\mathbf{E}[f(A(p) \cup B(q))]$ bounded below by the four corners

Proved

NonmonotoneSubmod.RandomSet.lemma_2_3_two_samples

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 $f : 2^X \to \mathbb{R}$ a submodular function (of any sign). Let $A, B \subseteq X$ be two sets, not necessarily disjoint, and $p, q \in [0,1]$ . Let $A(p)$ and $B(q)$ be independently sampled subsets: each element of $A$ appears in $A(p)$ independently with probability $p$ , each element of $B$ appears in $B(q)$ independently with probability $q$ , and the two samples are independent of each other. Then

\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q)\, f(\emptyset) + p(1-q)\, f(A) + (1-p)q\, f(B) + pq\, f(A \cup B).

The right-hand side is the bilinear interpolation of $f$ between the four "corners" $\emptyset$ , $A$ , $B$ , $A \cup B$ . The lemma is the tool behind the analyses of the random set algorithm (Theorem 2.1), the nonadaptive algorithm (Theorem 2.6) and smooth local search (Theorem 3.6).

Formalization Note The expectation over the pair of independent samples is the exact double sum

\sum_{S \subseteq A} \sum_{T \subseteq B} p^{|S|}(1-p)^{|A \setminus S|}\; q^{|T|}(1-q)^{|B \setminus T|}\; f(S \cup T).

Overlapping $A$ and $B$ are allowed, as printed; an element of $A \cap B$ then lies in $A(p) \cup B(q)$ with probability $1-(1-p)(1-q)$ , which the double sum accounts for. The hypotheses $0 \le p, q \le 1$ are added explicitly; the paper implies them by calling $p, q$ probabilities.

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular

Formal statement

namespace NonmonotoneSubmod.RandomSet

/-- Lemma 2.3 (Feige–Mirrokni–Vondrák 2011, p. 1137). Let `f : 2^X → ℝ` be submodular, let
`A, B ⊆ X` be two (not necessarily disjoint) sets, and let `A(p)`, `B(q)` be independently sampled
subsets (each element of `A` in `A(p)` with probability `p`, each element of `B` in `B(q)` with
probability `q`). Then
`E[f(A(p) ∪ B(q))] ≥ (1-p)(1-q) f(∅) + p(1-q) f(A) + (1-p)q f(B) + pq f(A ∪ B)`.
The expectation over the pair of independent samples is the exact double sum over `S ⊆ A`,
`T ⊆ B` with weights `p^|S| (1-p)^|A \ S|` and `q^|T| (1-q)^|B \ T|`. -/
theorem lemma_2_3_two_samples {X : Type} [Fintype X] [DecidableEq X]
    (f : Finset X → ℝ) (hf : NonmonotoneSubmod.Shared.Submodular f) (A B : Finset X) (p q : ℝ)
    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
    (1 - p) * (1 - q) * f ∅ + p * (1 - q) * f A + (1 - p) * q * f B + p * q * f (A ∪ B) ≤
      ∑ S ∈ A.powerset, ∑ T ∈ B.powerset,
        (p ^ S.card * (1 - p) ^ (A \ S).card) * (q ^ T.card * (1 - q) ^ (B \ T).card) *
          f (S ∪ 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.3

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 finite subsets of $X$ . Let $A, B \subseteq X$ be finite sets; they may overlap or coincide. Let $p, q$ be real numbers.

Hypotheses.

$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 imposed: no sign condition, monotonicity or normalization.
$0 \le p \le 1$ .
$0 \le q \le 1$ .

Conclusion.

(1-p)(1-q)\,f(\emptyset) + p(1-q)\,f(A) + (1-p)q\,f(B) + pq\,f(A\cup B) \;\le\; \sum_{S \subseteq A}\ \sum_{T \subseteq B} \Big(p^{|S|}(1-p)^{|A\setminus S|}\Big)\Big(q^{|T|}(1-q)^{|B\setminus T|}\Big)\, f(S\cup T).

The double sum runs over all ordered pairs $(S,T)$ with $S \subseteq A$ and $T \subseteq B$ . When $A$ and $B$ overlap, different pairs can have the same union $S\cup T$ . Each such pair is counted separately, with its own weight. The statement is only about this finite sum; it does not mention probability or independence.

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

$A=B=\emptyset$ : the only term is $S=T=\emptyset$ , with weight $1$ . The left side's coefficients sum to $1$ , and every set on the left is $\emptyset$ . Both sides equal $f(\emptyset)$ .
$p=q=0$ : only $S=T=\emptyset$ has nonzero weight. Both sides equal $f(\emptyset)$ .
$p=q=1$ : only $S=A$ , $T=B$ has nonzero weight. Both sides equal $f(A\cup B)$ .
$A=B$ : the left side becomes

\big((1-p)(1-q)\big)f(\emptyset) + \big(p(1-q)+(1-p)q+pq\big)f(A).

Empty $X$ : then $A=B=\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.3 — E[f(A(p)∪B(q))]\mathbf{E}[f(A(p) \cup B(q))]E[f(A(p)∪B(q))] bounded below by the four corners

Lemma 2.3 — $\mathbf{E}[f(A(p) \cup B(q))]$ bounded below by the four corners