Lemma 16 — asymptotic value of RANDOM on the triangular instance

Proved

KVVMatching.UpperBound.lemma_16

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

asymptoticsbipartite-matchingonline-algorithmsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $T_n$ be the $n\times n$ complete upper-triangular graph. The expected matching size of RANDOM on $T_n$ is $n(1-1/e)+o(n)$ , in the two-sided sense

\lim_{n\to\infty}\frac{V_{T_n}(n,\varnothing)}{n}=1-e^{-1}.

This supplies the asymptotic value used in Theorem 2.

Formalization Note The paper writes $o(n)$ without a numerical rate. The value at $n=0$ is defined by Lean's total division but does not affect the limit.

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 16 (p. 357). -/
theorem lemma_16 :
    Filter.Tendsto
      (fun n : ℕ => randomValue (upperTriangular n) / (n : ℝ))
      Filter.atTop (nhds (1 - Real.exp (-1))) := by sorry

end KVVMatching.UpperBound

Source

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

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