GameTheory 4b - Theoreme d’Existence de Nash (Lean)

Navigation : << 4-NashEquilibrium (track principal)) | Index

Autrès side tracks : 4c-NashExistence-Python

Companion Python : GameTheory-04c-NashExistence-Python

Kernel : Lean 4 (WSL)

Introduction

Ce notebook formalise en Lean 4 le celebre theoreme d’existence de Nash (1950) :

Tout jeu fini possede au moins un équilibre de Nash en stratégies mixtes.

La preuve repose sur le theoreme du point fixe de Brouwer, un résultat fondamental de topologie.

Objectifs d’apprentissage

  1. Formaliser le theoreme de Brouwer en Lean
  2. Définir les structures de jeu et stratégies mixtes
  3. Enoncer et comprendre la preuve d’existence
  4. Explorer les extensions (Kakutani, produit de simplexes)

Prerequis

  • Avoir complète le notebook GameTheory-02b-Lean-Definitions-Lean (définitions de base)
  • Notions de topologie (continuite, compacite, convexite)
  • Familiarite avec les tactiques Lean

Duree estimee : 55 minutes

Plan de ce Notebook

  1. Le Simplexe Standard
  2. Theoreme de Brouwer
  3. Definitions de Jeu
  4. Meilleure Reponse et Nash
  5. Structure de la Preuve
  6. Exemples guides
  7. Corrections – Reference enseignant
  8. Resume

## 1. Le Simplexe Standard

Le simplexe standard de dimension \(n-1\) est l’ensemble des distributions de probabilité sur \(n\) éléments :

\[\Delta^{n-1} = \{(x_1, ..., x_n) \in \mathbb{R}^n : x_i \geq 0, \sum_i x_i = 1\}\]

C’est un ensemble compact et convexe.

-- Definition du simplexe standard

-- Version avec Float (simplifiee)
def Simplex (n : Nat) : Type := 
  { v : Fin n → Float // 
    (∀ i, v i >= 0) ∧ 
    (List.finRange n).foldl (fun acc i => acc + v i) 0 = 1 }

#check Simplex 3
-- Definition du simplexe standard
-- Version avec Float (simplifiee)
def Simplex (n : Nat) : Type := 
  { v : Fin n → Float // 
    (∀ i, v i >= 0) ∧ 
    (List.finRange n).foldl (fun acc i => acc + v i) 0 = 1 }
 Simplex 3 : Type
