Open Research Index

Dependent finite mixed Nash equilibria in Lean

Arthur Freitas Ramos

Palomar Registrypalomar/PALOMAR-2026-09-07-000014Sep 7, 2026math.LOscore 0

A Lean-native formalization of finite mixed Nash equilibrium for games in which each player has its own finite, nonempty action type. The library defines dependent profiles and finite expected payoffs, proves support equalization and Dirac transport, establishes the closed/compact/convex mixed-profile geometry, and connects the normalized excess map to a checked product-of-simplices Brouwer theorem. It also proves the correspondence between ambient finite games with player-indexed legal action sets and dependent legal-action subtypes. This is a reusable formalization artifact, not a claim of…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-07-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000014/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-07-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'