§8.6, p. 182 — ν(F) ≤ ν*(F) = τ*(F) ≤ τ(F) for every finite set system
ProvedMatousekLP.DIntervals.fractional_matching_eq_fractional_transversalLet be a finite set and a system of nonempty subsets of . Then the fractional transversal LP and the fractional matching LP of both have optimal solutions and , their optimal values agree, and they sit between the matching and transversal numbers:
Here is the minimum total weight of a fractional transversal and the maximum total weight of a fractional matching.
The equality is the linear-programming duality between the two relaxations; it is the step in the proof of Lemma 8.6.3 that turns a bound on fractional matchings of -intervals into a fractional transversal of small weight.
Formalization Note The statement asserts the existence of a fractional transversal and a fractional matching such that is optimal (its objective is that of every fractional transversal), is optimal, and ; this is the book's chain with , written as attained optima rather than as possibly empty infima and suprema. The book states the chain "always"; the members of are assumed nonempty, which the book tacitly assumes as well: if there is no transversal ( undefined), the fractional transversal LP is infeasible and the fractional matching LP is unbounded.
import Mathlib import Definitions.Def_MatousekLP_DIntervals_SetSystem open Finset
namespace MatousekLP.DIntervals
/-- §8.6, p. 182: for a finite set system `F` on a finite set `V` whose members are nonempty,
the fractional transversal LP and the fractional matching LP both have optimal solutions `x`,
`y` with the same objective value, `ν*(F) = τ*(F)`, and
`ν(F) ≤ ν*(F) = τ*(F) ≤ τ(F)`. -/
theorem fractional_matching_eq_fractional_transversal {V : Type*} [Fintype V] [DecidableEq V]
(F : Finset (Finset V)) (hF : ∀ S ∈ F, S.Nonempty) :
∃ (x : V → ℝ) (y : Finset V → ℝ),
IsFractionalTransversal F x ∧ IsFractionalMatching F y ∧
(∀ x' : V → ℝ, IsFractionalTransversal F x' → ∑ v, x v ≤ ∑ v, x' v) ∧
(∀ y' : Finset V → ℝ, IsFractionalMatching F y' → ∑ S ∈ F, y' S ≤ ∑ S ∈ F, y S) ∧
(matchingNumber F : ℝ) ≤ ∑ S ∈ F, y S ∧
∑ S ∈ F, y S = ∑ v, x v ∧
∑ v, x v ≤ (transversalNumber F : ℝ) := by sorry
end MatousekLP.DIntervals
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.