Lemma 13 — greedy algorithms on permuted triangular instances

Proved

KVVMatching.UpperBound.lemma_13

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

bipartite-matchingonline-algorithmsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1probability

Let $T_n$ be the complete upper-triangular bipartite graph with $n$ rows and $n$ columns. For every deterministic greedy on-line algorithm $a$ , the average matching size over uniform row permutations $\pi$ equals the expected matching size of RANDOM on $T_n$ :

\frac{1}{n!}\sum_{\pi}|M_a(T_\pi)|=V_{T_n}(n,\varnothing).

This identifies the value of every greedy deterministic rule against the paper's uniform hard-input distribution.

Formalization Note The row permutation sends the old row $i$ to $\pi(i)$ ; reversing this convention leaves the uniform average unchanged. The equation also holds when $n=0$ .

Preamble

import Mathlib
import Definitions.Def_KVVMatching_UpperBound_RandomValue
import Definitions.Def_KVVMatching_UpperBound_Triangular

Formal statement

namespace KVVMatching.UpperBound

/-- Karp, Vazirani and Vazirani, Lemma 13 (p. 357). -/
theorem lemma_13 (n : ℕ) (a : DetAlg n) (ha : IsGreedy a) :
    (1 / (n.factorial : ℝ)) *
      (∑ π : Equiv.Perm (Fin n),
        (matchingSize (permutedTriangular π) 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 13

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