Lemma 14 — universal upper bound from RANDOM on the triangular instance

Proved

KVVMatching.UpperBound.lemma_14

by mikedeng1 · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

bipartite-matchingonline-algorithmsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1yao-principle

For every randomized on-line matching algorithm $A$ on $n$ rows and $n$ columns, some graph $G$ with a perfect matching satisfies

\mathbb E_A[|M(G)|]\le V_{T_n}(n,\varnothing).

Thus the worst-case performance of any algorithm is at most RANDOM's expected matching size on the complete upper-triangular graph. The hard graph may depend on the algorithm, as required by the order of the quantifiers.

Formalization Note The statement ranges over all randomized rules, including non-greedy ones. A perfect matching is witnessed by a bijection between boys and girls whose edges lie in $G$ .

Preamble

import Mathlib
import Definitions.Def_KVVMatching_UpperBound_RandomValue
import Definitions.Def_KVVMatching_UpperBound_Triangular
import Definitions.Def_DiscreteConvex_IntegralConvexityB_IsPerfectMatchingBij

Formal statement

namespace KVVMatching.UpperBound

/-- Karp, Vazirani and Vazirani, Lemma 14 (p. 357). -/
theorem lemma_14 (n : ℕ) (A : RandomAlg n) :
    ∃ G : Graph n,
      (∃ σ : Fin n ≃ Fin n,
        DiscreteConvex.IntegralConvexityB.IsPerfectMatchingBij G σ) ∧
      expectedSize G A ≤ randomValue (upperTriangular n) := by sorry

end KVVMatching.UpperBound

Source

Karp, Vazirani, Vazirani, An Optimal Algorithm for On-line Bipartite Matching, STOC 1990, p. 357, Lemma 14

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph