Online bipartite matching

DefinitionGreedy step of online bipartite matching#✓fully proved

Consider a bipartite graph with left vertices \(0, \dots, a-1\) and right vertices \(0, \dots, b-1\), and an assignment \(m\) giving each right vertex either a left partner or none. On the arrival of a right vertex \(j\), the greedy step returns the assignment that agrees with \(m\) at every right vertex other than \(j\), and gives \(j\) the smallest left neighbour of \(j\) that is free in \(m\) (the partner of no right vertex), or no partner if \(j\) has no free neighbour.

def step (mate : Fin b → Option (Fin a)) (j : Fin b) : Fin b → Option (Fin a) :=
  Function.update mate j
    ((List.finRange a).find? fun i => decide (j ∈ adj i) && decide (Free mate i))
Uses 1 · Used by 5
Statement usesUnmatched left vertex
Used byGreedy online bipartite matching · The greedy matching is maximal · Invariants of the greedy run · The greedy online matching is a matching · Earlier partners survive an arrival

DefinitionGreedy online bipartite matching#✓fully proved

Consider a bipartite graph with left vertices \(0, \dots, a-1\) and right vertices \(0, \dots, b-1\), an assignment \(m\) giving each right vertex either a left partner or none, and a list \(j_1, \dots, j_n\) of right vertices, the arrivals in order. The greedy matching from \(m\) on these arrivals is the assignment obtained from \(m\) by applying the greedy step of online bipartite matching for the arrival of \(j_1\), then of \(j_2\), and so on up to \(j_n\); if the list is empty, it is \(m\).

def greedy (js : List (Fin b)) (mate : Fin b → Option (Fin a)) : Fin b → Option (Fin a) :=
  js.foldl (step adj) mate
Uses 1 · Used by 3
Statement usesGreedy step of online bipartite matching
Used byThe greedy matching is maximal · Invariants of the greedy run · The greedy online matching is a matching

TheoremEarlier partners survive an arrival#✓fully proved

Let \(m\) be an assignment giving each right vertex of a bipartite graph either a left partner or none, and let \(j\) be a right vertex with no partner in \(m\). If a right vertex \(j'\) has partner \(i\) in \(m\), then \(j'\) still has partner \(i\) after the greedy step for the arrival of \(j\).

theorem step_extends {mate : Fin b → Option (Fin a)} {j : Fin b} (hj : mate j = none)
    {j' : Fin b} {i : Fin a} (h : mate j' = some i) : step adj mate j j' = some i
Uses 2 · Used by 1
Statement usesGreedy step of online bipartite matching
Proof usesUnmatched left vertex
Used byInvariants of the greedy run

DefinitionDone right vertices#✓fully proved

Given a partner array, which assigns to each right vertex its partner on the left if it has one, the right vertices of a list \(S\) are done when, for every right vertex \(j\) of \(S\) and every left vertex \(i\) adjacent to \(j\), \(j\) is matched or \(i\) is matched.

def Done (mate : Fin b → Option (Fin a)) (S : List (Fin b)) : Prop :=
  ∀ j ∈ S, ∀ i, j ∈ adj i → mate j ≠ none ∨ ¬ Free mate i
Uses 1 · Used by 3
Statement usesUnmatched left vertex
Used byThe greedy matching is maximal · Invariants of the greedy run · The greedy online matching is a matching

TheoremInvariants of the greedy run#✓fully proved

Let \(L\) be a list of distinct right vertices, all unmatched in a valid partner array \(m\), and let \(S\) be a list of right vertices that are done for \(m\). Then the partner array obtained from \(m\) by the greedy run along \(L\) is valid, and every right vertex of \(L\) or of \(S\) is done for it.

theorem greedy_spec : ∀ (js : List (Fin b)) (mate : Fin b → Option (Fin a)) (S : List (Fin b)),
    js.Nodup → (∀ j ∈ js, mate j = none) → Valid adj mate → Done adj mate S →
    Valid adj (greedy adj js mate) ∧ Done adj (greedy adj js mate) (js.reverse ++ S)
