Matchings, outside options and pairwise stability
DefinitionAMLGS62_AppliedModelingLib_Markets_Matching_Basicaml-gs62-stable-marriage-20260915game-theorystable-matching
For sets , a matching consists of optional partner maps and satisfying
Real-valued preferences extend to unmatched outcomes with value zero. Stability requires that each assigned outcome has nonnegative value for its participant and that no pair would strictly improve both participants' values. The bundle also defines reversal of the two sides. These are the matching objects and comparison predicates used throughout the existence proof.
Definition code
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Real.Basic
namespace AppliedModelingLib
namespace Matching
/-- A matching between Men and Women. -/
structure Assignment (M W : Type*) where
m_match : M → Option W
w_match : W → Option M
consistent_m : ∀ m w, m_match m = some w ↔ w_match w = some m
namespace Assignment
/-- Swap the two sides of a matching. -/
def swap {M W : Type*} (mu : Assignment M W) : Assignment W M where
m_match := mu.w_match
w_match := mu.m_match
consistent_m w m := (mu.consistent_m m w).symm
end Assignment
/-- The value of a match for a man. 0 if unmatched. -/
def valM {M W : Type*} (val : M → W → ℝ) (m : M) (w : Option W) : ℝ :=
match w with
| none => 0
| some w' => val m w'
/-- The value of a match for a woman. 0 if unmatched. -/
def valW {M W : Type*} (val : W → M → ℝ) (w : W) (m : Option M) : ℝ :=
match m with
| none => 0
| some m' => val w m'
/-- A matching is stable if it is individually rational and admits no blocking pairs. -/
def IsStable {M W : Type*} (val_m : M → W → ℝ) (val_w : W → M → ℝ) (mu : Assignment M W) : Prop :=
(∀ m, 0 ≤ valM val_m m (mu.m_match m)) ∧
(∀ w, 0 ≤ valW val_w w (mu.w_match w)) ∧
(∀ m w, valM val_m m (mu.m_match m) < val_m m w →
valW val_w w (mu.w_match w) < val_w w m → False)
end Matching
end AppliedModelingLib
Source