Applicant-optimal college assignment predicate

Definition

AMLGS62Rest_GS62CollegeAdmissions_SourceModel

by nkgarg · Sep 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

aml-gs62-stable-marriage-20260915college-admissionsgame-theorystable-matching

The predicate holds of a college assignment $\mu$ exactly when $\mu$ respects the college quotas, is individually rational, has no blocking applicant–college pair (including acceptable vacancies), and every applicant weakly prefers $\mu$ to every stable assignment in the same market. Unassigned applicants have value zero. This is the source-facing abbreviation for the college applicant-optimality predicate.

Definition code

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Lattice.Basic
import Mathlib.Data.Finset.Max
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.EquivFin
import Mathlib.Data.Fintype.Option
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Fintype.Sort
import Mathlib.Data.Prod.Lex
import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceCompletion

namespace GS62CollegeAdmissions
namespace PaperInterface

open AppliedModelingLib.Matching

/-- Applicant optimality under the completed standard convention. -/
def applicantOptimalCollegeAssignment {Applicants Colleges : Type*}
    (quota : Colleges → ℕ)
    (val_applicant : Applicants → Colleges → ℝ)
    (val_college : Colleges → Applicants → ℝ)
    (mu : ManyToOneAssignment Applicants Colleges) : Prop :=
  gs_applicant_optimal_college_assignment quota val_applicant val_college mu

end PaperInterface
end GS62CollegeAdmissions

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/SourceModel.lean#L105-L111

View graph