Uses 6 · Used by 2
Statement usesPartner arrays that describe a matching · Done right vertices · Greedy online bipartite matching
Proof usesUnmatched left vertex · Greedy step of online bipartite matching · Earlier partners survive an arrival
Used byThe greedy matching is maximal · The greedy online matching is a matching

DefinitionPartner assignment from an array#✓fully proved

An array \(A\) whose entries are each a left vertex or none is read as an assignment of partners to the right vertices \(0, \dots, b-1\): right vertex \(j\) gets the entry of \(A\) at index \(j\) when \(j\) is less than the length of \(A\), and no partner otherwise.

def toFun (arr : Array (Option (Fin a))) : Fin b → Option (Fin a) := fun j => arr.getD j none
Used by 4
Used byThe greedy online matching · The greedy matching is maximal · The greedy online matching is a matching · Greedy step on an array

DefinitionGreedy step on an array#✓fully proved

In a bipartite graph with left vertices \(0, \dots, a - 1\) and right vertices \(0, \dots, b - 1\), take an array whose entry \(k\) holds the partner of the right vertex \(k\), a missing entry meaning no partner. On the arrival of a right vertex \(j\), entry \(j\) is set to the first left neighbour of \(j\), in the order \(0, \dots, a - 1\), that is free, that is, the partner of none of the right vertices \(0, \dots, b - 1\) in the array, or to none if no neighbour of \(j\) is free; if the array has no entry \(j\), it is unchanged.

Storing the partners in an array computes each choice once per arrival; evaluating the composed function updates of the specification directly would recompute every earlier choice at each lookup, a cost exponential in the number of right vertices.

def stepArr (arr : Array (Option (Fin a))) (j : Fin b) : Array (Option (Fin a)) :=
  arr.set! j ((List.finRange a).find? fun i =>
    decide (j ∈ adj i) && decide (Free (toFun (b := b) arr) i))
Uses 2 · Used by 3
Statement usesUnmatched left vertex · Partner assignment from an array
Used byThe greedy matching is maximal · Greedy run on an array · The greedy online matching is a matching

DefinitionGreedy run on an array#✓fully proved

In a bipartite graph with left vertices \(0, \dots, a - 1\) and right vertices \(0, \dots, b - 1\), start from an array whose entry \(k\) holds the partner of the right vertex \(k\), a missing entry meaning no partner, and let the right vertices of a list \(L\) arrive one after another in the order of \(L\). Each arrival performs the greedy step on the array: the entry of the arriving vertex \(j\) is set to the first left neighbour of \(j\), in the order \(0, \dots, a - 1\), that is free, that is, the partner of none of the right vertices \(0, \dots, b - 1\) in the current array, or to none if no neighbour of \(j\) is free; if the array has no entry \(j\), it is unchanged.

def greedyArr (js : List (Fin b)) (arr : Array (Option (Fin a))) : Array (Option (Fin a)) :=
  js.foldl (stepArr adj) arr
Uses 1 · Used by 3
Statement usesGreedy step on an array
Used byThe greedy online matching · The greedy matching is maximal · The greedy online matching is a matching

DefinitionThe greedy online matching#✓fully proved

In a bipartite graph with left vertices \(0, \dots, a - 1\) and right vertices \(0, \dots, b - 1\), the greedy online matching is the partner array obtained by starting from the empty matching and letting the right vertices arrive in the order \(0, 1, \dots, b - 1\), each arriving vertex being matched to its first free left neighbour in the order \(0, \dots, a - 1\), or left unmatched if no neighbour is free.

It is computed on arrays, with one array write per arrival.

def greedyAll : Fin b → Option (Fin a) :=
  toFun (greedyArr adj (List.finRange b) (Array.replicate b none))
