Proposition 6.4 — Hall's theorem with a bounded deficit

Proved

YogeshwaranDM.deficient_hall_matching

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

graph-theoryhall-theoremmatchings

Proposition 6.4 — Hall's theorem with a bounded deficit. Let $G$ be a finite simple bipartite graph with vertex partition $L\sqcup R$ , and let $d\in\mathbb N$ satisfy $d\ge1$ . Suppose

\forall S\subseteq L,\qquad |N_G(S)|\ge |S|-d.

Then $G$ contains a matching $M$ for which

|E(M)|\ge |L|-d.

Formalization note. Quantification over finite subsets of the finite subtype $L$ covers every left subset. Natural subtraction is truncated at zero, which is equivalent here to the integer lower bound because edge and neighborhood cardinalities are nonnegative. The conclusion counts actual unordered edges of a native matching subgraph.

Preamble

import Mathlib.Combinatorics.SimpleGraph.Hall
import Mathlib.Data.Finset.Sum
import Mathlib.Tactic

set_option autoImplicit false

Formal statement

namespace YogeshwaranDM

theorem deficient_hall_matching {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [G.LocallyFinite] (L R : Set V)
    (hG : G.IsBipartiteWith L R) (hcover : L ∪ R = Set.univ)
    (d : ℕ) (hd : 1 ≤ d)
    (h : ∀ S : Finset L, S.card - d ≤ (S.biUnion (fun x => G.neighborFinset x)).card) :
    ∃ M : G.Subgraph, M.IsMatching ∧ L.ncard - d ≤ M.edgeSet.ncard := by sorry

end YogeshwaranDM

Source

D. Yogeshwaran, Discrete Mathematics—Lecture Notes, Indian Statistical Institute Bangalore, HTML edition generated May 9, 2025, Proposition 6.4, https://www.isibang.ac.in/~d.yogesh/Course_Notes/DM1/Ch6.S1.html

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

For every finite type $V$ equipped with a finite enumeration and decidable equality, every simple undirected loopless graph $G$ on $V$ equipped with finite enumerations of all its neighbor sets, every pair of sets $L,R \subseteq V$ , and every natural number $d$ , assume that $L$ and $R$ are disjoint, every edge of $G$ has one endpoint in each part, $L \cup R=V$ , and $1 \leq d$ . Assume also that, for every finite set $S$ of elements of $L$ , $\max(|S|-d,0) \leq |N_G(S)|$ , where $N_G(S)$ is the finite union of the sets of neighbors in $G$ of the vertices belonging to $S$ . Then there exists a subgraph $M$ of $G$ such that every vertex in the vertex set of $M$ has exactly one neighbor in $M$ , and $\max(|L|-d,0) \leq |E(M)|$ . Here a subgraph chooses a vertex set and some of the edges of $G$ , with both endpoints of every chosen edge in that vertex set; $E(M)$ is its set of unordered edges, so each edge is counted once, rather than once per orientation or endpoint. All finite sets contain distinct elements, and a vertex appearing in several of the neighbor sets is counted only once in their union. Both subtractions in the formal assertion are subtraction in the natural numbers, truncated at zero; the expressions with $\max$ denote this convention. The cardinalities of $L$ and $E(M)$ are natural-number set cardinalities, while the other cardinalities count finite sets; all are ordinary finite counts because $V$ is finite, so the general zero value of natural-number cardinality on infinite sets is not used. The conclusion is an existence assertion and imposes no further requirement of uniqueness, maximality, or that $M$ contain every vertex of $L$ or $R$ . Empty $V$ , empty parts, and the empty choice of $S$ are included. The empty choice of $S$ gives $0 \leq 0$ . If $d \geq |L|$ , every assumed cardinality inequality is automatic and the empty subgraph satisfies the conclusion. In particular, this applies when $L$ is empty. The value $d=0$ and infinite vertex types are outside the hypotheses.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph