GameTheory-5b — Théorème minimax de von Neumann (companion formel natif)

Ce notebook est le companion formel du lake minimax_lean, dont la lib Minimax prouve le théorème minimax de von Neumann (1928) pour les jeux finis à somme nulle — via le minimax de Sion (Mathlib Topology.Sion) — avec zéro sorry.

\[\max_x \min_y\, x^{T} A\, y \;=\; \min_y \max_x\, x^{T} A\, y\]

(x parcourt le simplexe des stratégies mixtes du joueur-ligne, y celui du joueur-colonne, A est la matrice de gains m × n).

Convention de vérification — #check natif dans le kernel Lean

Ce notebook est un notebook Lean natif (kernel lean4-wsl) : il importe le lake directement et le compilateur Lean rend les signatures dans le notebook. C’est rendu possible par l’UNLOCK (patch lean4_jupyter + jonction Mathlib #2611).

⚠️ À l’exécution, la première cellule (import) peut prendre ~3 min : le kernel charge les oleans Mathlib via la jonction NTFS. Les suivantes sont instantanées.

1. Import des modules du lake minimax_lean

Le lake minimax_lean est structuré en modules (ZeroSum, Concavity, SionApplication) sous le namespace MinimaxLean. On importe les modules (l’umbrella racine n’est pas buildée par la config submodules du lake — on cible donc directement les modules qui portent les définitions).

import Minimax.ZeroSum
import Minimax.Concavity
import Minimax.SionApplication
open MinimaxLean

import Minimax.ZeroSum

import Minimax.Concavity

import Minimax.SionApplication

open MinimaxLean

--% env 0

Raw input

{"cmd": "import Minimax.ZeroSum\nimport Minimax.Concavity\nimport Minimax.SionApplication\nopen MinimaxLean"}

Raw output

{"env": 0}

2. Preuve sans sorry — #print axioms

Le théorème phare exists_saddle_point_payoff ne dépend que des 3 axiomes standards de Lean (propext, Classical.choice, Quot.sound) — pas de sorryAx — ce qui prouve que la preuve est complète (0 sorry).

#print axioms MinimaxLean.exists_saddle_point_payoff

#print axioms MinimaxLean.exists_saddle_point_payoff
 'MinimaxLean.exists_saddle_point_payoff' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 1

Raw input

{"cmd": "#print axioms MinimaxLean.exists_saddle_point_payoff", "env": 0}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "'MinimaxLean.exists_saddle_point_payoff' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 1}

3. Matrice de gains, stratégies mixtes, payoff bilinéaire

Le module Minimax/ZeroSum.lean pose le cadre combinatoire :

• PayoffMatrix m n = Matrix m n ℝ — les gains du joueur-ligne (\(A_{ij}\) quand \(i\) joue ligne \(i\), \(j\) colonne \(j\)).
• payoff A x y = Σ_{(i,j)} x_i · A_{ij} · y_j — le payoff espéré bilinéaire sous les stratégies mixtes \(x\) (lignes) et \(y\) (colonnes).

La représentation comme somme unique sur le produit \(m × n\) rend la bilinéarité immédiate (sum_add_distrib / sum_mul en une étape), et la continuité découle de la continuité des opérations algébriques sur ℝ.

#check PayoffMatrix
#check payoff
#check payoff_add_in_x
#check continuous_payoff_in_x

#check PayoffMatrix
 MinimaxLean.PayoffMatrix.{u_3, u_4} (m : Type u_3) (n : Type u_4) : Type (max u_3 u_4)

#check payoff
 MinimaxLean.payoff.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : PayoffMatrix m n) (x : m → ℝ)
  (y : n → ℝ) : ℝ

#check payoff_add_in_x
 MinimaxLean.payoff_add_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : PayoffMatrix m n)
  (x x' : m → ℝ) (y : n → ℝ) : payoff A (x + x') y = payoff A x y + payoff A x' y

#check continuous_payoff_in_x
 MinimaxLean.continuous_payoff_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]
  (A : PayoffMatrix m n) (y : n → ℝ) : Continuous fun x => payoff A x y

--% env 2

Raw input

{"cmd": "#check PayoffMatrix\n#check payoff\n#check payoff_add_in_x\n#check continuous_payoff_in_x", "env": 1}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "MinimaxLean.PayoffMatrix.{u_3, u_4} (m : Type u_3) (n : Type u_4) : Type (max u_3 u_4)"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "MinimaxLean.payoff.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : PayoffMatrix m n) (x : m → ℝ)\n (y : n → ℝ) : ℝ"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "MinimaxLean.payoff_add_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : PayoffMatrix m n)\n (x x' : m → ℝ) (y : n → ℝ) : payoff A (x + x') y = payoff A x y + payoff A x' y"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "MinimaxLean.continuous_payoff_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]\n (A : PayoffMatrix m n) (y : n → ℝ) : Continuous fun x => payoff A x y"}], "env": 2}

Lecture : bilinéarité et continuité du payoff