Uses 2 · Used by 4
Statement usesGreedy run on an array · Partner assignment from an array
Used byGreedy online matching is 1/2-competitive · Greedy online matching is within a factor \(2\) of the maximum · The greedy matching is maximal · The greedy online matching is a matching

TheoremThe greedy matching is maximal#✓fully proved

Every edge has a matched endpoint.

theorem greedyAll_maximal {i : Fin a} {j : Fin b} (h : j ∈ adj i) :
    greedyAll adj j ≠ none ∨ ¬ Free (greedyAll adj) i
Uses 10 · Used by 1
Statement usesUnmatched left vertex · The greedy online matching
Proof usesPartner arrays that describe a matching · Done right vertices · Greedy online bipartite matching · Greedy run on an array · Invariants of the greedy run · Greedy step of online bipartite matching · Greedy step on an array · Partner assignment from an array
Used byGreedy online matching is 1/2-competitive

TheoremGreedy online matching is 1/2-competitive#✓fully proved

Every matching has at most twice as many edges as the greedy one. An edge of the matching whose right vertex the greedy algorithm matched is charged to that right vertex, any other edge to its left vertex, which the greedy algorithm matched by maximality; a matching charges each greedy edge at most once on each side.

theorem card_le_two_mul_greedyAll {M : Finset (Fin a × Fin b)} (hM : IsMatching adj M) :
    M.card ≤ 2 * (pairs (greedyAll adj)).card
Uses 5 · Used by 1
Statement usesMatching in a bipartite graph · Matched pairs of a partner assignment · The greedy online matching
Proof usesUnmatched left vertex · The greedy matching is maximal
Used byGreedy online matching is within a factor \(2\) of the maximum

TheoremThe greedy online matching is a matching#✓fully proved

The set of pairs \((i, j)\) such that the greedy online matching assigns the left vertex \(i\) to the right vertex \(j\) is a matching of the bipartite graph.

theorem isMatching_greedyAll : IsMatching adj (pairs (greedyAll adj))
Uses 13
Statement usesMatching in a bipartite graph · Matched pairs of a partner assignment · The greedy online matching
Proof usesUnmatched left vertex · Partner arrays that describe a matching · A valid partner array gives a matching · Done right vertices · Greedy online bipartite matching · Greedy run on an array · Invariants of the greedy run · Greedy step of online bipartite matching · Greedy step on an array · Partner assignment from an array

TheoremGreedy online matching is within a factor \(2\) of the maximum#✓fully proved

In a bipartite graph, the maximum matching computed by augmenting paths has at most twice as many edges as the greedy online matching, in which the right vertices arrive in increasing order.

theorem card_maxMatching_le : (pairs (maxMatching adj)).card ≤ 2 * (pairs (greedyAll adj)).card
Uses 5
Statement usesThe augmenting-path maximum matching · Matched pairs of a partner assignment · The greedy online matching
Proof usesThe augmenting-path algorithm returns a matching · Greedy online matching is 1/2-competitive

StructureDeterministic online bipartite matching algorithm#✓fully proved

A deterministic online bipartite matching algorithm with \(a\) offline (left) vertices \(0, \dots, a - 1\) is given by a proposal rule: on each arrival it receives the neighbour lists (lists of left vertices) of all earlier arrivals, in order, and the neighbour list of the current arrival, and proposes a left vertex to match the arrival to, or none.

structure OnlineMatcher (a : ℕ) where
  /-- The proposal for the current arrival, from the earlier arrivals and the current one. -/
  choose : List (List (Fin a)) → List (Fin a) → Option (Fin a)
Used by 9
Used byThe adversary for online bipartite matching · The adversary's offline matching · The \(1/2\) lower bound with a matching of the arrivals' graph · No deterministic online bipartite matching algorithm beats 1/2 · The adversary's arrivals have a perfect matching · Number of arrivals an online matcher matches · The adversary holds every algorithm to one match per gadget · No deterministic online matcher beats ratio \(1/2\), with any additive constant · Finite-size lower bound for deterministic online matching