--% env 0
Raw input {"cmd": "-- Definition du simplexe standard\n\n-- Version avec Float (simplifiee)\ndef Simplex (n : Nat) : Type := \n { v : Fin n \u2192 Float // \n (\u2200 i, v i >= 0) \u2227 \n (List.finRange n).foldl (fun acc i => acc + v i) 0 = 1 }\n\n#check Simplex 3"}
Raw output {"messages": [{"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "Simplex 3 : Type"}], "env": 0}

Interpretation

La définition du simplexe utilise un sous-type Lean : { v : Fin n -> Float // P v } représente les vecteurs v satisfaisant la propriete P.

Decomposition de la définition :

Composante Expression Signification
Support Fin n -> Float Vecteur de n coordonnees
Non-negativite forall i, v i >= 0 Toutes les coordonnees sont positives ou nulles
Normalisation foldl (+) 0 = 1 La somme des coordonnees vaut 1

Exemple : Simplex 3 contient les triplets (p1, p2, p3) tels que : - p1, p2, p3 >= 0 - p1 + p2 + p3 = 1

Ce sont les distributions de probabilité sur 3 éléments.

Choix technique : L’utilisation de Float au lieu de Rat ou d’un type réel formel simplifie les calculs mais limite les preuves formelles (pas d’arithmetique decidable sur Float).

-- Proprietes du simplexe : convexite

-- Une combinaison convexe de points du simplexe reste dans le simplexe
def convexCombination (n : Nat) (x y : Fin n → Float) (t : Float) : Fin n → Float :=
  fun i => t * x i + (1 - t) * y i

-- Propriete : le simplexe est convexe
-- Si x, y ∈ Δ et λ ∈ [0,1], alors tx + (1-λ)y ∈ Δ
def inSimplex (n : Nat) (v : Fin n → Float) : Prop :=
  (∀ i, v i >= 0) ∧ (List.finRange n).foldl (fun acc i => acc + v i) 0 = 1

-- Enonce (la preuve necessite de l'arithmetique sur Float)
theorem simplex_convex (n : Nat) (x y : Fin n → Float) (t : Float)
    (hx : inSimplex n x) (hy : inSimplex n y)
    (ht : 0 <= t ∧ t <= 1) :
    inSimplex n (convexCombination n x y t) := by
  constructor
  · -- Non-negativite : λ*x_i + (1-λ)*y_i >= 0
    intro i
    sorry  -- Necessite arithmetique sur Float
  · -- Somme = 1
    sorry

#check simplex_convex
-- Proprietes du simplexe : convexite
-- Une combinaison convexe de points du simplexe reste dans le simplexe
def convexCombination (n : Nat) (x y : Fin n → Float) (t : Float) : Fin n → Float :=
  fun i => t * x i + (1 - t) * y i
-- Propriete : le simplexe est convexe
-- Si x, y ∈ Δ et λ ∈ [0,1], alors tx + (1-λ)y ∈ Δ
def inSimplex (n : Nat) (v : Fin n → Float) : Prop :=
  (∀ i, v i >= 0) ∧ (List.finRange n).foldl (fun acc i => acc + v i) 0 = 1
-- Enonce (la preuve necessite de l'arithmetique sur Float)
🟨 declaration uses `sorry`
    (hx : inSimplex n x) (hy : inSimplex n y)
    (ht : 0 <= t ∧ t <= 1) :
    inSimplex n (convexCombination n x y t) := by
  constructor
  · -- Non-negativite : λ*x_i + (1-λ)*y_i >= 0
    intro i
    sorry  -- Necessite arithmetique sur Float
  · -- Somme = 1
    sorry
 simplex_convex (n : Nat) (x y : Fin n → Float) (t : Float) (hx : inSimplex n x) (hy : inSimplex n y)
  (ht : 0 ≤ t ∧ t ≤ 1) : inSimplex n (convexCombination n x y t)
--% env 1
--% prove 1
Raw input {"cmd": "-- Proprietes du simplexe : convexite\n\n-- Une combinaison convexe de points du simplexe reste dans le simplexe\ndef convexCombination (n : Nat) (x y : Fin n \u2192 Float) (t : Float) : Fin n \u2192 Float :=\n fun i => t * x i + (1 - t) * y i\n\n-- Propriete : le simplexe est convexe\n-- Si x, y \u2208 \u0394 et \u03bb \u2208 [0,1], alors tx + (1-\u03bb)y \u2208 \u0394\ndef inSimplex (n : Nat) (v : Fin n \u2192 Float) : Prop :=\n (\u2200 i, v i >= 0) \u2227 (List.finRange n).foldl (fun acc i => acc + v i) 0 = 1\n\n-- Enonce (la preuve necessite de l'arithmetique sur Float)\ntheorem simplex_convex (n : Nat) (x y : Fin n \u2192 Float) (t : Float)\n (hx : inSimplex n x) (hy : inSimplex n y)\n (ht : 0 <= t \u2227 t <= 1) :\n inSimplex n (convexCombination n x y t) := by\n constructor\n \u00b7 -- Non-negativite : \u03bb*x_i + (1-\u03bb)*y_i >= 0\n intro i\n sorry -- Necessite arithmetique sur Float\n \u00b7 -- Somme = 1\n sorry\n\n#check simplex_convex", "env": 0}
Raw output {"sorries": [{"proofState": 0, "pos": {"line": 20, "column": 4}, "goal": "case left\nn : Nat\nx y : Fin n → Float\nt : Float\nhx : inSimplex n x\nhy : inSimplex n y\nht : 0 ≤ t ∧ t ≤ 1\ni : Fin n\n⊢ convexCombination n x y t i ≥ 0", "endPos": {"line": 20, "column": 9}}, {"proofState": 1, "pos": {"line": 22, "column": 4}, "goal": "case right\nn : Nat\nx y : Fin n → Float\nt : Float\nhx : inSimplex n x\nhy : inSimplex n y\nht : 0 ≤ t ∧ t ≤ 1\n⊢ List.foldl (fun acc i => acc + convexCombination n x y t i) 0 (List.finRange n) = 1", "endPos": {"line": 22, "column": 9}}], "messages": [{"severity": "warning", "pos": {"line": 13, "column": 8}, "endPos": {"line": 13, "column": 22}, "data": "declaration uses `sorry`"}, {"severity": "info", "pos": {"line": 24, "column": 0}, "endPos": {"line": 24, "column": 6}, "data": "simplex_convex (n : Nat) (x y : Fin n → Float) (t : Float) (hx : inSimplex n x) (hy : inSimplex n y)\n (ht : 0 ≤ t ∧ t ≤ 1) : inSimplex n (convexCombination n x y t)"}], "env": 1}

Interpretation : Convexite du simplexe

Le theoreme simplex_convex enonce formellement que le simplexe est convexe : si \(x, y \in \Delta^{n-1}\) et \(\lambda \in [0,1]\), alors \(\lambda x + (1-\lambda)y \in \Delta^{n-1}\).

Les deux sous-objectifs de la preuve :

Objectif But a prouver Statut
Non-negativite \(\lambda x_i + (1-\lambda) y_i \geq 0\) sorry – necessite arithmetique sur Float
Normalisation \(\sum_i (\lambda x_i + (1-\lambda) y_i) = 1\) sorry – necessite linearite de la somme

La preuve complète sera donnee en Section 7 (Correction Exemple guide 1). Les deux sorry refletent une limitation technique de Lean 4 : l’absence d’arithmetique decidable sur le type Float.

L’importance de la convexite : La convexite du simplexe est l’une des trois hypotheses fondamentales du theoreme de Brouwer (compact, convexe, non vide). Sans convexite, le theoreme ne s’applique pas et l’existence de Nash n’est pas garantie.

## 2. Theoreme du Point Fixe de Brouwer

Enonce

Theoreme de Brouwer (1911) : Soit \(f : K \to K\) une fonction continue ou \(K\) est un compact convexe non vide de \(\mathbb{R}^n\). Alors \(f\) admet au moins un point fixe \(x^*\) tel que \(f(x^*) = x^*\).

Intuition

Imaginez une carte de France posee sur la France réelle. Si vous deformez la carte de manière continue (sans la dechirer), au moins un point de la carte reste exactement au-dessus de sa position réelle.

-- Theoreme de Brouwer sur le simplexe (axiomatise)

-- La preuve complete utilise le lemme de Sperner et le lemme de Scarf
-- Voir: https://github.com/math-xmum/Brouwer

-- Nous axiomatisons le theoreme pour ce notebook
axiom brouwer_simplex {n : Nat} (f : Simplex n → Simplex n) 
    (hcont : True)  -- condition de continuite (simplifiee)
    : ∃ x : Simplex n, f x = x

#check @brouwer_simplex
-- Theoreme de Brouwer sur le simplexe (axiomatise)
-- La preuve complete utilise le lemme de Sperner et le lemme de Scarf
-- Voir: https://github.com/math-xmum/Brouwer
-- Nous axiomatisons le theoreme pour ce notebook
axiom brouwer_simplex {n : Nat} (f : Simplex n → Simplex n) 
    (hcont : True)  -- condition de continuite (simplifiee)
    : ∃ x : Simplex n, f x = x
 @brouwer_simplex : ∀ {n : Nat} (f : Simplex n → Simplex n), True → ∃ x, f x = x
--% env 2
Raw input {"cmd": "-- Theoreme de Brouwer sur le simplexe (axiomatise)\n\n-- La preuve complete utilise le lemme de Sperner et le lemme de Scarf\n-- Voir: https://github.com/math-xmum/Brouwer\n\n-- Nous axiomatisons le theoreme pour ce notebook\naxiom brouwer_simplex {n : Nat} (f : Simplex n \u2192 Simplex n) \n (hcont : True) -- condition de continuite (simplifiee)\n : \u2203 x : Simplex n, f x = x\n\n#check @brouwer_simplex", "env": 1}
Raw output {"messages": [{"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "@brouwer_simplex : ∀ {n : Nat} (f : Simplex n → Simplex n), True → ∃ x, f x = x"}], "env": 2}

Interpretation

Le theoreme de Brouwer est axiomatise dans ce notebook car sa preuve complète est complexe et disponible dans des formalisations dediees.

Pourquoi axiomatiser ? - La preuve de Brouwer utilise le lemme de Sperner (combinatoire) ou des techniques d’homologie (topologie algebrique) - Le depot math-xmum/Brouwer fournit une formalisation complète en Lean 4

Lecture de l’axiome :

axiom brouwer_simplex {n : Nat} (f : Simplex n -> Simplex n) 
    (hcont : True) : exists x : Simplex n, f x = x
Composante Signification
f : Simplex n -> Simplex n Fonction du simplexe vers lui-même
hcont : True Placeholder pour la condition de continuite (simplifiee)
exists x, f x = x Il existe un point fixe

Limitation : La condition hcont : True est une simplification. Dans une formalisation rigoureuse, il faudrait utiliser la topologie de Mathlib pour exprimer la continuite.

-- Extension au produit de simplexes

-- Pour Nash, on a besoin du theoreme sur un produit de simplexes
-- (un simplexe par joueur)

def SimplexProduct (n : Nat) (actions : Fin n → Nat) : Type :=
  (i : Fin n) → Simplex (actions i)

-- Brouwer sur produit de simplexes
axiom brouwer_product {n : Nat} {actions : Fin n → Nat}
    (f : SimplexProduct n actions → SimplexProduct n actions)
    (hcont : True) :
    ∃ x : SimplexProduct n actions, f x = x

#check @brouwer_product
-- Extension au produit de simplexes
-- Pour Nash, on a besoin du theoreme sur un produit de simplexes
-- (un simplexe par joueur)
def SimplexProduct (n : Nat) (actions : Fin n → Nat) : Type :=
  (i : Fin n) → Simplex (actions i)
-- Brouwer sur produit de simplexes
axiom brouwer_product {n : Nat} {actions : Fin n → Nat}
    (f : SimplexProduct n actions → SimplexProduct n actions)
    (hcont : True) :
    ∃ x : SimplexProduct n actions, f x = x
 @brouwer_product : ∀ {n : Nat} {actions : Fin n → Nat} (f : SimplexProduct n actions → SimplexProduct n actions),
  True → ∃ x, f x = x
--% env 3
Raw input {"cmd": "-- Extension au produit de simplexes\n\n-- Pour Nash, on a besoin du theoreme sur un produit de simplexes\n-- (un simplexe par joueur)\n\ndef SimplexProduct (n : Nat) (actions : Fin n \u2192 Nat) : Type :=\n (i : Fin n) \u2192 Simplex (actions i)\n\n-- Brouwer sur produit de simplexes\naxiom brouwer_product {n : Nat} {actions : Fin n \u2192 Nat}\n (f : SimplexProduct n actions \u2192 SimplexProduct n actions)\n (hcont : True) :\n \u2203 x : SimplexProduct n actions, f x = x\n\n#check @brouwer_product", "env": 2}
Raw output {"messages": [{"severity": "info", "pos": {"line": 15, "column": 0}, "endPos": {"line": 15, "column": 6}, "data": "@brouwer_product : ∀ {n : Nat} {actions : Fin n → Nat} (f : SimplexProduct n actions → SimplexProduct n actions),\n True → ∃ x, f x = x"}], "env": 3}

Interpretation : Produit de simplexes

La définition SimplexProduct et l’axiome brouwer_product etendent le theoreme de Brouwer au cas de plusieurs joueurs :

\[\text{SimplexProduct}\ n\ \text{actions} = \prod_{i=0}^{n-1} \Delta^{\text{actions}(i) - 1}\]

Pourquoi cette extension est cruciale : Un profil de stratégies mixtes associe a chaque joueur \(i\) une distribution sur \(\Delta^{\text{actions}(i) - 1}\). L’espace des profils est donc le produit cartesiens des simplexes individuels.

Proprietes preservees :

Propriete Simplexe seul Produit de simplexes
Compact Oui Oui (produit de compacts)
Convexe Oui Oui (produit de convexes)
Non vide Oui Oui

L’axiome brouwer_product affirme que toute fonction continue du produit vers lui-même admet un point fixe. C’est ce résultat qui sera applique a la fonction de meilleure reponse perturbee pour prouver l’existence de Nash.

## 3. Definitions de Jeu

Rappel des définitions du notebook GameTheory-02b-Lean-Definitions-Lean, adaptees pour la preuve d’existence. Nous définissons succèssivement : - La structure de jeu fini (FiniteGame) - Les profils de stratégies mixtes (MixedProfile, MixedProfileSimple) - Le gain espere (expectedPayoff2x2)

Ces définitions constituent les briques de base sur lesquelles repose la formalisation de l’équilibre de Nash et la preuve d’existence.

Exemple guide 4 : Verifier les hypotheses de Brouwer sur le simplexe

Solution contribuee par Clovis Lefebvre & Evariste Balvay (TP EPITA IASY 2026), integree comme exemple guide.

Le theoreme de Brouwer s’applique quand le domaine est compact, convexe et non vide. Pour un jeu a 2 joueurs avec 2 actions chacun, l’espace des stratégies mixtes est le produit de deux simplexes \(\Delta^1 \times \Delta^1\).

Objectif : Verifier que le simplexe Simplex 2 et le produit SimplexProduct 2 (fun _ => 2) sont bien définis, et construire un élément du simplexe pour confirmer que l’espace est non vide.

Indices : - # Étape 1 : Utiliser #check Simplex 2 pour vérifier que le type est bien défini - # Étape 2 : Utiliser #check SimplexProduct 2 (fun _ => 2) pour le produit - # Étape 3 : Construire un élément de type Simplex 2 avec { val := fun _ => 0.5, property := by sorry } - # Étape 4 : Repondre : quelle propriete du theoreme de Brouwer est la plus delicate a prouver formellement ? (compact, convexe, non vide) - # Indice : Le type Simplex 2 est le sous-type des vecteurs Fin 2 -> Float dont la somme vaut 1

-- Exemple guide 4 : Verifier les hypotheses de Brouwer pour un jeu 2x2
-- (solution Lefebvre & Balvay)
-- Le simplexe et le produit de simplexes donnent le domaine auquel
-- on appliquera Brouwer dans la preuve d'existence de Nash.

-- # Etape 1 : Verifier que le simplexe est bien defini
-- Le type Simplex 2 represente les distributions sur 2 actions.
#check Simplex 2

-- # Etape 2 : Verifier que le produit de simplexes est defini
-- Pour un jeu a 2 joueurs avec 2 actions chacun : Δ¹ × Δ¹.
#check SimplexProduct 2 (fun _ => 2)

-- # Etape 3 : Construire un element du simplexe pour montrer qu'il est non vide
-- Dans ce notebook, l'arithmetique Float est volontairement simplifiee :
-- on isole donc le calcul numerique 0.5 + 0.5 = 1 dans un axiome.
axiom half_half_in_simplex2 :
    (∀ i : Fin 2, (fun _ => (0.5 : Float)) i >= 0) ∧
    (List.finRange 2).foldl (fun acc i => acc + (fun _ => (0.5 : Float)) i) 0 = 1

def mySimplexPoint : Simplex 2 := {
  val := fun _ => 0.5
  property := half_half_in_simplex2
}

#check mySimplexPoint

-- # Etape 4 : Quelle propriete manque-t-il pour que Brouwer s'applique ?
-- Pour appliquer Brouwer, il faut un domaine non vide, convexe et compact.
-- Ici, `mySimplexPoint` illustre la non-vacuite ; la convexite est donnee
-- par `simplex_convex` ; la propriete la plus delicate a formaliser dans ce
-- notebook simplifie est la compacite du simplexe / produit de simplexes.

#check brouwer_product

-- Exemple guide 4 : Verifier les hypotheses de Brouwer pour un jeu 2x2
-- (solution Lefebvre & Balvay)
-- Le simplexe et le produit de simplexes donnent le domaine auquel
-- on appliquera Brouwer dans la preuve d'existence de Nash.
-- # Etape 1 : Verifier que le simplexe est bien defini
-- Le type Simplex 2 represente les distributions sur 2 actions.
 Simplex 2 : Type
-- # Etape 2 : Verifier que le produit de simplexes est defini
-- Pour un jeu a 2 joueurs avec 2 actions chacun : Δ¹ × Δ¹.
 SimplexProduct 2 fun x => 2 : Type
-- # Etape 3 : Construire un element du simplexe pour montrer qu'il est non vide
-- Dans ce notebook, l'arithmetique Float est volontairement simplifiee :
-- on isole donc le calcul numerique 0.5 + 0.5 = 1 dans un axiome.
axiom half_half_in_simplex2 :
    (∀ i : Fin 2, (fun _ => (0.5 : Float)) i >= 0) ∧
    (List.finRange 2).foldl (fun acc i => acc + (fun _ => (0.5 : Float)) i) 0 = 1
def mySimplexPoint : Simplex 2 := {
  val := fun _ => 0.5
  property := half_half_in_simplex2
}
 mySimplexPoint : Simplex 2
-- # Etape 4 : Quelle propriete manque-t-il pour que Brouwer s'applique ?
-- Pour appliquer Brouwer, il faut un domaine non vide, convexe et compact.
-- Ici, `mySimplexPoint` illustre la non-vacuite ; la convexite est donnee
-- par `simplex_convex` ; la propriete la plus delicate a formaliser dans ce
-- notebook simplifie est la compacite du simplexe / produit de simplexes.
 brouwer_product {n : Nat} {actions : Fin n → Nat} (f : SimplexProduct n actions → SimplexProduct n actions)
  (hcont : True) : ∃ x, f x = x
--% env 4
Raw input {"cmd": "-- Exemple guide 4 : Verifier les hypotheses de Brouwer pour un jeu 2x2\n-- (solution Lefebvre & Balvay)\n-- Le simplexe et le produit de simplexes donnent le domaine auquel\n-- on appliquera Brouwer dans la preuve d'existence de Nash.\n\n-- # Etape 1 : Verifier que le simplexe est bien defini\n-- Le type Simplex 2 represente les distributions sur 2 actions.\n#check Simplex 2\n\n-- # Etape 2 : Verifier que le produit de simplexes est defini\n-- Pour un jeu a 2 joueurs avec 2 actions chacun : \u0394\u00b9 \u00d7 \u0394\u00b9.\n#check SimplexProduct 2 (fun _ => 2)\n\n-- # Etape 3 : Construire un element du simplexe pour montrer qu'il est non vide\n-- Dans ce notebook, l'arithmetique Float est volontairement simplifiee :\n-- on isole donc le calcul numerique 0.5 + 0.5 = 1 dans un axiome.\naxiom half_half_in_simplex2 :\n (\u2200 i : Fin 2, (fun _ => (0.5 : Float)) i >= 0) \u2227\n (List.finRange 2).foldl (fun acc i => acc + (fun _ => (0.5 : Float)) i) 0 = 1\n\ndef mySimplexPoint : Simplex 2 := {\n val := fun _ => 0.5\n property := half_half_in_simplex2\n}\n\n#check mySimplexPoint\n\n-- # Etape 4 : Quelle propriete manque-t-il pour que Brouwer s'applique ?\n-- Pour appliquer Brouwer, il faut un domaine non vide, convexe et compact.\n-- Ici, `mySimplexPoint` illustre la non-vacuite ; la convexite est donnee\n-- par `simplex_convex` ; la propriete la plus delicate a formaliser dans ce\n-- notebook simplifie est la compacite du simplexe / produit de simplexes.\n\n#check brouwer_product\n", "env": 3}
Raw output {"messages": [{"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "Simplex 2 : Type"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "SimplexProduct 2 fun x => 2 : Type"}, {"severity": "info", "pos": {"line": 26, "column": 0}, "endPos": {"line": 26, "column": 6}, "data": "mySimplexPoint : Simplex 2"}, {"severity": "info", "pos": {"line": 34, "column": 0}, "endPos": {"line": 34, "column": 6}, "data": "brouwer_product {n : Nat} {actions : Fin n → Nat} (f : SimplexProduct n actions → SimplexProduct n actions)\n (hcont : True) : ∃ x, f x = x"}], "env": 4}

Exercice 1 : Points asymétriques et simplexe a trois actions

L’exemple guide 4 a construit le point uniforme (0.5, 0.5) de Simplex 2. Pour s’assurer que la construction est générale, on la rejoue avec des poids asymétriques, puis on monte en dimension.

Objectif : Construire un point asymétrique de Simplex 2, un point uniforme de Simplex 3, et identifier l’hypothese de Brouwer qui tombe quand on retire le bord du simplexe.

Indices : - # Étape 1 : Construire myAsymPoint : Simplex 2 avec les poids (0.3, 0.7), en axiomatisant le fait numérique comme dans l’exemple guide 4 - # Étape 2 : Construire un point uniforme de Simplex 3 avec les poids (1/3, 1/3, 1/3) - # Étape 3 : Verifier avec #check SimplexProduct 3 (fun _ => 2) l’espace de stratégies d’un jeu a 3 joueurs et 2 actions - # Étape 4 : Repondre en commentaire : sur l’interieur strict du simplexe (bord retire), quelle hypothese de Brouwer est perdue ?

-- Exercice 1 : Points asymetriques et simplexe a trois actions
-- TODO etudiant : generaliser la construction de l'exemple guide 4

-- # Etape 1 : Un point asymetrique de Simplex 2
-- TODO etudiant : axiomatiser le fait numerique 0.3 + 0.7 = 1 puis construire le point
-- axiom asym_in_simplex2 : ...
-- def myAsymPoint : Simplex 2 := {
--   val := fun i => ...   -- (0.3, 0.7) par pattern matching sur Fin 2
--   property := asym_in_simplex2
-- }

-- # Etape 2 : Le point uniforme de Simplex 3
-- TODO etudiant : meme construction avec les poids (1/3, 1/3, 1/3)

-- # Etape 3 : L'espace de strategies d'un jeu a 3 joueurs / 2 actions
-- TODO etudiant : utiliser #check SimplexProduct 3 (fun _ => 2)

-- # Etape 4 : Brouwer sur l'interieur strict du simplexe ?
-- TODO etudiant : repondre en commentaire (compact / convexe / non vide)

#check Simplex 3

-- Exercice 1 : Points asymetriques et simplexe a trois actions
-- TODO etudiant : generaliser la construction de l'exemple guide 4
-- # Etape 1 : Un point asymetrique de Simplex 2
-- TODO etudiant : axiomatiser le fait numerique 0.3 + 0.7 = 1 puis construire le point
-- axiom asym_in_simplex2 : ...
-- def myAsymPoint : Simplex 2 := {
--   val := fun i => ...   -- (0.3, 0.7) par pattern matching sur Fin 2
--   property := asym_in_simplex2
-- }
-- # Etape 2 : Le point uniforme de Simplex 3
-- TODO etudiant : meme construction avec les poids (1/3, 1/3, 1/3)
-- # Etape 3 : L'espace de strategies d'un jeu a 3 joueurs / 2 actions
-- TODO etudiant : utiliser #check SimplexProduct 3 (fun _ => 2)
-- # Etape 4 : Brouwer sur l'interieur strict du simplexe ?
-- TODO etudiant : repondre en commentaire (compact / convexe / non vide)
 Simplex 3 : Type
--% env 5
Raw input {"cmd": "-- Exercice 1 : Points asymetriques et simplexe a trois actions\n-- TODO etudiant : generaliser la construction de l'exemple guide 4\n\n-- # Etape 1 : Un point asymetrique de Simplex 2\n-- TODO etudiant : axiomatiser le fait numerique 0.3 + 0.7 = 1 puis construire le point\n-- axiom asym_in_simplex2 : ...\n-- def myAsymPoint : Simplex 2 := {\n-- val := fun i => ... -- (0.3, 0.7) par pattern matching sur Fin 2\n-- property := asym_in_simplex2\n-- }\n\n-- # Etape 2 : Le point uniforme de Simplex 3\n-- TODO etudiant : meme construction avec les poids (1/3, 1/3, 1/3)\n\n-- # Etape 3 : L'espace de strategies d'un jeu a 3 joueurs / 2 actions\n-- TODO etudiant : utiliser #check SimplexProduct 3 (fun _ => 2)\n\n-- # Etape 4 : Brouwer sur l'interieur strict du simplexe ?\n-- TODO etudiant : repondre en commentaire (compact / convexe / non vide)\n\n#check Simplex 3\n", "env": 4}
Raw output {"messages": [{"severity": "info", "pos": {"line": 21, "column": 0}, "endPos": {"line": 21, "column": 6}, "data": "Simplex 3 : Type"}], "env": 5} 
-- Structure de jeu fini

structure FiniteGame where
  numPlayers : Nat
  numActions : Fin numPlayers → Nat
  payoff : (i : Fin numPlayers) → 
           ((j : Fin numPlayers) → Fin (numActions j)) → 
           Float

#check FiniteGame
-- Structure de jeu fini
structure FiniteGame where
  numPlayers : Nat
  numActions : Fin numPlayers → Nat
  payoff : (i : Fin numPlayers) → 
           ((j : Fin numPlayers) → Fin (numActions j)) → 
           Float
 FiniteGame : Type
--% env 6
Raw input {"cmd": "-- Structure de jeu fini\n\nstructure FiniteGame where\n numPlayers : Nat\n numActions : Fin numPlayers \u2192 Nat\n payoff : (i : Fin numPlayers) \u2192 \n ((j : Fin numPlayers) \u2192 Fin (numActions j)) \u2192 \n Float\n\n#check FiniteGame", "env": 5}
Raw output {"messages": [{"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "FiniteGame : Type"}], "env": 6}

Interpretation

La structure FiniteGame capture formellement les trois composantes d’un jeu sous forme normale :

Champ Type Signification
numPlayers Nat Nombre de joueurs n
numActions Fin numPlayers -> Nat Fonction donnant le nombre d’actions de chaque joueur
payoff (i : Fin numPlayers) -> ((j : Fin numPlayers) -> Fin (numActions j)) -> Float Fonction de gain

Lecture de la fonction payoff : - Premier argument i : joueur dont on calcule le gain - Second argument : profil d’actions pures (une action par joueur) - Résultat : gain du joueur i pour ce profil

Exemple : Dans un jeu 2x2 comme le Dilemme du Prisonnier : - numPlayers = 2 - numActions 0 = 2, numActions 1 = 2 - payoff 0 (fun j => if j = 0 then 1 else 0) = gain du joueur 0 quand J0 joue action 1, J1 joue action 0

-- Profil de strategies mixtes

-- Un profil associe a chaque joueur une distribution sur ses actions
def MixedProfile (g : FiniteGame) : Type :=
  (i : Fin g.numPlayers) → Simplex (g.numActions i)

-- Alternative simplifiee avec Float
def MixedProfileSimple (g : FiniteGame) : Type :=
  (i : Fin g.numPlayers) → Fin (g.numActions i) → Float

#check MixedProfile
#check MixedProfileSimple
-- Profil de strategies mixtes
-- Un profil associe a chaque joueur une distribution sur ses actions
def MixedProfile (g : FiniteGame) : Type :=
  (i : Fin g.numPlayers) → Simplex (g.numActions i)
-- Alternative simplifiee avec Float
def MixedProfileSimple (g : FiniteGame) : Type :=
  (i : Fin g.numPlayers) → Fin (g.numActions i) → Float
 MixedProfile (g : FiniteGame) : Type
 MixedProfileSimple (g : FiniteGame) : Type
--% env 7
Raw input {"cmd": "-- Profil de strategies mixtes\n\n-- Un profil associe a chaque joueur une distribution sur ses actions\ndef MixedProfile (g : FiniteGame) : Type :=\n (i : Fin g.numPlayers) \u2192 Simplex (g.numActions i)\n\n-- Alternative simplifiee avec Float\ndef MixedProfileSimple (g : FiniteGame) : Type :=\n (i : Fin g.numPlayers) \u2192 Fin (g.numActions i) \u2192 Float\n\n#check MixedProfile\n#check MixedProfileSimple", "env": 6}
Raw output {"messages": [{"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "MixedProfile (g : FiniteGame) : Type"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "MixedProfileSimple (g : FiniteGame) : Type"}], "env": 7}

Interpretation

Un profil de stratégies mixtes associe a chaque joueur une distribution de probabilité sur ses actions.

Deux formalisations équivalentes :

Type Definition Interpretation
MixedProfile g (i : Fin g.numPlayers) -> Simplex (g.numActions i) Version rigoureuse avec contraintes du simplexe (probabilités >= 0, somme = 1)
MixedProfileSimple g (i : Fin g.numPlayers) -> Fin (g.numActions i) -> Float Version simplifiee sans contraintes explicites

Exemple concret : Pour un jeu a 2 joueurs avec 3 actions chacun, un profil mixte sigma est : - sigma(0) = [0.3, 0.5, 0.2] : distribution du joueur 1 - sigma(1) = [0.1, 0.4, 0.5] : distribution du joueur 2

Note : La version MixedProfileSimple est utilisee dans ce notebook pour simplifier les preuves, mais la version MixedProfile garantit mathématiquement que les stratégies sont bien des distributions de probabilité valides.

-- Gain espere

-- Le gain espere d'un joueur sous un profil mixte
-- (formule simplifiee pour 2 joueurs, 2 actions)
def expectedPayoff2x2 (U : Fin 2 → Fin 2 → Float) 
    (σ1 σ2 : Fin 2 → Float) : Float :=
  (σ1 0) * (σ2 0) * (U 0 0) +
  (σ1 0) * (σ2 1) * (U 0 1) +
  (σ1 1) * (σ2 0) * (U 1 0) +
  (σ1 1) * (σ2 1) * (U 1 1)

#check expectedPayoff2x2
-- Gain espere
-- Le gain espere d'un joueur sous un profil mixte
-- (formule simplifiee pour 2 joueurs, 2 actions)
def expectedPayoff2x2 (U : Fin 2 → Fin 2 → Float) 
    (σ1 σ2 : Fin 2 → Float) : Float :=
  (σ1 0) * (σ2 0) * (U 0 0) +
  (σ1 0) * (σ2 1) * (U 0 1) +
  (σ1 1) * (σ2 0) * (U 1 0) +
  (σ1 1) * (σ2 1) * (U 1 1)
 expectedPayoff2x2 (U : Fin 2 → Fin 2 → Float) (σ1 σ2 : Fin 2 → Float) : Float
--% env 8
Raw input {"cmd": "-- Gain espere\n\n-- Le gain espere d'un joueur sous un profil mixte\n-- (formule simplifiee pour 2 joueurs, 2 actions)\ndef expectedPayoff2x2 (U : Fin 2 \u2192 Fin 2 \u2192 Float) \n (\u03c31 \u03c32 : Fin 2 \u2192 Float) : Float :=\n (\u03c31 0) * (\u03c32 0) * (U 0 0) +\n (\u03c31 0) * (\u03c32 1) * (U 0 1) +\n (\u03c31 1) * (\u03c32 0) * (U 1 0) +\n (\u03c31 1) * (\u03c32 1) * (U 1 1)\n\n#check expectedPayoff2x2", "env": 7}
Raw output {"messages": [{"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "expectedPayoff2x2 (U : Fin 2 → Fin 2 → Float) (σ1 σ2 : Fin 2 → Float) : Float"}], "env": 8}

Interpretation : Gain espere

La fonction expectedPayoff2x2 implemente la formule du gain espere pour un jeu 2x2 :

\[E[u_i(\sigma_1, \sigma_2)] = \sum_{a_1, a_2} \sigma_1(a_1) \cdot \sigma_2(a_2) \cdot u_i(a_1, a_2)\]

C’est la moyenne pondérée des gains sur tous les profils d’actions possibles, ou les poids sont les probabilités jointes de jeu.

Decomposition pour Matching Pennies (avec \(\sigma_1 = \sigma_2 = (0.5, 0.5)\)) :

Terme Calcul Valeur
\(\sigma_1(0) \cdot \sigma_2(0) \cdot U(0,0)\) \(0.5 \times 0.5 \times 1\) 0.25
\(\sigma_1(0) \cdot \sigma_2(1) \cdot U(0,1)\) \(0.5 \times 0.5 \times (-1)\) -0.25
\(\sigma_1(1) \cdot \sigma_2(0) \cdot U(1,0)\) \(0.5 \times 0.5 \times (-1)\) -0.25
\(\sigma_1(1) \cdot \sigma_2(1) \cdot U(1,1)\) \(0.5 \times 0.5 \times 1\) 0.25
Total 0

Cette fonction est la brique de base pour définir l’équilibre de Nash : un profil est Nash si aucun joueur ne peut améliorér son gain espere par deviation unilaterale.

## 4. Meilleure Reponse et Equilibre de Nash

Correspondance de meilleure reponse

\[BR_i(\sigma_{-i}) = \arg\max_{\sigma_i} E[u_i(\sigma_i, \sigma_{-i})]\]

Lien avec les points fixes

\(\sigma^*\) est un équilibre de Nash ssi \(\sigma^*\) est un point fixe de la correspondance de meilleure reponse.

-- Definition de l'equilibre de Nash

-- Version simplifiee pour jeux 2 joueurs
structure Game2Players where
  actions1 : Nat
  actions2 : Nat
  payoff1 : Fin actions1 → Fin actions2 → Float
  payoff2 : Fin actions1 → Fin actions2 → Float

-- Deviation unilaterale
def deviate2 (σ : Fin 2 → Float × Float) (player : Fin 2) 
    (newStrat : Float × Float) : Fin 2 → Float × Float :=
  fun i => if i = player then newStrat else σ i

-- Equilibre de Nash (informel)
-- Un profil σ est Nash si aucun joueur ne peut ameliorer son gain
-- par une deviation unilaterale
def isNashEquilibrium2x2 (U1 U2 : Fin 2 → Fin 2 → Float) 
    (σ1 σ2 : Fin 2 → Float) : Prop :=
  -- Joueur 1 ne veut pas devier
  (∀ σ1' : Fin 2 → Float, 
    expectedPayoff2x2 U1 σ1 σ2 >= expectedPayoff2x2 U1 σ1' σ2) ∧
  -- Joueur 2 ne veut pas devier  
  (∀ σ2' : Fin 2 → Float,
    expectedPayoff2x2 U2 σ1 σ2 >= expectedPayoff2x2 U2 σ1 σ2')

#check isNashEquilibrium2x2
-- Definition de l'equilibre de Nash
-- Version simplifiee pour jeux 2 joueurs
structure Game2Players where
  actions1 : Nat
  actions2 : Nat
  payoff1 : Fin actions1 → Fin actions2 → Float
  payoff2 : Fin actions1 → Fin actions2 → Float
-- Deviation unilaterale
def deviate2 (σ : Fin 2 → Float × Float) (player : Fin 2) 
    (newStrat : Float × Float) : Fin 2 → Float × Float :=
  fun i => if i = player then newStrat else σ i
-- Equilibre de Nash (informel)
-- Un profil σ est Nash si aucun joueur ne peut ameliorer son gain
-- par une deviation unilaterale
def isNashEquilibrium2x2 (U1 U2 : Fin 2 → Fin 2 → Float) 
    (σ1 σ2 : Fin 2 → Float) : Prop :=
  -- Joueur 1 ne veut pas devier
  (∀ σ1' : Fin 2 → Float, 
    expectedPayoff2x2 U1 σ1 σ2 >= expectedPayoff2x2 U1 σ1' σ2) ∧
  -- Joueur 2 ne veut pas devier  
  (∀ σ2' : Fin 2 → Float,
    expectedPayoff2x2 U2 σ1 σ2 >= expectedPayoff2x2 U2 σ1 σ2')
 isNashEquilibrium2x2 (U1 U2 : Fin 2 → Fin 2 → Float) (σ1 σ2 : Fin 2 → Float) : Prop
--% env 9
Raw input {"cmd": "-- Definition de l'equilibre de Nash\n\n-- Version simplifiee pour jeux 2 joueurs\nstructure Game2Players where\n actions1 : Nat\n actions2 : Nat\n payoff1 : Fin actions1 \u2192 Fin actions2 \u2192 Float\n payoff2 : Fin actions1 \u2192 Fin actions2 \u2192 Float\n\n-- Deviation unilaterale\ndef deviate2 (\u03c3 : Fin 2 \u2192 Float \u00d7 Float) (player : Fin 2) \n (newStrat : Float \u00d7 Float) : Fin 2 \u2192 Float \u00d7 Float :=\n fun i => if i = player then newStrat else \u03c3 i\n\n-- Equilibre de Nash (informel)\n-- Un profil \u03c3 est Nash si aucun joueur ne peut ameliorer son gain\n-- par une deviation unilaterale\ndef isNashEquilibrium2x2 (U1 U2 : Fin 2 \u2192 Fin 2 \u2192 Float) \n (\u03c31 \u03c32 : Fin 2 \u2192 Float) : Prop :=\n -- Joueur 1 ne veut pas devier\n (\u2200 \u03c31' : Fin 2 \u2192 Float, \n expectedPayoff2x2 U1 \u03c31 \u03c32 >= expectedPayoff2x2 U1 \u03c31' \u03c32) \u2227\n -- Joueur 2 ne veut pas devier \n (\u2200 \u03c32' : Fin 2 \u2192 Float,\n expectedPayoff2x2 U2 \u03c31 \u03c32 >= expectedPayoff2x2 U2 \u03c31 \u03c32')\n\n#check isNashEquilibrium2x2", "env": 8}
Raw output {"messages": [{"severity": "info", "pos": {"line": 27, "column": 0}, "endPos": {"line": 27, "column": 6}, "data": "isNashEquilibrium2x2 (U1 U2 : Fin 2 → Fin 2 → Float) (σ1 σ2 : Fin 2 → Float) : Prop"}], "env": 9}

Interpretation

Cette cellule formalise deux concepts cles :

1. Structure Game2Players : Une version simplifiee de jeu a 2 joueurs avec : - actions1, actions2 : nombre d’actions disponibles pour chaque joueur - payoff1, payoff2 : matrices de gains pour chaque joueur

2. Definition formelle de l’équilibre de Nash : Le predicat isNashEquilibrium2x2 capture mathématiquement l’idee qu’aucun joueur ne peut améliorér son gain par une deviation unilaterale :

\[\forall i, \forall \sigma'_i : E[u_i(\sigma^*)] \geq E[u_i(\sigma'_i, \sigma^*_{-i})]\]

Composante Signification
forall sigma1' Pour toute stratégie alternative du joueur 1
expectedPayoff2x2 U1 sigma1 sigma2 Gain espere actuel
>= expectedPayoff2x2 U1 sigma1' sigma2 Doit etre au moins aussi bon que toute deviation

Lien avec les points fixes : Un équilibre de Nash est précisément un point fixe de la correspondance de meilleure reponse. C’est cette equivalence qui permet d’appliquer le theoreme de Brouwer.

Exemple guide 5 : Calculer le gain espere pour un profil mixte

Solution contribuee par Clovis Lefebvre & Evariste Balvay (TP EPITA IASY 2026), integree comme exemple guide.

Dans cette section, nous avons défini expectedPayoff2x2 qui calcule le gain espere pour un jeu 2x2. L’objectif est d’utiliser cette fonction pour évaluer un profil de stratégies mixtes dans un jeu concret.

Objectif : Pour le jeu Chicken (poule mouillee), calculer le gain espere des deux joueurs pour un profil mixte donne et vérifier si une deviation amélioré le gain d’un joueur.

Swan (0) Straight (1)
Swan (0) (0, 0) (-1, 1)
Straight (1) (1, -1) (-10, -10)

Indices : - # Étape 1 : Définir les matrices de gain chicken1 et chicken2 (pattern matching sur Fin 2) - # Étape 2 : Définir un profil mixte, par exemple sigma1 = (0.8, 0.2) et sigma2 = (0.8, 0.2) - # Étape 3 : Calculer le gain espere avec expectedPayoff2x2 - # Étape 4 : Verifier si devier vers l’action pure “Straight” (1, 0) amélioré le gain du joueur 1

-- Exemple guide 5 : Gain espere dans le jeu Chicken
-- (solution Lefebvre & Balvay)
-- On utilise la matrice :
--              Swan(0)   Straight(1)
-- Swan(0)      (0,0)     (-1,1)
-- Straight(1)  (1,-1)    (-10,-10)

-- # Etape 1 : Matrice de gain du joueur 1
def chicken1 : Fin 2 → Fin 2 → Float
  | 0, 0 => 0
  | 0, 1 => -1
  | 1, 0 => 1
  | 1, 1 => -10

-- # Etape 2 : Matrice de gain du joueur 2
def chicken2 : Fin 2 → Fin 2 → Float
  | 0, 0 => 0
  | 0, 1 => 1
  | 1, 0 => -1
  | 1, 1 => -10

-- # Etape 3 : Profil de strategies mixtes
-- Chaque joueur joue Swan avec probabilite 0.8 et Straight avec probabilite 0.2.
def chicken_sigma1 : Fin 2 → Float
  | 0 => 0.8
  | 1 => 0.2

def chicken_sigma2 : Fin 2 → Float
  | 0 => 0.8
  | 1 => 0.2

-- Deviations pures utiles pour comparer les gains du joueur 1.
def chicken_pure_swan : Fin 2 → Float
  | 0 => 1
  | 1 => 0

def chicken_pure_straight : Fin 2 → Float
  | 0 => 0
  | 1 => 1

-- # Etape 4 : Calculer le gain espere et verifier les deviations
-- E[u1(sigma1,sigma2)] = 0.8*0.8*0 + 0.8*0.2*(-1)
--                      + 0.2*0.8*1 + 0.2*0.2*(-10)
--                      = -0.4
-- Si J1 devie vers Straight pur : 0*0.8*0 + 0*0.2*(-1)
--                              + 1*0.8*1 + 1*0.2*(-10)
--                              = -1.2
-- Cette deviation n'ameliore donc pas son gain.
#check expectedPayoff2x2 chicken1 chicken_sigma1 chicken_sigma2
#check expectedPayoff2x2 chicken2 chicken_sigma1 chicken_sigma2
#check expectedPayoff2x2 chicken1 chicken_pure_straight chicken_sigma2

-- Exemple guide 5 : Gain espere dans le jeu Chicken
-- (solution Lefebvre & Balvay)
-- On utilise la matrice :
--              Swan(0)   Straight(1)
-- Swan(0)      (0,0)     (-1,1)
-- Straight(1)  (1,-1)    (-10,-10)
-- # Etape 1 : Matrice de gain du joueur 1
def chicken1 : Fin 2 → Fin 2 → Float
  | 0, 0 => 0
  | 0, 1 => -1
  | 1, 0 => 1
  | 1, 1 => -10
-- # Etape 2 : Matrice de gain du joueur 2
def chicken2 : Fin 2 → Fin 2 → Float
  | 0, 0 => 0
  | 0, 1 => 1
  | 1, 0 => -1
  | 1, 1 => -10
-- # Etape 3 : Profil de strategies mixtes
-- Chaque joueur joue Swan avec probabilite 0.8 et Straight avec probabilite 0.2.
def chicken_sigma1 : Fin 2 → Float
  | 0 => 0.8
  | 1 => 0.2
def chicken_sigma2 : Fin 2 → Float
  | 0 => 0.8
  | 1 => 0.2
-- Deviations pures utiles pour comparer les gains du joueur 1.
def chicken_pure_swan : Fin 2 → Float
  | 0 => 1
  | 1 => 0
def chicken_pure_straight : Fin 2 → Float
  | 0 => 0
  | 1 => 1
-- # Etape 4 : Calculer le gain espere et verifier les deviations
-- E[u1(sigma1,sigma2)] = 0.8*0.8*0 + 0.8*0.2*(-1)
--                      + 0.2*0.8*1 + 0.2*0.2*(-10)
--                      = -0.4
-- Si J1 devie vers Straight pur : 0*0.8*0 + 0*0.2*(-1)
--                              + 1*0.8*1 + 1*0.2*(-10)
--                              = -1.2
-- Cette deviation n'ameliore donc pas son gain.
 expectedPayoff2x2 chicken1 chicken_sigma1 chicken_sigma2 : Float
 expectedPayoff2x2 chicken2 chicken_sigma1 chicken_sigma2 : Float
 expectedPayoff2x2 chicken1 chicken_pure_straight chicken_sigma2 : Float
--% env 10
Raw input {"cmd": "-- Exemple guide 5 : Gain espere dans le jeu Chicken\n-- (solution Lefebvre & Balvay)\n-- On utilise la matrice :\n-- Swan(0) Straight(1)\n-- Swan(0) (0,0) (-1,1)\n-- Straight(1) (1,-1) (-10,-10)\n\n-- # Etape 1 : Matrice de gain du joueur 1\ndef chicken1 : Fin 2 \u2192 Fin 2 \u2192 Float\n | 0, 0 => 0\n | 0, 1 => -1\n | 1, 0 => 1\n | 1, 1 => -10\n\n-- # Etape 2 : Matrice de gain du joueur 2\ndef chicken2 : Fin 2 \u2192 Fin 2 \u2192 Float\n | 0, 0 => 0\n | 0, 1 => 1\n | 1, 0 => -1\n | 1, 1 => -10\n\n-- # Etape 3 : Profil de strategies mixtes\n-- Chaque joueur joue Swan avec probabilite 0.8 et Straight avec probabilite 0.2.\ndef chicken_sigma1 : Fin 2 \u2192 Float\n | 0 => 0.8\n | 1 => 0.2\n\ndef chicken_sigma2 : Fin 2 \u2192 Float\n | 0 => 0.8\n | 1 => 0.2\n\n-- Deviations pures utiles pour comparer les gains du joueur 1.\ndef chicken_pure_swan : Fin 2 \u2192 Float\n | 0 => 1\n | 1 => 0\n\ndef chicken_pure_straight : Fin 2 \u2192 Float\n | 0 => 0\n | 1 => 1\n\n-- # Etape 4 : Calculer le gain espere et verifier les deviations\n-- E[u1(sigma1,sigma2)] = 0.8*0.8*0 + 0.8*0.2*(-1)\n-- + 0.2*0.8*1 + 0.2*0.2*(-10)\n-- = -0.4\n-- Si J1 devie vers Straight pur : 0*0.8*0 + 0*0.2*(-1)\n-- + 1*0.8*1 + 1*0.2*(-10)\n-- = -1.2\n-- Cette deviation n'ameliore donc pas son gain.\n#check expectedPayoff2x2 chicken1 chicken_sigma1 chicken_sigma2\n#check expectedPayoff2x2 chicken2 chicken_sigma1 chicken_sigma2\n#check expectedPayoff2x2 chicken1 chicken_pure_straight chicken_sigma2\n", "env": 9}
Raw output {"messages": [{"severity": "info", "pos": {"line": 49, "column": 0}, "endPos": {"line": 49, "column": 6}, "data": "expectedPayoff2x2 chicken1 chicken_sigma1 chicken_sigma2 : Float"}, {"severity": "info", "pos": {"line": 50, "column": 0}, "endPos": {"line": 50, "column": 6}, "data": "expectedPayoff2x2 chicken2 chicken_sigma1 chicken_sigma2 : Float"}, {"severity": "info", "pos": {"line": 51, "column": 0}, "endPos": {"line": 51, "column": 6}, "data": "expectedPayoff2x2 chicken1 chicken_pure_straight chicken_sigma2 : Float"}], "env": 10}

Exercice 2 : Dilemme du prisonnier – deviation et dominance

L’exemple guide 5 a montre que dans Chicken, devier vers l’action pure Straight n’amélioré pas le gain du joueur 1. Le dilemme du prisonnier illustre la situation opposee : une action domine strictement l’autre, et la deviation est toujours payante.

Cooperer (0) Trahir (1)
Cooperer (0) (-1, -1) (-3, 0)
Trahir (1) (0, -3) (-2, -2)

Objectif : Calculer le gain espere du profil mixte uniforme et montrer que la deviation vers Trahir pur amélioré strictement le gain du joueur 1 – contrairement a Chicken.

Indices : - # Étape 1 : Définir les matrices pd1 et pd2 (pattern matching sur Fin 2) - # Étape 2 : Garder le profil mixte uniforme sigma1 = sigma2 = (0.5, 0.5) - # Étape 3 : Calculer E[u1] a la main en commentaire, puis vérifier avec #check expectedPayoff2x2 - # Étape 4 : Comparer avec la deviation vers Trahir pur ; que conclure sur l’unique équilibre de Nash du jeu ?

-- Exercice 2 : Dilemme du prisonnier -- deviation et dominance
-- TODO etudiant : definir les matrices et comparer profil mixte vs deviation pure

-- # Etape 1 : Matrices de gain
def pd1 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer
def pd2 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer

-- # Etape 2 : Profil mixte uniforme
def pd_sigma1 : Fin 2 → Float := fun _ => 0.5
def pd_sigma2 : Fin 2 → Float := fun _ => 0.5

-- # Etape 3 : Gain espere du profil mixte
-- TODO etudiant : calculer E[u1] a la main en commentaire, puis verifier :
-- #check expectedPayoff2x2 pd1 pd_sigma1 pd_sigma2

-- # Etape 4 : Deviation vers Trahir pur
-- TODO etudiant : definir pd_pure_trahir (probabilite 1 sur l'action 1) et comparer
-- Quel est l'unique equilibre de Nash du dilemme du prisonnier ?

#check Nat

-- Exercice 2 : Dilemme du prisonnier -- deviation et dominance
-- TODO etudiant : definir les matrices et comparer profil mixte vs deviation pure
-- # Etape 1 : Matrices de gain
def pd1 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer
def pd2 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer
-- # Etape 2 : Profil mixte uniforme
def pd_sigma1 : Fin 2 → Float := fun _ => 0.5
def pd_sigma2 : Fin 2 → Float := fun _ => 0.5
-- # Etape 3 : Gain espere du profil mixte
-- TODO etudiant : calculer E[u1] a la main en commentaire, puis verifier :
-- #check expectedPayoff2x2 pd1 pd_sigma1 pd_sigma2
-- # Etape 4 : Deviation vers Trahir pur
-- TODO etudiant : definir pd_pure_trahir (probabilite 1 sur l'action 1) et comparer
-- Quel est l'unique equilibre de Nash du dilemme du prisonnier ?
 Nat : Type
--% env 11
Raw input {"cmd": "-- Exercice 2 : Dilemme du prisonnier -- deviation et dominance\n-- TODO etudiant : definir les matrices et comparer profil mixte vs deviation pure\n\n-- # Etape 1 : Matrices de gain\ndef pd1 : Fin 2 \u2192 Fin 2 \u2192 Float := fun _ _ => 0 -- TODO etudiant : completer\ndef pd2 : Fin 2 \u2192 Fin 2 \u2192 Float := fun _ _ => 0 -- TODO etudiant : completer\n\n-- # Etape 2 : Profil mixte uniforme\ndef pd_sigma1 : Fin 2 \u2192 Float := fun _ => 0.5\ndef pd_sigma2 : Fin 2 \u2192 Float := fun _ => 0.5\n\n-- # Etape 3 : Gain espere du profil mixte\n-- TODO etudiant : calculer E[u1] a la main en commentaire, puis verifier :\n-- #check expectedPayoff2x2 pd1 pd_sigma1 pd_sigma2\n\n-- # Etape 4 : Deviation vers Trahir pur\n-- TODO etudiant : definir pd_pure_trahir (probabilite 1 sur l'action 1) et comparer\n-- Quel est l'unique equilibre de Nash du dilemme du prisonnier ?\n\n#check Nat\n", "env": 10}
Raw output {"messages": [{"severity": "info", "pos": {"line": 20, "column": 0}, "endPos": {"line": 20, "column": 6}, "data": "Nat : Type"}], "env": 11} 
-- Fonction de meilleure reponse perturbee

-- L'idee : au lieu d'utiliser la correspondance BR (multi-valuee),
-- on construit une fonction continue qui "pousse" vers BR

-- f(σ) = normalise(σ + ε * (BR(σ) - σ))

-- Version simplifiee (placeholder)
def perturbedBR (g : FiniteGame) (σ : MixedProfileSimple g) : 
    MixedProfileSimple g :=
  -- Dans la vraie preuve, cette fonction:
  -- 1. Calcule le regret pour chaque action
  -- 2. Ajoute du poids aux actions avec regret positif
  -- 3. Normalise
  σ  -- Placeholder

#check perturbedBR
-- Fonction de meilleure reponse perturbee
-- L'idee : au lieu d'utiliser la correspondance BR (multi-valuee),
-- on construit une fonction continue qui "pousse" vers BR
-- f(σ) = normalise(σ + ε * (BR(σ) - σ))
-- Version simplifiee (placeholder)
def perturbedBR (g : FiniteGame) (σ : MixedProfileSimple g) : 
    MixedProfileSimple g :=
  -- Dans la vraie preuve, cette fonction:
  -- 1. Calcule le regret pour chaque action
  -- 2. Ajoute du poids aux actions avec regret positif
  -- 3. Normalise
  σ  -- Placeholder
 perturbedBR (g : FiniteGame) (σ : MixedProfileSimple g) : MixedProfileSimple g
--% env 12
Raw input {"cmd": "-- Fonction de meilleure reponse perturbee\n\n-- L'idee : au lieu d'utiliser la correspondance BR (multi-valuee),\n-- on construit une fonction continue qui \"pousse\" vers BR\n\n-- f(\u03c3) = normalise(\u03c3 + \u03b5 * (BR(\u03c3) - \u03c3))\n\n-- Version simplifiee (placeholder)\ndef perturbedBR (g : FiniteGame) (\u03c3 : MixedProfileSimple g) : \n MixedProfileSimple g :=\n -- Dans la vraie preuve, cette fonction:\n -- 1. Calcule le regret pour chaque action\n -- 2. Ajoute du poids aux actions avec regret positif\n -- 3. Normalise\n \u03c3 -- Placeholder\n\n#check perturbedBR", "env": 11}
Raw output {"messages": [{"severity": "info", "pos": {"line": 17, "column": 0}, "endPos": {"line": 17, "column": 6}, "data": "perturbedBR (g : FiniteGame) (σ : MixedProfileSimple g) : MixedProfileSimple g"}], "env": 12}

Interpretation : Fonction de meilleure reponse perturbee

La définition perturbedBR introduit un concept central de la preuve d’existence : au lieu de travailler directement avec la correspondance de meilleure reponse (qui est multi-valuee), on construit une fonction continue qui approxime le comportement de meilleure reponse.

Pourquoi cette transformation ?

Problème avec BR directe Solution avec perturbedBR
Correspondance (multi-valuee) Fonction (valeur unique)
Brouwer ne s’applique pas Brouwer s’applique directement
Pas continue en général Continue par construction

La formule : \(f(\sigma) = \text{normalise}(\sigma + \varepsilon \cdot (BR(\sigma) - \sigma))\)

Le terme \(\varepsilon \cdot (BR(\sigma) - \sigma)\) ajoute une petite poussee dans la direction de la meilleure reponse. La normalisation garantit que le résultat reste dans le simplexe (somme = 1).

Note : Dans cette cellule, perturbedBR renvoie \(\sigma\) (placeholder). L’implementation complète calcule le regret pour chaque action et realloue les probabilités en consequence.

## 5. Structure de la Preuve d’Existence

Étapes principales :

  1. Construire la fonction de meilleure reponse perturbee \(f\)
  2. Montrer que \(f\) est continue (résultat technique)
  3. Appliquer Brouwer : \(f\) a un point fixe \(\sigma^*\)
  4. Verifier que \(\sigma^*\) est un équilibre de Nash
-- Theoreme d'existence de Nash

-- Gain esperé pour N joueurs (axiomatise)
-- La formule complete: E[u_i(sigma)] = sum_{a in A} prod_j sigma_j(a_j) * u_i(a)
-- La formalisation complete necessite un produit sur les profils d'actions
axiom expectedPayoffGeneral (g : FiniteGame) (σ : MixedProfileSimple g) 
    (i : Fin g.numPlayers) : Float

-- sigma est un equilibre de Nash : aucune deviation unilaterale n'ameliore
-- Formellement: forall i, forall sigma_i', E[u_i(sigma)] >= E[u_i(sigma_i', sigma_{-i})]
def IsNashEq (g : FiniteGame) (σ : MixedProfileSimple g) : Prop :=
  ∀ i : Fin g.numPlayers,
    ∀ σ'_i : Fin (g.numActions i) → Float,
      expectedPayoffGeneral g σ i >= 
        expectedPayoffGeneral g (fun j => if h : j = i then h ▸ σ'_i else σ j) i

-- Enonce formel : tout jeu fini possede un equilibre de Nash en strategies mixtes
theorem nash_equilibrium_exists (g : FiniteGame) 
    (h_pos : ∀ i, g.numActions i > 0) :
    ∃ σ : MixedProfileSimple g, IsNashEq g σ := by
  -- Structure de la preuve :
  -- 1. Definir f = perturbedBR (meilleure reponse perturbee)
  -- 2. f : produit de simplexes -> produit de simplexes est continue
  -- 3. Par Brouwer (brouwer_product), f a un point fixe sigma*
  -- 4. Ce point fixe satisfait IsNashEq (aucune deviation n'ameliore)
  sorry

#check nash_equilibrium_exists
#check IsNashEq
-- Theoreme d'existence de Nash
-- Gain esperé pour N joueurs (axiomatise)
-- La formule complete: E[u_i(sigma)] = sum_{a in A} prod_j sigma_j(a_j) * u_i(a)
-- La formalisation complete necessite un produit sur les profils d'actions
axiom expectedPayoffGeneral (g : FiniteGame) (σ : MixedProfileSimple g) 
    (i : Fin g.numPlayers) : Float
-- sigma est un equilibre de Nash : aucune deviation unilaterale n'ameliore
-- Formellement: forall i, forall sigma_i', E[u_i(sigma)] >= E[u_i(sigma_i', sigma_{-i})]
def IsNashEq (g : FiniteGame) (σ : MixedProfileSimple g) : Prop :=
  ∀ i : Fin g.numPlayers,
    ∀ σ'_i : Fin (g.numActions i) → Float,
      expectedPayoffGeneral g σ i >= 
        expectedPayoffGeneral g (fun j => if h : j = i then h ▸ σ'_i else σ j) i
-- Enonce formel : tout jeu fini possede un equilibre de Nash en strategies mixtes
🟨 declaration uses `sorry`
    (h_pos : ∀ i, g.numActions i > 0) :
    ∃ σ : MixedProfileSimple g, IsNashEq g σ := by
  -- Structure de la preuve :
  -- 1. Definir f = perturbedBR (meilleure reponse perturbee)
  -- 2. f : produit de simplexes -> produit de simplexes est continue
  -- 3. Par Brouwer (brouwer_product), f a un point fixe sigma*
  -- 4. Ce point fixe satisfait IsNashEq (aucune deviation n'ameliore)
  sorry
 nash_equilibrium_exists (g : FiniteGame) (h_pos : ∀ (i : Fin g.numPlayers), g.numActions i > 0) : ∃ σ, IsNashEq g σ
 IsNashEq (g : FiniteGame) (σ : MixedProfileSimple g) : Prop
--% env 13
--% prove 2
Raw input {"cmd": "-- Theoreme d'existence de Nash\n\n-- Gain esper\u00e9 pour N joueurs (axiomatise)\n-- La formule complete: E[u_i(sigma)] = sum_{a in A} prod_j sigma_j(a_j) * u_i(a)\n-- La formalisation complete necessite un produit sur les profils d'actions\naxiom expectedPayoffGeneral (g : FiniteGame) (\u03c3 : MixedProfileSimple g) \n (i : Fin g.numPlayers) : Float\n\n-- sigma est un equilibre de Nash : aucune deviation unilaterale n'ameliore\n-- Formellement: forall i, forall sigma_i', E[u_i(sigma)] >= E[u_i(sigma_i', sigma_{-i})]\ndef IsNashEq (g : FiniteGame) (\u03c3 : MixedProfileSimple g) : Prop :=\n \u2200 i : Fin g.numPlayers,\n \u2200 \u03c3'_i : Fin (g.numActions i) \u2192 Float,\n expectedPayoffGeneral g \u03c3 i >= \n expectedPayoffGeneral g (fun j => if h : j = i then h \u25b8 \u03c3'_i else \u03c3 j) i\n\n-- Enonce formel : tout jeu fini possede un equilibre de Nash en strategies mixtes\ntheorem nash_equilibrium_exists (g : FiniteGame) \n (h_pos : \u2200 i, g.numActions i > 0) :\n \u2203 \u03c3 : MixedProfileSimple g, IsNashEq g \u03c3 := by\n -- Structure de la preuve :\n -- 1. Definir f = perturbedBR (meilleure reponse perturbee)\n -- 2. f : produit de simplexes -> produit de simplexes est continue\n -- 3. Par Brouwer (brouwer_product), f a un point fixe sigma*\n -- 4. Ce point fixe satisfait IsNashEq (aucune deviation n'ameliore)\n sorry\n\n#check nash_equilibrium_exists\n#check IsNashEq", "env": 12}
Raw output {"sorries": [{"proofState": 2, "pos": {"line": 26, "column": 2}, "goal": "g : FiniteGame\nh_pos : ∀ (i : Fin g.numPlayers), g.numActions i > 0\n⊢ ∃ σ, IsNashEq g σ", "endPos": {"line": 26, "column": 7}}], "messages": [{"severity": "warning", "pos": {"line": 18, "column": 8}, "endPos": {"line": 18, "column": 31}, "data": "declaration uses `sorry`"}, {"severity": "info", "pos": {"line": 28, "column": 0}, "endPos": {"line": 28, "column": 6}, "data": "nash_equilibrium_exists (g : FiniteGame) (h_pos : ∀ (i : Fin g.numPlayers), g.numActions i > 0) : ∃ σ, IsNashEq g σ"}, {"severity": "info", "pos": {"line": 29, "column": 0}, "endPos": {"line": 29, "column": 6}, "data": "IsNashEq (g : FiniteGame) (σ : MixedProfileSimple g) : Prop"}], "env": 13}

Interpretation

Le theoreme nash_equilibrium_exists formalise le résultat central de John Nash (1950) : tout jeu fini possede au moins un équilibre en stratégies mixtes.

Nouvelles définitions :

Definition Rôle
expectedPayoffGeneral Gain esperé du joueur i sous le profil sigma (axiomatise)
IsNashEq Predicat d’équilibre de Nash : aucune deviation unilaterale n’amélioré

Definition de IsNashEq :

IsNashEq g sigma := forall i, forall sigma_i',
  E[u_i(sigma)] >= E[u_i(sigma_i', sigma_{-i})]

C’est la traduction formelle de : pour chaque joueur i, aucune stratégie alternative sigma_i’ ne donne un gain esperé strictement superieur a la stratégie courante sigma_i, quand les autrès joueurs conservent leurs stratégies.

Structure de la preuve (sorry - non complètee) : 1. Construction : On définit la fonction de meilleure reponse perturbee perturbedBR 2. Application de Brouwer : Cette fonction est continue sur un produit de simplexes (compact convexe), donc elle admet un point fixe (via brouwer_product) 3. Verification : Le point fixe satisfait IsNashEq (regret nul)

Lien avec isNashEquilibrium2x2 : La définition IsNashEq est la généralisation N-joueurs du predicat isNashEquilibrium2x2 défini plus haut pour 2 joueurs. Pour les jeux 2x2, expectedPayoff2x2 donne une implémentation concrete de expectedPayoffGeneral.

Note technique : expectedPayoffGeneral est axiomatise car la formule complète (produit de toutes les distributions d’actions) necessite des outils de sommation sur les produits finis de Mathlib. La preuve réelle utilise le regret : regret_i(a, sigma) = max(0, u_i(a, sigma_{-i}) - u_i(sigma)), et montre qu’au point fixe le regret est nul.

-- Version plus complete avec le lien a Brouwer

-- La preuve complete est dans math-xmum/Brouwer/Nash.lean
-- Structure de la preuve :

/-
1. Definir le regret:
   regret_i(a, σ) = max(0, u_i(a, σ_{-i}) - u_i(σ))

2. Definir la fonction de perturbation:
   f_i(σ)(a) = (σ_i(a) + ε * regret_i(a, σ)) / Z
   ou Z normalise pour que sum = 1

3. Montrer que f est continue:
   - regret est continue (max de fonctions continues)
   - normalisation preserve la continuite

4. Appliquer Brouwer:
   Le produit de simplexes est compact convexe
   f : produit → produit est continue
   Donc f a un point fixe σ*

5. Verifier que σ* est Nash:
   Au point fixe: σ*_i(a) = (σ*_i(a) + ε * regret_i(a, σ*)) / Z
   Si regret_i(a, σ*) > 0 pour une action a,
   alors σ*_i(a) devrait augmenter, contradiction.
   Donc regret = 0 partout, donc σ* est Nash.
-/

#check True  -- Preuve complete dans math-xmum/Brouwer
-- Version plus complete avec le lien a Brouwer
-- La preuve complete est dans math-xmum/Brouwer/Nash.lean
-- Structure de la preuve :
/-
1. Definir le regret:
   regret_i(a, σ) = max(0, u_i(a, σ_{-i}) - u_i(σ))
2. Definir la fonction de perturbation:
   f_i(σ)(a) = (σ_i(a) + ε * regret_i(a, σ)) / Z
   ou Z normalise pour que sum = 1
3. Montrer que f est continue:
   - regret est continue (max de fonctions continues)
   - normalisation preserve la continuite
4. Appliquer Brouwer:
   Le produit de simplexes est compact convexe
   f : produit → produit est continue
   Donc f a un point fixe σ*
5. Verifier que σ* est Nash:
   Au point fixe: σ*_i(a) = (σ*_i(a) + ε * regret_i(a, σ*)) / Z
   Si regret_i(a, σ*) > 0 pour une action a,
   alors σ*_i(a) devrait augmenter, contradiction.
   Donc regret = 0 partout, donc σ* est Nash.
-/
 True : Prop
--% env 14
Raw input {"cmd": "-- Version plus complete avec le lien a Brouwer\n\n-- La preuve complete est dans math-xmum/Brouwer/Nash.lean\n-- Structure de la preuve :\n\n/-\n1. Definir le regret:\n regret_i(a, \u03c3) = max(0, u_i(a, \u03c3_{-i}) - u_i(\u03c3))\n\n2. Definir la fonction de perturbation:\n f_i(\u03c3)(a) = (\u03c3_i(a) + \u03b5 * regret_i(a, \u03c3)) / Z\n ou Z normalise pour que sum = 1\n\n3. Montrer que f est continue:\n - regret est continue (max de fonctions continues)\n - normalisation preserve la continuite\n\n4. Appliquer Brouwer:\n Le produit de simplexes est compact convexe\n f : produit \u2192 produit est continue\n Donc f a un point fixe \u03c3*\n\n5. Verifier que \u03c3* est Nash:\n Au point fixe: \u03c3*_i(a) = (\u03c3*_i(a) + \u03b5 * regret_i(a, \u03c3*)) / Z\n Si regret_i(a, \u03c3*) > 0 pour une action a,\n alors \u03c3*_i(a) devrait augmenter, contradiction.\n Donc regret = 0 partout, donc \u03c3* est Nash.\n-/\n\n#check True -- Preuve complete dans math-xmum/Brouwer", "env": 13}
Raw output {"messages": [{"severity": "info", "pos": {"line": 30, "column": 0}, "endPos": {"line": 30, "column": 6}, "data": "True : Prop"}], "env": 14}

Interpretation : Le sketch de preuve complet

Le bloc de code précèdent detaille les cinq étapes de la preuve d’existence de Nash via Brouwer, en utilisant le concept de regret :

\[\text{regret}_i(a, \sigma) = \max(0, u_i(a, \sigma_{-i}) - u_i(\sigma))\]

Logique de la preuve :

  1. Le regret mesure l’incitation a devier vers l’action pure \(a\)
  2. La fonction de perturbation \(f_i(\sigma)(a) = \frac{\sigma_i(a) + \varepsilon \cdot \text{regret}_i(a, \sigma)}{Z}\) pousse les probabilités vers les meilleures reponses
  3. La normalisation par \(Z\) garantit que le résultat reste dans le simplexe
  4. Au point fixe \(\sigma^*\) : \(\sigma^*_i(a) = \frac{\sigma^*_i(a) + \varepsilon \cdot \text{regret}_i(a, \sigma^*)}{Z}\)
  5. Si \(\text{regret}_i(a, \sigma^*) > 0\), alors \(\sigma^*_i(a)\) augmente, contredisant le fait que \(\sigma^*\) est un point fixe. Donc le regret est nul partout, ce qui signifie que \(\sigma^*\) est un équilibre de Nash.

Point subtil : L’argument “le regret est nul au point fixe” est une preuve par l’absurde. Si une action avait un regret positif, elle recevrait plus de poids dans la perturbation, donc la stratégie ne serait pas stable.

Formalisations existantes

Depot Contenu Status
math-xmum/Brouwer Nash via Scarf vers Brouwer Complet
harfe/fixed-point-theorems-lean4 Brouwer + Kakutani Complet
MixedMatched/formalizing-game-theory Definitions N-joueurs En cours

Exemple guide 6 : Verifier un équilibre de Nash dans Battle of Sexes

Solution contribuee par Clovis Lefebvre & Evariste Balvay (TP EPITA IASY 2026), integree comme exemple guide.

Le jeu Battle of Sexes est un jeu 2x2 classique ou les deux joueurs préférént se coordonner, mais ont des préférences différentes sur l’action de coordination :

Opera (0) Foot (1)
Opera (0) (3, 2) (0, 0)
Foot (1) (0, 0) (2, 3)

Objectif : Définir les matrices de gain et vérifier qu’un profil mixte donne est (ou n’est pas) un équilibre de Nash en calculant les gains esperes.

Indices : - # Étape 1 : Définir les deux matrices de gain bos1 et bos2 (type Fin 2 -> Fin 2 -> Float) - # Étape 2 : Définir un profil mixte, par exemple sigma1 = (0.6, 0.4) et sigma2 = (0.4, 0.6) - # Étape 3 : Utiliser #check expectedPayoff2x2 pour calculer le gain de chaque joueur - # Étape 4 : Comparer avec le gain obtenu en deviant vers une action pure pour déterminer si c’est un équilibre

-- Exemple guide 6 : Battle of Sexes -- Verifier un equilibre de Nash
-- (solution Lefebvre & Balvay)
-- Matrice :
--             Opera(0)  Foot(1)
-- Opera(0)    (3,2)     (0,0)
-- Foot(1)     (0,0)     (2,3)

-- # Etape 1 : Definir la matrice de gain du joueur 1
def bos1 : Fin 2 → Fin 2 → Float
  | 0, 0 => 3
  | 0, 1 => 0
  | 1, 0 => 0
  | 1, 1 => 2

-- # Etape 2 : Definir la matrice de gain du joueur 2
def bos2 : Fin 2 → Fin 2 → Float
  | 0, 0 => 2
  | 0, 1 => 0
  | 1, 0 => 0
  | 1, 1 => 3

-- # Etape 3 : Definir un profil de strategies mixtes
-- Exemple propose : J1 joue Opera avec 0.6, J2 joue Opera avec 0.4.
def bos_sigma1 : Fin 2 → Float
  | 0 => 0.6
  | 1 => 0.4

def bos_sigma2 : Fin 2 → Float
  | 0 => 0.4
  | 1 => 0.6

-- Deviations pures pour comparer les incitations.
def bos_pure_opera : Fin 2 → Float
  | 0 => 1
  | 1 => 0

def bos_pure_foot : Fin 2 → Float
  | 0 => 0
  | 1 => 1

-- # Etape 4 : Calculer le gain espere de chaque joueur
-- Pour J1 : 0.6*0.4*3 + 0.4*0.6*2 = 1.2.
-- S'il devie vers Opera pur : 1*0.4*3 = 1.2.
-- S'il devie vers Foot pur : 1*0.6*2 = 1.2.
-- J1 est donc indifferent entre ses actions.
-- Pour J2 : 0.6*0.4*2 + 0.4*0.6*3 = 1.2.
-- S'il devie vers Opera pur : 0.6*1*2 = 1.2.
-- S'il devie vers Foot pur : 0.4*1*3 = 1.2.
-- J2 est donc aussi indifferent : ce profil est l'equilibre mixte classique.
#check expectedPayoff2x2 bos1 bos_sigma1 bos_sigma2
#check expectedPayoff2x2 bos2 bos_sigma1 bos_sigma2
#check expectedPayoff2x2 bos1 bos_pure_opera bos_sigma2
#check expectedPayoff2x2 bos1 bos_pure_foot bos_sigma2
#check expectedPayoff2x2 bos2 bos_sigma1 bos_pure_opera
#check expectedPayoff2x2 bos2 bos_sigma1 bos_pure_foot

-- Exemple guide 6 : Battle of Sexes -- Verifier un equilibre de Nash
-- (solution Lefebvre & Balvay)
-- Matrice :
--             Opera(0)  Foot(1)
-- Opera(0)    (3,2)     (0,0)
-- Foot(1)     (0,0)     (2,3)
-- # Etape 1 : Definir la matrice de gain du joueur 1
def bos1 : Fin 2 → Fin 2 → Float
  | 0, 0 => 3
  | 0, 1 => 0
  | 1, 0 => 0
  | 1, 1 => 2
-- # Etape 2 : Definir la matrice de gain du joueur 2
def bos2 : Fin 2 → Fin 2 → Float
  | 0, 0 => 2
  | 0, 1 => 0
  | 1, 0 => 0
  | 1, 1 => 3
-- # Etape 3 : Definir un profil de strategies mixtes
-- Exemple propose : J1 joue Opera avec 0.6, J2 joue Opera avec 0.4.
def bos_sigma1 : Fin 2 → Float
  | 0 => 0.6
  | 1 => 0.4
def bos_sigma2 : Fin 2 → Float
  | 0 => 0.4
  | 1 => 0.6
-- Deviations pures pour comparer les incitations.
def bos_pure_opera : Fin 2 → Float
  | 0 => 1
  | 1 => 0
def bos_pure_foot : Fin 2 → Float
  | 0 => 0
  | 1 => 1
-- # Etape 4 : Calculer le gain espere de chaque joueur
-- Pour J1 : 0.6*0.4*3 + 0.4*0.6*2 = 1.2.
-- S'il devie vers Opera pur : 1*0.4*3 = 1.2.
-- S'il devie vers Foot pur : 1*0.6*2 = 1.2.
-- J1 est donc indifferent entre ses actions.
-- Pour J2 : 0.6*0.4*2 + 0.4*0.6*3 = 1.2.
-- S'il devie vers Opera pur : 0.6*1*2 = 1.2.
-- S'il devie vers Foot pur : 0.4*1*3 = 1.2.
-- J2 est donc aussi indifferent : ce profil est l'equilibre mixte classique.
 expectedPayoff2x2 bos1 bos_sigma1 bos_sigma2 : Float
 expectedPayoff2x2 bos2 bos_sigma1 bos_sigma2 : Float
 expectedPayoff2x2 bos1 bos_pure_opera bos_sigma2 : Float
 expectedPayoff2x2 bos1 bos_pure_foot bos_sigma2 : Float
 expectedPayoff2x2 bos2 bos_sigma1 bos_pure_opera : Float
 expectedPayoff2x2 bos2 bos_sigma1 bos_pure_foot : Float
--% env 15
Raw input {"cmd": "-- Exemple guide 6 : Battle of Sexes -- Verifier un equilibre de Nash\n-- (solution Lefebvre & Balvay)\n-- Matrice :\n-- Opera(0) Foot(1)\n-- Opera(0) (3,2) (0,0)\n-- Foot(1) (0,0) (2,3)\n\n-- # Etape 1 : Definir la matrice de gain du joueur 1\ndef bos1 : Fin 2 \u2192 Fin 2 \u2192 Float\n | 0, 0 => 3\n | 0, 1 => 0\n | 1, 0 => 0\n | 1, 1 => 2\n\n-- # Etape 2 : Definir la matrice de gain du joueur 2\ndef bos2 : Fin 2 \u2192 Fin 2 \u2192 Float\n | 0, 0 => 2\n | 0, 1 => 0\n | 1, 0 => 0\n | 1, 1 => 3\n\n-- # Etape 3 : Definir un profil de strategies mixtes\n-- Exemple propose : J1 joue Opera avec 0.6, J2 joue Opera avec 0.4.\ndef bos_sigma1 : Fin 2 \u2192 Float\n | 0 => 0.6\n | 1 => 0.4\n\ndef bos_sigma2 : Fin 2 \u2192 Float\n | 0 => 0.4\n | 1 => 0.6\n\n-- Deviations pures pour comparer les incitations.\ndef bos_pure_opera : Fin 2 \u2192 Float\n | 0 => 1\n | 1 => 0\n\ndef bos_pure_foot : Fin 2 \u2192 Float\n | 0 => 0\n | 1 => 1\n\n-- # Etape 4 : Calculer le gain espere de chaque joueur\n-- Pour J1 : 0.6*0.4*3 + 0.4*0.6*2 = 1.2.\n-- S'il devie vers Opera pur : 1*0.4*3 = 1.2.\n-- S'il devie vers Foot pur : 1*0.6*2 = 1.2.\n-- J1 est donc indifferent entre ses actions.\n-- Pour J2 : 0.6*0.4*2 + 0.4*0.6*3 = 1.2.\n-- S'il devie vers Opera pur : 0.6*1*2 = 1.2.\n-- S'il devie vers Foot pur : 0.4*1*3 = 1.2.\n-- J2 est donc aussi indifferent : ce profil est l'equilibre mixte classique.\n#check expectedPayoff2x2 bos1 bos_sigma1 bos_sigma2\n#check expectedPayoff2x2 bos2 bos_sigma1 bos_sigma2\n#check expectedPayoff2x2 bos1 bos_pure_opera bos_sigma2\n#check expectedPayoff2x2 bos1 bos_pure_foot bos_sigma2\n#check expectedPayoff2x2 bos2 bos_sigma1 bos_pure_opera\n#check expectedPayoff2x2 bos2 bos_sigma1 bos_pure_foot\n", "env": 14}
Raw output {"messages": [{"severity": "info", "pos": {"line": 50, "column": 0}, "endPos": {"line": 50, "column": 6}, "data": "expectedPayoff2x2 bos1 bos_sigma1 bos_sigma2 : Float"}, {"severity": "info", "pos": {"line": 51, "column": 0}, "endPos": {"line": 51, "column": 6}, "data": "expectedPayoff2x2 bos2 bos_sigma1 bos_sigma2 : Float"}, {"severity": "info", "pos": {"line": 52, "column": 0}, "endPos": {"line": 52, "column": 6}, "data": "expectedPayoff2x2 bos1 bos_pure_opera bos_sigma2 : Float"}, {"severity": "info", "pos": {"line": 53, "column": 0}, "endPos": {"line": 53, "column": 6}, "data": "expectedPayoff2x2 bos1 bos_pure_foot bos_sigma2 : Float"}, {"severity": "info", "pos": {"line": 54, "column": 0}, "endPos": {"line": 54, "column": 6}, "data": "expectedPayoff2x2 bos2 bos_sigma1 bos_pure_opera : Float"}, {"severity": "info", "pos": {"line": 55, "column": 0}, "endPos": {"line": 55, "column": 6}, "data": "expectedPayoff2x2 bos2 bos_sigma1 bos_pure_foot : Float"}], "env": 15}

Exercice 3 : Stag Hunt – trouver l’équilibre mixte par indifference

L’exemple guide 6 a vérifie que le profil ((0.6, 0.4), (0.4, 0.6)) de Battle of Sexes rend chaque joueur indifferent entre ses actions pures. Cette fois, l’équilibre mixte n’est pas donne : il faut le calculer en posant la condition d’indifference, puis le vérifier.

Cerf (0) Lievre (1)
Cerf (0) (4, 4) (0, 3)
Lievre (1) (3, 0) (3, 3)

Objectif : Determiner la probabilité p de jouer Cerf qui rend l’adversaire indifferent, puis vérifier l’équilibre mixte obtenu comme dans l’exemple guide 6.

Indices : - # Étape 1 : Définir les matrices stag1 et stag2 - # Étape 2 : Poser l’indifference du joueur 2 quand J1 joue Cerf avec probabilité p : E[u2 | Cerf] = E[u2 | Lievre], et résoudre pour p - # Étape 3 : Définir le profil mixte symétrique (p, 1-p) pour les deux joueurs - # Étape 4 : Verifier l’indifference des deux joueurs avec #check expectedPayoff2x2 et les deviations pures, comme dans l’exemple guide 6

-- Exercice 3 : Stag Hunt -- trouver l'equilibre mixte par indifference
-- TODO etudiant : calculer p par la condition d'indifference, puis verifier

-- # Etape 1 : Matrices de gain
def stag1 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer
def stag2 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer

-- # Etape 2 : Condition d'indifference
-- TODO etudiant : si J1 joue Cerf avec probabilite p,
-- E[u2 | Cerf] = ... et E[u2 | Lievre] = ...
-- Resoudre E[u2 | Cerf] = E[u2 | Lievre] pour trouver p.

-- # Etape 3 : Profil mixte symetrique
def stag_sigma1 : Fin 2 → Float := fun _ => 0.5  -- TODO etudiant : remplacer par (p, 1-p)
def stag_sigma2 : Fin 2 → Float := fun _ => 0.5  -- TODO etudiant : remplacer par (p, 1-p)

-- # Etape 4 : Verifier l'indifference des deux joueurs
-- TODO etudiant : utiliser #check expectedPayoff2x2 avec les deviations pures

#check Nat

-- Exercice 3 : Stag Hunt -- trouver l'equilibre mixte par indifference
-- TODO etudiant : calculer p par la condition d'indifference, puis verifier
-- # Etape 1 : Matrices de gain
def stag1 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer
def stag2 : Fin 2 → Fin 2 → Float := fun _ _ => 0  -- TODO etudiant : completer
-- # Etape 2 : Condition d'indifference
-- TODO etudiant : si J1 joue Cerf avec probabilite p,
-- E[u2 | Cerf] = ... et E[u2 | Lievre] = ...
-- Resoudre E[u2 | Cerf] = E[u2 | Lievre] pour trouver p.
-- # Etape 3 : Profil mixte symetrique
def stag_sigma1 : Fin 2 → Float := fun _ => 0.5  -- TODO etudiant : remplacer par (p, 1-p)
def stag_sigma2 : Fin 2 → Float := fun _ => 0.5  -- TODO etudiant : remplacer par (p, 1-p)
-- # Etape 4 : Verifier l'indifference des deux joueurs
-- TODO etudiant : utiliser #check expectedPayoff2x2 avec les deviations pures
 Nat : Type
--% env 16
Raw input {"cmd": "-- Exercice 3 : Stag Hunt -- trouver l'equilibre mixte par indifference\n-- TODO etudiant : calculer p par la condition d'indifference, puis verifier\n\n-- # Etape 1 : Matrices de gain\ndef stag1 : Fin 2 \u2192 Fin 2 \u2192 Float := fun _ _ => 0 -- TODO etudiant : completer\ndef stag2 : Fin 2 \u2192 Fin 2 \u2192 Float := fun _ _ => 0 -- TODO etudiant : completer\n\n-- # Etape 2 : Condition d'indifference\n-- TODO etudiant : si J1 joue Cerf avec probabilite p,\n-- E[u2 | Cerf] = ... et E[u2 | Lievre] = ...\n-- Resoudre E[u2 | Cerf] = E[u2 | Lievre] pour trouver p.\n\n-- # Etape 3 : Profil mixte symetrique\ndef stag_sigma1 : Fin 2 \u2192 Float := fun _ => 0.5 -- TODO etudiant : remplacer par (p, 1-p)\ndef stag_sigma2 : Fin 2 \u2192 Float := fun _ => 0.5 -- TODO etudiant : remplacer par (p, 1-p)\n\n-- # Etape 4 : Verifier l'indifference des deux joueurs\n-- TODO etudiant : utiliser #check expectedPayoff2x2 avec les deviations pures\n\n#check Nat\n", "env": 15}
Raw output {"messages": [{"severity": "info", "pos": {"line": 20, "column": 0}, "endPos": {"line": 20, "column": 6}, "data": "Nat : Type"}], "env": 16}

## 6. Exemples guides

Exemple guide 1 : Convexite du simplexe

Completer la preuve que le simplexe est convexe.

Exemple guide 2 : Point fixe explicite

Pour le jeu Matching Pennies, montrer que la stratégie uniforme (0.5, 0.5) est un point fixe de la fonction de meilleure reponse.

Exemple guide 3 : Contre-exemple a Brouwer

Construire un exemple de fonction sans point fixe quand le domaine n’est pas compact.

Trois exemples guides supplementaires (4 a 6), issus des solutions contribuees par Clovis Lefebvre & Evariste Balvay (TP 2026), accompagnent les exercices 1 a 3 plus haut dans le notebook.

## 7. Corrections – Reference enseignant

Les corrections ci-dessous illustrent trois techniques de preuve essentielles en formalisation de la théorie des jeux :

Correction Technique Concept demontre
Exemple guide 1 Decomposition en sous-objectifs + axiomes algebriques Convexite du simplexe
Exemple guide 2 Calcul explicite + axiome numérique Point fixe de la meilleure reponse
Exemple guide 3 Preuve par contradiction (intro + exact) Necessite de la compacite

Chaque correction utilise le pattern classique : unfold pour deployer les définitions, have pour les résultats intermediaires, exact pour conclure.

Correction Exemple guide 1

-- Solution Exemple guide 1 : Convexite du simplexe

-- La preuve repose sur deux faits:
-- 1. Si x_i >= 0, y_i >= 0, λ >= 0, (1-λ) >= 0
--    alors λ*x_i + (1-λ)*y_i >= 0

-- 2. Si sum(x) = 1 et sum(y) = 1
--    alors sum(tx + (1-λ)y) = λ*sum(x) + (1-λ)*sum(y)
--                           = λ*1 + (1-λ)*1 = 1

-- Preuve formelle (avec axiomes sur Float)
-- Note: Lean 4 ne dispose pas d'arithmetique decidable sur Float ;
-- on axiomatise les proprietes algebriques utilisees (vraies sur R).
axiom float_nonneg_mul : ∀ a b : Float, a >= 0 → b >= 0 → a * b >= 0
axiom float_nonneg_add : ∀ a b : Float, a >= 0 → b >= 0 → a + b >= 0
axiom float_one_sub_nonneg : ∀ t : Float, t <= 1 → 1 - t >= 0

theorem simplex_convex_proof (n : Nat) (x y : Fin n → Float) (t : Float)
    (hx : ∀ i, x i >= 0) (hy : ∀ i, y i >= 0)
    (ht : 0 <= t) (ht' : t <= 1) :
    ∀ i, convexCombination n x y t i >= 0 := by
  intro i
  unfold convexCombination
  -- t * x i >= 0 car t >= 0 et x i >= 0
  have h_tx : t * x i >= 0 := float_nonneg_mul t (x i) ht (hx i)
  -- (1 - t) >= 0 car t <= 1
  have h1t : (1 - t) >= 0 := float_one_sub_nonneg t ht'
  -- (1 - t) * y i >= 0 car (1-t) >= 0 et y i >= 0
  have h_1ty : (1 - t) * y i >= 0 := float_nonneg_mul (1 - t) (y i) h1t (hy i)
  -- La somme de deux nombres positifs est positive
  exact float_nonneg_add (t * x i) ((1 - t) * y i) h_tx h_1ty

#check simplex_convex_proof

-- Solution Exemple guide 1 : Convexite du simplexe
-- La preuve repose sur deux faits:
-- 1. Si x_i >= 0, y_i >= 0, λ >= 0, (1-λ) >= 0
--    alors λ*x_i + (1-λ)*y_i >= 0
-- 2. Si sum(x) = 1 et sum(y) = 1
--    alors sum(tx + (1-λ)y) = λ*sum(x) + (1-λ)*sum(y)
--                           = λ*1 + (1-λ)*1 = 1
-- Preuve formelle (avec axiomes sur Float)
-- Note: Lean 4 ne dispose pas d'arithmetique decidable sur Float ;
-- on axiomatise les proprietes algebriques utilisees (vraies sur R).
axiom float_nonneg_mul : ∀ a b : Float, a >= 0 → b >= 0 → a * b >= 0
axiom float_nonneg_add : ∀ a b : Float, a >= 0 → b >= 0 → a + b >= 0
axiom float_one_sub_nonneg : ∀ t : Float, t <= 1 → 1 - t >= 0
theorem simplex_convex_proof (n : Nat) (x y : Fin n → Float) (t : Float)
    (hx : ∀ i, x i >= 0) (hy : ∀ i, y i >= 0)
    (ht : 0 <= t) (ht' : t <= 1) :
    ∀ i, convexCombination n x y t i >= 0 := by
  intro i
  unfold convexCombination
  -- t * x i >= 0 car t >= 0 et x i >= 0
  have h_tx : t * x i >= 0 := float_nonneg_mul t (x i) ht (hx i)
  -- (1 - t) >= 0 car t <= 1
  have h1t : (1 - t) >= 0 := float_one_sub_nonneg t ht'
  -- (1 - t) * y i >= 0 car (1-t) >= 0 et y i >= 0
  have h_1ty : (1 - t) * y i >= 0 := float_nonneg_mul (1 - t) (y i) h1t (hy i)
  -- La somme de deux nombres positifs est positive
  exact float_nonneg_add (t * x i) ((1 - t) * y i) h_tx h_1ty
 simplex_convex_proof (n : Nat) (x y : Fin n → Float) (t : Float) (hx : ∀ (i : Fin n), x i ≥ 0)
  (hy : ∀ (i : Fin n), y i ≥ 0) (ht : 0 ≤ t) (ht' : t ≤ 1) (i : Fin n) : convexCombination n x y t i ≥ 0
--% env 17
Raw input {"cmd": "-- Solution Exemple guide 1 : Convexite du simplexe\n\n-- La preuve repose sur deux faits:\n-- 1. Si x_i >= 0, y_i >= 0, \u03bb >= 0, (1-\u03bb) >= 0\n-- alors \u03bb*x_i + (1-\u03bb)*y_i >= 0\n\n-- 2. Si sum(x) = 1 et sum(y) = 1\n-- alors sum(tx + (1-\u03bb)y) = \u03bb*sum(x) + (1-\u03bb)*sum(y)\n-- = \u03bb*1 + (1-\u03bb)*1 = 1\n\n-- Preuve formelle (avec axiomes sur Float)\n-- Note: Lean 4 ne dispose pas d'arithmetique decidable sur Float ;\n-- on axiomatise les proprietes algebriques utilisees (vraies sur R).\naxiom float_nonneg_mul : \u2200 a b : Float, a >= 0 \u2192 b >= 0 \u2192 a * b >= 0\naxiom float_nonneg_add : \u2200 a b : Float, a >= 0 \u2192 b >= 0 \u2192 a + b >= 0\naxiom float_one_sub_nonneg : \u2200 t : Float, t <= 1 \u2192 1 - t >= 0\n\ntheorem simplex_convex_proof (n : Nat) (x y : Fin n \u2192 Float) (t : Float)\n (hx : \u2200 i, x i >= 0) (hy : \u2200 i, y i >= 0)\n (ht : 0 <= t) (ht' : t <= 1) :\n \u2200 i, convexCombination n x y t i >= 0 := by\n intro i\n unfold convexCombination\n -- t * x i >= 0 car t >= 0 et x i >= 0\n have h_tx : t * x i >= 0 := float_nonneg_mul t (x i) ht (hx i)\n -- (1 - t) >= 0 car t <= 1\n have h1t : (1 - t) >= 0 := float_one_sub_nonneg t ht'\n -- (1 - t) * y i >= 0 car (1-t) >= 0 et y i >= 0\n have h_1ty : (1 - t) * y i >= 0 := float_nonneg_mul (1 - t) (y i) h1t (hy i)\n -- La somme de deux nombres positifs est positive\n exact float_nonneg_add (t * x i) ((1 - t) * y i) h_tx h_1ty\n\n#check simplex_convex_proof\n", "env": 16}
Raw output {"messages": [{"severity": "info", "pos": {"line": 33, "column": 0}, "endPos": {"line": 33, "column": 6}, "data": "simplex_convex_proof (n : Nat) (x y : Fin n → Float) (t : Float) (hx : ∀ (i : Fin n), x i ≥ 0)\n (hy : ∀ (i : Fin n), y i ≥ 0) (ht : 0 ≤ t) (ht' : t ≤ 1) (i : Fin n) : convexCombination n x y t i ≥ 0"}], "env": 17}

Interpretation : Preuve de convexite

Le theoreme simplex_convex_proof demontre rigoureusement la non-negativite des combinaisons convexes dans le simplexe, en decomposant le calcul en étapes élémentaires :

Étape de la preuve Tactique Résultat intermediaire
\(t \geq 0\) et \(x_i \geq 0\) Hypotheses ht, hx i Precondition
\(t \cdot x_i \geq 0\) float_nonneg_mul Premier terme positif
\(t \leq 1 \Rightarrow 1-t \geq 0\) float_one_sub_nonneg Complementaire
\((1-t) \cdot y_i \geq 0\) float_nonneg_mul Second terme positif
\(t \cdot x_i + (1-t) \cdot y_i \geq 0\) float_nonneg_add Conclusion

Ce qui est prouve et ce qui reste : Cette preuve couvre uniquement la non-negativite des coordonnees. La seconde partie (normalisation : la somme des coordonnees vaut 1) necessiterait un axiome supplementaire sur la linearite de la somme.

Note sur les axiomes : Les trois axiomes float_nonneg_mul, float_nonneg_add et float_one_sub_nonneg sont des proprietes vraies sur les réels mais non decidables sur Float en Lean 4. Dans une formalisation complète avec Mathlib, ces résultats decouleraient de l’arithmetique sur Real.

Correction Exemple guide 2

-- Solution Exemple guide 2 : Point fixe dans Matching Pennies

-- Matrice de Matching Pennies (J1 veut matcher)
def matchingPennies1 : Fin 2 → Fin 2 → Float
  | 0, 0 => 1   -- (H,H) : J1 gagne
  | 0, 1 => -1  -- (H,T) : J1 perd
  | 1, 0 => -1  -- (T,H) : J1 perd
  | 1, 1 => 1   -- (T,T) : J1 gagne

-- Strategie uniforme
def uniform2 : Fin 2 → Float := fun _ => 0.5

-- Gain espere avec strategie uniforme
-- E[u1] = 0.5*0.5*1 + 0.5*0.5*(-1) + 0.5*0.5*(-1) + 0.5*0.5*1 = 0
-- Contre n'importe quelle action pure, le gain est aussi 0
-- Donc la strategie uniforme est meilleure reponse

-- Lean 4 ne reduit pas l'arithmetique Float (pas de Decidable Float =) ;
-- on axiomatise le resultat numerique exact pour conclure.
axiom float_pennies_sum_zero :
    (0.5 : Float) * 0.5 * 1 + 0.5 * 0.5 * (-1) + 0.5 * 0.5 * (-1) + 0.5 * 0.5 * 1 = 0

theorem matching_pennies_uniform_is_br :
    -- Avec la strategie uniforme de l'adversaire,
    -- la strategie uniforme est une meilleure reponse
    expectedPayoff2x2 matchingPennies1 uniform2 uniform2 = 0 := by
  unfold expectedPayoff2x2 matchingPennies1 uniform2
  exact float_pennies_sum_zero

-- Donc (uniform, uniform) est un point fixe de BR
#check matching_pennies_uniform_is_br

-- Solution Exemple guide 2 : Point fixe dans Matching Pennies
-- Matrice de Matching Pennies (J1 veut matcher)
def matchingPennies1 : Fin 2 → Fin 2 → Float
  | 0, 0 => 1   -- (H,H) : J1 gagne
  | 0, 1 => -1  -- (H,T) : J1 perd
  | 1, 0 => -1  -- (T,H) : J1 perd
  | 1, 1 => 1   -- (T,T) : J1 gagne
-- Strategie uniforme
def uniform2 : Fin 2 → Float := fun _ => 0.5
-- Gain espere avec strategie uniforme
-- E[u1] = 0.5*0.5*1 + 0.5*0.5*(-1) + 0.5*0.5*(-1) + 0.5*0.5*1 = 0
-- Contre n'importe quelle action pure, le gain est aussi 0
-- Donc la strategie uniforme est meilleure reponse
-- Lean 4 ne reduit pas l'arithmetique Float (pas de Decidable Float =) ;
-- on axiomatise le resultat numerique exact pour conclure.
axiom float_pennies_sum_zero :
    (0.5 : Float) * 0.5 * 1 + 0.5 * 0.5 * (-1) + 0.5 * 0.5 * (-1) + 0.5 * 0.5 * 1 = 0
theorem matching_pennies_uniform_is_br :
    -- Avec la strategie uniforme de l'adversaire,
    -- la strategie uniforme est une meilleure reponse
    expectedPayoff2x2 matchingPennies1 uniform2 uniform2 = 0 := by
  unfold expectedPayoff2x2 matchingPennies1 uniform2
  exact float_pennies_sum_zero
-- Donc (uniform, uniform) est un point fixe de BR
 matching_pennies_uniform_is_br : expectedPayoff2x2 matchingPennies1 uniform2 uniform2 = 0
--% env 18
Raw input {"cmd": "-- Solution Exemple guide 2 : Point fixe dans Matching Pennies\n\n-- Matrice de Matching Pennies (J1 veut matcher)\ndef matchingPennies1 : Fin 2 \u2192 Fin 2 \u2192 Float\n | 0, 0 => 1 -- (H,H) : J1 gagne\n | 0, 1 => -1 -- (H,T) : J1 perd\n | 1, 0 => -1 -- (T,H) : J1 perd\n | 1, 1 => 1 -- (T,T) : J1 gagne\n\n-- Strategie uniforme\ndef uniform2 : Fin 2 \u2192 Float := fun _ => 0.5\n\n-- Gain espere avec strategie uniforme\n-- E[u1] = 0.5*0.5*1 + 0.5*0.5*(-1) + 0.5*0.5*(-1) + 0.5*0.5*1 = 0\n-- Contre n'importe quelle action pure, le gain est aussi 0\n-- Donc la strategie uniforme est meilleure reponse\n\n-- Lean 4 ne reduit pas l'arithmetique Float (pas de Decidable Float =) ;\n-- on axiomatise le resultat numerique exact pour conclure.\naxiom float_pennies_sum_zero :\n (0.5 : Float) * 0.5 * 1 + 0.5 * 0.5 * (-1) + 0.5 * 0.5 * (-1) + 0.5 * 0.5 * 1 = 0\n\ntheorem matching_pennies_uniform_is_br :\n -- Avec la strategie uniforme de l'adversaire,\n -- la strategie uniforme est une meilleure reponse\n expectedPayoff2x2 matchingPennies1 uniform2 uniform2 = 0 := by\n unfold expectedPayoff2x2 matchingPennies1 uniform2\n exact float_pennies_sum_zero\n\n-- Donc (uniform, uniform) est un point fixe de BR\n#check matching_pennies_uniform_is_br\n", "env": 17}
Raw output {"messages": [{"severity": "info", "pos": {"line": 31, "column": 0}, "endPos": {"line": 31, "column": 6}, "data": "matching_pennies_uniform_is_br : expectedPayoff2x2 matchingPennies1 uniform2 uniform2 = 0"}], "env": 18}

Interpretation : Matching Pennies

La preuve matching_pennies_uniform_is_br montre que pour le jeu Matching Pennies, la stratégie uniforme \((0.5, 0.5)\) est un point fixe de la meilleure reponse :

Résultat obtenu : \(E[u_1(\text{uniform}, \text{uniform})] = 0\)

Ce résultat est remarquable a plusieurs egards :

Aspect Observation
Symetrie du jeu Les gains sont symétriques (+1/-1), donc l’équilibre est nécessairement uniforme
Gain nul a l’équilibre Aucun joueur n’a d’avantage – c’est un jeu a somme nulle pur
Stabilite Devier vers n’importe quelle action pure donne le même gain de 0, donc aucune incitation a devier

Lien avec Brouwer : La stratégie uniforme est un point fixe de la correspondance de meilleure reponse. Si chaque joueur joue uniformêment, la meilleure reponse de l’autre est aussi la stratégie uniforme. C’est exactement le type de point fixe dont Brouwer garantit l’existence.

Note technique : L’axiome float_pennies_sum_zero est nécessaire car Lean 4 ne peut pas reduire automatiquement les expressions arithmetiques sur Float. Sur les réels formels (Rat ou Real de Mathlib), ring ou omega resoudraient ce calcul.

Correction Exemple guide 3

-- Solution Exemple guide 3 : Contre-exemple a Brouwer

-- Sur R (non compact), f(x) = x + 1 n'a pas de point fixe
def shiftByOne : Float → Float := fun x => x + 1

-- Propriete algebrique de R : x + 1 ≠ x pour tout reel x.
-- (En IEEE-754, ceci est faux pour |x| >= 2^53 a cause de la perte
-- de precision, mais ce notebook etudie l'algebre de R, pas les
-- pathologies du virgule flottante.)
axiom float_add_one_ne_self : ∀ x : Float, ¬ (x + 1 = x)

-- Si f(x) = x, alors x + 1 = x, donc 1 = 0, contradiction
theorem no_fixed_point_shift :
    ¬ ∃ x : Float, shiftByOne x = x := by
  intro ⟨x, hx⟩
  unfold shiftByOne at hx
  -- hx : x + 1 = x  contredit l'axiome float_add_one_ne_self
  exact float_add_one_ne_self x hx

-- Le probleme : R n'est pas compact (non borne)
-- La fonction peut "fuir a l'infini"

#check no_fixed_point_shift

-- Solution Exemple guide 3 : Contre-exemple a Brouwer
-- Sur R (non compact), f(x) = x + 1 n'a pas de point fixe
def shiftByOne : Float → Float := fun x => x + 1
-- Propriete algebrique de R : x + 1 ≠ x pour tout reel x.
-- (En IEEE-754, ceci est faux pour |x| >= 2^53 a cause de la perte
-- de precision, mais ce notebook etudie l'algebre de R, pas les
-- pathologies du virgule flottante.)
axiom float_add_one_ne_self : ∀ x : Float, ¬ (x + 1 = x)
-- Si f(x) = x, alors x + 1 = x, donc 1 = 0, contradiction
theorem no_fixed_point_shift :
    ¬ ∃ x : Float, shiftByOne x = x := by
  intro ⟨x, hx⟩
  unfold shiftByOne at hx
  -- hx : x + 1 = x  contredit l'axiome float_add_one_ne_self
  exact float_add_one_ne_self x hx
-- Le probleme : R n'est pas compact (non borne)
-- La fonction peut "fuir a l'infini"
 no_fixed_point_shift : ¬∃ x, shiftByOne x = x
--% env 19
Raw input {"cmd": "-- Solution Exemple guide 3 : Contre-exemple a Brouwer\n\n-- Sur R (non compact), f(x) = x + 1 n'a pas de point fixe\ndef shiftByOne : Float \u2192 Float := fun x => x + 1\n\n-- Propriete algebrique de R : x + 1 \u2260 x pour tout reel x.\n-- (En IEEE-754, ceci est faux pour |x| >= 2^53 a cause de la perte\n-- de precision, mais ce notebook etudie l'algebre de R, pas les\n-- pathologies du virgule flottante.)\naxiom float_add_one_ne_self : \u2200 x : Float, \u00ac (x + 1 = x)\n\n-- Si f(x) = x, alors x + 1 = x, donc 1 = 0, contradiction\ntheorem no_fixed_point_shift :\n \u00ac \u2203 x : Float, shiftByOne x = x := by\n intro \u27e8x, hx\u27e9\n unfold shiftByOne at hx\n -- hx : x + 1 = x contredit l'axiome float_add_one_ne_self\n exact float_add_one_ne_self x hx\n\n-- Le probleme : R n'est pas compact (non borne)\n-- La fonction peut \"fuir a l'infini\"\n\n#check no_fixed_point_shift\n", "env": 18}
Raw output {"messages": [{"severity": "info", "pos": {"line": 23, "column": 0}, "endPos": {"line": 23, "column": 6}, "data": "no_fixed_point_shift : ¬∃ x, shiftByOne x = x"}], "env": 19}

Interpretation du contre-exemple

Le theoreme no_fixed_point_shift demontre formellement que la fonction \(f(x) = x + 1\) n’admet pas de point fixe sur \(\mathbb{R}\). La preuve procede par contradiction : si \(f(x^*) = x^*\), alors \(x^* + 1 = x^*\), ce qui viole l’axiome float_add_one_ne_self.

Pourquoi c’est important pour Nash : Ce contre-exemple justifie chaque hypothese du theoreme de Brouwer :

Hypothese de Brouwer Rôle dans la preuve de Nash Violation dans le contre-exemple
Compact (ferme + borne) Garantit l’existence du point fixe \(\mathbb{R}\) n’est pas borne
Convexe Assure que les combinaisons convexes restent dans le domaine \(\mathbb{R}\) est convexe (OK)
Continuite de \(f\) Necessaire pour le theoreme \(f(x) = x+1\) est continue (OK)

C’est précisément parce que les simplexes sont compacts (fermes et bornes dans \(\mathbb{R}^n\)) que Brouwer s’applique, garantissant l’existence d’un équilibre de Nash.

## 8. Resume

Theoremes formalises

Theoreme Enonce Statut
Brouwer \(f: K \to K\) continue sur compact convexe \(\Rightarrow\) point fixe Axiomatise
Nash Tout jeu fini a un équilibre mixte Structure de preuve
Convexite Le simplexe est convexe Prouve (modulo Float)

Structure de la preuve de Nash

1. Construire f : produit de simplexes → produit de simplexes
2. Montrer que f est continue
3. Appliquer Brouwer : f a un point fixe σ*
4. Verifier : σ* est un équilibre de Nash

Concepts cles a retenir

Concept Definition formelle Importance
Simplexe \(\Delta^{n-1}\) \(\{x \in \mathbb{R}^n : x_i \geq 0, \sum x_i = 1\}\) Espace des stratégies mixtes
Point fixe \(f(x^*) = x^*\) Cle de voute de la preuve d’existence
Equilibre de Nash \(\forall i, \forall \sigma_i' : E[u_i(\sigma^*)] \geq E[u_i(\sigma_i', \sigma^*_{-i})]\) Stabilite stratégique
Regret \(\max(0, u_i(a, \sigma_{-i}) - u_i(\sigma))\) Mesure l’incitation a devier

Ressources

Navigation : << 4-NashEquilibrium (track principal) | Index | 4c-NashExistence-Python >> > Prolongement computationnel : GameTheory-04e — Oracles réflexifs — auto-référence, décision causale (CDT/EDT) et restriction finie vérifiée (#14450).

Retour au sommet