Symbole Lean	Lecture
PayoffMatrix m n	\(A \in \mathbb{R}^{m \times n}\), matrice de gains
payoff A x y	\(\sum_{i,j} x_i A_{ij} y_j\), espérance du gain
payoff_add_in_x	additivité en \(x\) (moitié de la linéarité)
continuous_payoff_in_x	continuité en \(x\) (borne pour la semi-continuité)

4. Concavité, convexité et les quatre hypothèses de Sion

Le module Minimax/Concavity.lean déroule le glue analytique : du payoff bilinéaire, on dérive les quatre hypothèses exigées par Sion.exists_isSaddlePointOn' (Mathlib Topology.Sion) :

• quasi-convexité en \(x\) : payoff_quasiconvex_in_x (via ConvexOn.quasiconvexOn),
• quasi-concavité en \(y\) : payoff_quasiconcave_in_y (via ConcaveOn.quasiconcaveOn),
• semi-continuité inf. en \(x\) : payoff_lowerSemicontinuous_in_x,
• semi-continuité sup. en \(y\) : payoff_upperSemicontinuous_in_y.

Une fonction affine est à la fois concave et convexe (Jensen avec égalité), et la continuité entraîne les deux semi-continuités.

#check payoff_concave_in_x
#check payoff_quasiconvex_in_x
#check payoff_quasiconcave_in_y
#check payoff_lowerSemicontinuous_in_x
#check payoff_upperSemicontinuous_in_y

#check payoff_concave_in_x
 MinimaxLean.payoff_concave_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : PayoffMatrix m n)
  (y : n → ℝ) : ConcaveOn ℝ (stdSimplex ℝ m) fun x => payoff A x y

#check payoff_quasiconvex_in_x
 MinimaxLean.payoff_quasiconvex_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]
  (A : PayoffMatrix m n) (y : n → ℝ) : QuasiconvexOn ℝ (stdSimplex ℝ m) fun x => payoff A x y

#check payoff_quasiconcave_in_y
 MinimaxLean.payoff_quasiconcave_in_y.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]
  (A : PayoffMatrix m n) (x : m → ℝ) : QuasiconcaveOn ℝ (stdSimplex ℝ n) fun y => payoff A x y

#check payoff_lowerSemicontinuous_in_x
 MinimaxLean.payoff_lowerSemicontinuous_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]
  (A : PayoffMatrix m n) (y : n → ℝ) : LowerSemicontinuousOn (fun x => payoff A x y) (stdSimplex ℝ m)

#check payoff_upperSemicontinuous_in_y
 MinimaxLean.payoff_upperSemicontinuous_in_y.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]
  (A : PayoffMatrix m n) (x : m → ℝ) : UpperSemicontinuousOn (fun y => payoff A x y) (stdSimplex ℝ n)

--% env 3

Raw input

{"cmd": "#check payoff_concave_in_x\n#check payoff_quasiconvex_in_x\n#check payoff_quasiconcave_in_y\n#check payoff_lowerSemicontinuous_in_x\n#check payoff_upperSemicontinuous_in_y", "env": 2}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "MinimaxLean.payoff_concave_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] (A : PayoffMatrix m n)\n (y : n → ℝ) : ConcaveOn ℝ (stdSimplex ℝ m) fun x => payoff A x y"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "MinimaxLean.payoff_quasiconvex_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]\n (A : PayoffMatrix m n) (y : n → ℝ) : QuasiconvexOn ℝ (stdSimplex ℝ m) fun x => payoff A x y"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "MinimaxLean.payoff_quasiconcave_in_y.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]\n (A : PayoffMatrix m n) (x : m → ℝ) : QuasiconcaveOn ℝ (stdSimplex ℝ n) fun y => payoff A x y"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "MinimaxLean.payoff_lowerSemicontinuous_in_x.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]\n (A : PayoffMatrix m n) (y : n → ℝ) : LowerSemicontinuousOn (fun x => payoff A x y) (stdSimplex ℝ m)"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "MinimaxLean.payoff_upperSemicontinuous_in_y.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n]\n (A : PayoffMatrix m n) (x : m → ℝ) : UpperSemicontinuousOn (fun y => payoff A x y) (stdSimplex ℝ n)"}], "env": 3}

Lecture : du bilinéaire aux quatre hypothèses de Sion

Théorème	Conclusion	Rôle dans Sion
payoff_concave_in_x	ConcaveOn ℝ (stdSimplex ℝ m) (· ↦ payoff A · y)	affine ⟹ concave
payoff_quasiconvex_in_x	QuasiconvexOn …	hyp hfy'
payoff_quasiconcave_in_y	QuasiconcaveOn …	hyp hfx'
payoff_lowerSemicontinuous_in_x	LowerSemicontinuousOn …	hyp hfy
payoff_upperSemicontinuous_in_y	UpperSemicontinuousOn …	hyp hfx

5. Théorème phare : existence du point-selle (von Neumann)

Le module Minimax/SionApplication.lean câble les 4 hyps analytiques avec les faits topologiques de Mathlib sur stdSimplex (compacité, convexité, non-vacuité) pour conclure via Sion.exists_isSaddlePointOn : il existe un point-selle \((a, b) \in \mathrm{stdSimplex}(\mathbb{R}, m) \times \mathrm{stdSimplex}(\mathbb{R}, n)\).