DefinitionNumber of arrivals an online matcher matches#✓fully proved

Let \(A\) be an online matcher with \(a\) left vertices, \(h\) a history (the neighbour lists of earlier arrivals), \(U\) a list of left vertices already matched, and \(\sigma\) a sequence of arrivals, each given by its list of left neighbours. The run of \(A\) on \(\sigma\) takes the arrivals in order: on an arrival with neighbour list \(N\), \(A\) proposes a left vertex, or none, from the current history and \(N\); a proposal \(i\) with \(i \in N\) and \(i \notin U\) is accepted, counting the arrival as matched and adding \(i\) to \(U\), and otherwise the arrival stays unmatched; then \(N\) is appended to the history. The value is the number of arrivals matched.

def matched (A : OnlineMatcher a) : List (List (Fin a)) → List (Fin a) → List (List (Fin a)) → ℕ
  | _, _, [] => 0
  | h, used, nbrs :: σ =>
      match A.choose h nbrs with
      | some i =>
          if i ∈ nbrs ∧ i ∉ used then 1 + matched A (h ++ [nbrs]) (i :: used) σ
          else matched A (h ++ [nbrs]) used σ
      | none => matched A (h ++ [nbrs]) used σ
Uses 1 · Used by 5
Statement usesDeterministic online bipartite matching algorithm
Used byThe \(1/2\) lower bound with a matching of the arrivals' graph · No deterministic online bipartite matching algorithm beats 1/2 · The adversary holds every algorithm to one match per gadget · No deterministic online matcher beats ratio \(1/2\), with any additive constant · Finite-size lower bound for deterministic online matching

DefinitionPerfect matchings of a sequence of arrivals#✓fully proved

A list \(m\) of left vertices is a perfect matching of a sequence \(\sigma\) of arrivals (neighbour lists) when \(m\) and \(\sigma\) have the same length, the entries of \(m\) are pairwise distinct, and for each \(j\) the \(j\)-th entry of \(m\) lies in the \(j\)-th neighbour list of \(\sigma\).

def IsPerfect (σ : List (List (Fin a))) (m : List (Fin a)) : Prop :=
  m.Nodup ∧ List.Forall₂ (fun i nbrs => i ∈ nbrs) m σ
Used by 6
Used byThe \(1/2\) lower bound with a matching of the arrivals' graph · Perfect matchings of the arrivals are matchings of their graph · No deterministic online bipartite matching algorithm beats 1/2 · The adversary's arrivals have a perfect matching · No deterministic online matcher beats ratio \(1/2\), with any additive constant · Finite-size lower bound for deterministic online matching

DefinitionGraph of a sequence of arrivals#✓fully proved

For a sequence \(\sigma = (\sigma_0, \dots, \sigma_{k-1})\) of arrivals, each a list of left vertices in \(\{0, \dots, a - 1\}\), the bipartite graph of \(\sigma\) is given by adjacency lists: left vertex \(i\) is sent to the list, in increasing order, of the arrivals \(j < k\) with \(i \in \sigma_j\).

def toAdj (σ : List (List (Fin a))) : Fin a → List (Fin σ.length) :=
  fun i => (List.finRange σ.length).filter fun j => decide (i ∈ σ[j])
Used by 2
Used byThe \(1/2\) lower bound with a matching of the arrivals' graph · Perfect matchings of the arrivals are matchings of their graph

TheoremPerfect matchings of the arrivals are matchings of their graph#✓fully proved

Let \(\sigma\) be a sequence of arrivals (neighbour lists) and \(m\) a perfect matching of \(\sigma\). Then the bipartite graph of \(\sigma\), in which left vertex \(i\) is adjacent to arrival \(j\) when \(i\) lies in the \(j\)-th neighbour list, has a matching with as many edges as \(\sigma\) has arrivals.

theorem exists_isMatching_of_isPerfect {σ : List (List (Fin a))} {m : List (Fin a)}
    (hp : IsPerfect σ m) : ∃ M : Finset (Fin a × Fin σ.length),
      BipartiteMatching.IsMatching (toAdj σ) M ∧ M.card = σ.length
Uses 3 · Used by 1
Statement usesMatching in a bipartite graph · Perfect matchings of a sequence of arrivals · Graph of a sequence of arrivals
Used byThe \(1/2\) lower bound with a matching of the arrivals' graph

DefinitionThe adversary for online bipartite matching#✓fully proved

Let \(A\) be an online matcher, \(h\) a list of earlier neighbour lists and \(ps\) a list of gadgets, pairs \((u, v)\) of left vertices. The adversary's sequence of arrivals is empty when \(ps\) is empty. Otherwise, for the first gadget \((u, v)\), let \(x = v\) if \(A\), after the history \(h\), proposes \(v\) for an arrival with neighbour list \([u, v]\), and \(x = u\) otherwise (a proposal of \(u\), of no vertex, or of a non-neighbour). The sequence is an arrival with neighbour list \([u, v]\), then an arrival with neighbour list \([x]\), then the adversary's sequence for \(A\), the history \(h\) extended by \([u, v]\) and \([x]\), and the remaining gadgets.

def adversary (A : OnlineMatcher a) : List (List (Fin a)) → List (Fin a × Fin a) →
    List (List (Fin a))
  | _, [] => []
  | h, (u, v) :: ps =>
      let x := if A.choose h [u, v] = some v then v else u
      [u, v] :: [x] :: adversary A (h ++ [[u, v], [x]]) ps
Uses 1 · Used by 3
Statement usesDeterministic online bipartite matching algorithm
Used byNo deterministic online bipartite matching algorithm beats 1/2 · The adversary's arrivals have a perfect matching · The adversary holds every algorithm to one match per gadget

DefinitionThe adversary's offline matching#✓fully proved

Let \(A\) be an online matcher, \(h\) a list of earlier neighbour lists and \(ps\) a list of gadgets, pairs \((u, v)\) of left vertices. The list \(\mathrm{opt}(A, h, ps)\) of left vertices is empty when \(ps\) is empty. Otherwise, for the first gadget \((u, v)\), let \(x = v\) if \(A\), after the history \(h\), proposes \(v\) for an arrival with neighbour list \([u, v]\), and \(x = u\) otherwise; the list starts with \(u, v\) in the first case and with \(v, u\) in the second, and continues with \(\mathrm{opt}(A, h', ps')\), where \(h'\) is \(h\) extended by the neighbour lists \([u, v]\) and \([x]\) and \(ps'\) is the list of remaining gadgets.

def adversaryOpt (A : OnlineMatcher a) : List (List (Fin a)) → List (Fin a × Fin a) → List (Fin a)
  | _, [] => []
  | h, (u, v) :: ps =>
      let x := if A.choose h [u, v] = some v then v else u
      (if A.choose h [u, v] = some v then u else v) :: x :: adversaryOpt A (h ++ [[u, v], [x]]) ps
Uses 1 · Used by 2
Statement usesDeterministic online bipartite matching algorithm
Used byNo deterministic online bipartite matching algorithm beats 1/2 · The adversary's arrivals have a perfect matching

DefinitionGadgets with distinct vertices#✓fully proved

A list of gadgets, pairs \((u, v)\) of left vertices, has distinct vertices when \(u \ne v\) for every gadget \((u, v)\) of the list, and any two gadgets \((u, v)\) and \((u', v')\) at different positions of the list share no vertex: \(u \ne u'\), \(u \ne v'\), \(v \ne u'\) and \(v \ne v'\).

def GadgetsDisjoint (ps : List (Fin a × Fin a)) : Prop :=
  (∀ p ∈ ps, p.1 ≠ p.2) ∧
    ps.Pairwise fun p q => p.1 ≠ q.1 ∧ p.1 ≠ q.2 ∧ p.2 ≠ q.1 ∧ p.2 ≠ q.2