C’est exactement le théorème minimax de von Neumann : les stratégies mixtes optimales existent, et la valeur du jeu vérifie l’égalité minimax.

#check stdSimplex_nonempty_m
#check MinimaxLean.exists_saddle_point_payoff

#check stdSimplex_nonempty_m
 MinimaxLean.stdSimplex_nonempty_m.{u_1} {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] :
  (stdSimplex ℝ m).Nonempty

#check MinimaxLean.exists_saddle_point_payoff
 MinimaxLean.exists_saddle_point_payoff.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq m]
  [DecidableEq n] [Nonempty m] [Nonempty n] (A : PayoffMatrix m n) :
  ∃ a ∈ stdSimplex ℝ m, ∃ b ∈ stdSimplex ℝ n, IsSaddlePointOn (stdSimplex ℝ m) (stdSimplex ℝ n) (payoff A) a b

--% env 4

Raw input

{"cmd": "#check stdSimplex_nonempty_m\n#check MinimaxLean.exists_saddle_point_payoff", "env": 3}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "MinimaxLean.stdSimplex_nonempty_m.{u_1} {m : Type u_1} [Fintype m] [DecidableEq m] [Nonempty m] :\n (stdSimplex ℝ m).Nonempty"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "MinimaxLean.exists_saddle_point_payoff.{u_1, u_2} {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] [DecidableEq m]\n [DecidableEq n] [Nonempty m] [Nonempty n] (A : PayoffMatrix m n) :\n ∃ a ∈ stdSimplex ℝ m, ∃ b ∈ stdSimplex ℝ n, IsSaddlePointOn (stdSimplex ℝ m) (stdSimplex ℝ n) (payoff A) a b"}], "env": 4}

Lecture : le câblage final vers von Neumann

exists_saddle_point_payoff fournit ∃ a ∈ stdSimplex ℝ m, ∃ b ∈ stdSimplex ℝ n, IsSaddlePointOn (stdSimplex ℝ m) (stdSimplex ℝ n) (payoff A) a b. Le point-selle \((a, b)\) réalise simultanément le maximum en \(x\) et le minimum en \(y\) : c’est l’égalité \(\max_x \min_y x^T A y = \min_y \max_x x^T A y\).

6. La chaîne causale complète

Les modules composent une chaîne unique, de la bilinéarité au point-selle :

1. ZeroSum — payoff bilinéaire (\(\sum_{i,j} x_i A_{ij} y_j\)) + continuité.
2. Concavity — du bilinéaire aux 4 hyps de Sion (quasi-convexité/concavité + semi-continuités).
3. SionApplication — câblage avec stdSimplex (compact convexe non vide) + Sion.exists_isSaddlePointOn ⟹ point-selle ⟹ von Neumann.

7. Exercices

Exercice 1 — Valeur d’un jeu à point-selle pur (Python)

Avant le formalisme, ancrez l’intuition : pour une matrice \(A\) qui admet un point-selle pur (une entrée qui est à la fois le max de sa colonne et le min de sa ligne), la valeur du jeu est cette entrée. Complétez la fonction (en Python, hors du kernel Lean).

def pure_saddle_value(A):
    # TODO etudiant : pour chaque entree A[i][j], verifier si elle est
    # le min de sa ligne ET le max de sa colonne. Retourner sa valeur.
    return None  # TODO

Exercice 2 — Homogénéité du payoff en \(y\)

Le payoff est homogène en \(y\) : payoff A x (c • y) = c * payoff A x y. Formalisez cette linéarité (sur papier puis tentez en Lean).

-- TODO etudiant : formaliser payoff_smul_in_y
-- example (A : PayoffMatrix m n) (c : ℝ) (x : m → ℝ) (y : n → ℝ) :
--     payoff A x (c • y) = c * payoff A x y := by sorry

Exercice 3 — Un jeu sans point-selle pur

Le jeu pierre-feuille-ciseaux (matrice antisymétrique) n’a pas de point-selle pur : il faut des stratégies mixtes. Donnez la matrice et justifiez (sur papier) pourquoi aucune entrée n’est simultanément max de colonne et min de ligne.

# TODO etudiant : matrice RPS 3x3 + justification (markdown) de l'absence de point-selle pur

Conclusion

Ce companion natif exhibe la preuve formelle 0-sorry du théorème minimax de von Neumann dans le kernel Lean lui-même : #check et #print axioms rendent les signatures et les axiomes réels produits par le compilateur, sans intermédiaire Python.

La sensitivity conjecture de Huang a son companion natif ; ici c’est le minimax de von Neumann (1928) — l’un des résultats fondateurs de la théorie des jeux — qui est formellement résolu via le minimax de Sion.

Jalon ouvert : l’unicité de la valeur du jeu (et son calcul explicite sur une matrice donnée) n’est pas formalisée dans le lake ; la lib reste sorry-free.