Used by 2
Used byNo deterministic online bipartite matching algorithm beats 1/2 · The adversary's arrivals have a perfect matching

TheoremThe adversary holds every algorithm to one match per gadget#✓fully proved

For every online matcher \(A\), every list \(h\) of earlier neighbour lists, every list \(U\) of left vertices and every list of \(k\) gadgets, the run of \(A\) on the adversary's arrivals for \(A\), \(h\) and the gadgets, after the history \(h\) and with the left vertices of \(U\) already matched, matches at most \(k\) arrivals.

theorem matched_adversary_le (A : OnlineMatcher a) : ∀ (h : List (List (Fin a)))
    (used : List (Fin a)) (ps : List (Fin a × Fin a)),
    matched A h used (adversary A h ps) ≤ ps.length
Uses 3 · Used by 1
Statement usesDeterministic online bipartite matching algorithm · The adversary for online bipartite matching · Number of arrivals an online matcher matches
Used byNo deterministic online bipartite matching algorithm beats 1/2

TheoremThe adversary's arrivals have a perfect matching#✓fully proved

For every online matcher \(A\), every list \(h\) of earlier neighbour lists and every list of gadgets with distinct vertices, the adversary's offline matching for \(A\), \(h\) and the gadgets is a perfect matching of the adversary's arrivals for \(A\), \(h\) and the gadgets. In each gadget, the first arrival takes the vertex the second one does not.

theorem isPerfect_adversaryOpt (A : OnlineMatcher a) : ∀ (h : List (List (Fin a)))
    (ps : List (Fin a × Fin a)), GadgetsDisjoint ps →
    IsPerfect (adversary A h ps) (adversaryOpt A h ps)
Uses 5 · Used by 1
Statement usesGadgets with distinct vertices · Perfect matchings of a sequence of arrivals · Deterministic online bipartite matching algorithm · The adversary for online bipartite matching · The adversary's offline matching
Used byNo deterministic online bipartite matching algorithm beats 1/2

DefinitionThe \(n\) gadgets on \(2n\) left vertices#✓fully proved

For \(n \in \mathbb{N}\), the list of gadgets \((0, 1), (2, 3), \dots, (2n - 2, 2n - 1)\) of left vertices in \(\{0, \dots, 2n - 1\}\), that is, the pairs \((2k, 2k + 1)\) for \(k = 0, \dots, n - 1\) in increasing order of \(k\).

def gadgets (n : ℕ) : List (Fin (2 * n) × Fin (2 * n)) :=
  (List.finRange n).map fun (k : Fin n) =>
    (⟨2 * k, by have := k.isLt; omega⟩, ⟨2 * k + 1, by have := k.isLt; omega⟩)
Used by 1
Used byNo deterministic online bipartite matching algorithm beats 1/2

TheoremNo deterministic online bipartite matching algorithm beats 1/2#✓fully proved

No deterministic online bipartite matching algorithm beats 1/2 (Karp, Vazirani and Vazirani): against every algorithm with 2 n left vertices, some sequence of 2 n arrivals has a perfect matching while the algorithm matches at most n of them.

theorem exists_perfect_matched_le (n : ℕ) (A : OnlineMatcher (2 * n)) :
    ∃ σ m, IsPerfect σ m ∧ m.length = 2 * n ∧ σ.length = 2 * n ∧ matched A [] [] σ ≤ n
Uses 9 · Used by 2
Statement usesPerfect matchings of a sequence of arrivals · Deterministic online bipartite matching algorithm · Number of arrivals an online matcher matches
Proof usesGadgets with distinct vertices · The adversary for online bipartite matching · The adversary's offline matching · The \(n\) gadgets on \(2n\) left vertices · The adversary's arrivals have a perfect matching · The adversary holds every algorithm to one match per gadget
Used byThe \(1/2\) lower bound with a matching of the arrivals' graph · Finite-size lower bound for deterministic online matching

TheoremThe \(1/2\) lower bound with a matching of the arrivals' graph#✓fully proved

For every \(n \in \mathbb{N}\) and every online matcher \(A\) with \(2n\) left vertices, there is a sequence \(\sigma\) of arrivals (neighbour lists) such that the bipartite graph of \(\sigma\), in which left vertex \(i\) is adjacent to arrival \(j\) when \(i\) lies in the \(j\)-th neighbour list, has a matching with \(2n\) edges, while \(A\), run on \(\sigma\) from the empty history with no left vertex matched, matches at most \(n\) arrivals.

theorem exists_isMatching_matched_le (n : ℕ) (A : OnlineMatcher (2 * n)) :
    ∃ σ : List (List (Fin (2 * n))), ∃ M : Finset (Fin (2 * n) × Fin σ.length),
      BipartiteMatching.IsMatching (toAdj σ) M ∧ M.card = 2 * n ∧ matched A [] [] σ ≤ n
Uses 7
Statement usesMatching in a bipartite graph · Deterministic online bipartite matching algorithm · Number of arrivals an online matcher matches · Graph of a sequence of arrivals
Proof usesPerfect matchings of a sequence of arrivals · Perfect matchings of the arrivals are matchings of their graph · No deterministic online bipartite matching algorithm beats 1/2

TheoremFinite-size lower bound for deterministic online matching#✓fully proved

Let \(n\), \(b\), \(c\), \(d\) be natural numbers with \(d < 2c\) and \(b < n\). For every online matcher \(A\) with \(2n\) left vertices there are a sequence \(\sigma\) of arrivals and a perfect matching \(m\) of \(\sigma\) such that \(d \cdot \mathrm{ALG} + b < c \cdot |m|\), where \(\mathrm{ALG}\) is the number of arrivals of \(\sigma\) that \(A\) matches when run from the empty history with no left vertex matched, and \(|m|\) is the length of \(m\).

At a fixed size some additive constant always suffices, which is why \(b\) is bounded by \(n\); letting the size grow removes the bound.

theorem not_competitive_of_lt (n : ℕ) {c d : ℕ} (hcd : d < 2 * c) {b : ℕ} (hb : b < n)
    (A : OnlineMatcher (2 * n)) :
    ∃ σ m, IsPerfect σ m ∧ d * matched A [] [] σ + b < c * m.length
Uses 4 · Used by 1
Statement usesPerfect matchings of a sequence of arrivals · Deterministic online bipartite matching algorithm · Number of arrivals an online matcher matches
Proof usesNo deterministic online bipartite matching algorithm beats 1/2
Used byNo deterministic online matcher beats ratio \(1/2\), with any additive constant

TheoremNo deterministic online matcher beats ratio \(1/2\), with any additive constant#✓fully proved

Let \((A_n)_{n \in \mathbb{N}}\) be a family of online matchers, \(A_n\) having \(2n\) left vertices, and let \(b\), \(c\), \(d\) be natural numbers with \(d < 2c\). Then for some \(n\) there are a sequence \(\sigma\) of arrivals on the left vertices of \(A_n\) and a perfect matching \(m\) of \(\sigma\) such that \(d \cdot \mathrm{ALG} + b < c \cdot |m|\), where \(\mathrm{ALG}\) is the number of arrivals of \(\sigma\) that \(A_n\) matches when run from the empty history with no left vertex matched, and \(|m|\) is the length of \(m\).

For \(d > 0\) this says that the family is not \(c/d\)-competitive, whatever the additive constant.

theorem not_competitive (A : ∀ n, OnlineMatcher (2 * n)) {c d : ℕ} (hcd : d < 2 * c) (b : ℕ) :
    ∃ n σ m, IsPerfect σ m ∧ d * matched (A n) [] [] σ + b < c * m.length
Uses 4
Statement usesPerfect matchings of a sequence of arrivals · Deterministic online bipartite matching algorithm · Number of arrivals an online matcher matches
Proof usesFinite-size lower bound for deterministic online matching
28 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.