Notebook compagnon Lean 4 natif du notebook Python GameTheory-11-Python : on restate en Lean 4 les définitions et théorèmes clés de la théorie des jeux bayésiens (Harsanyi 1967), l’enchère de Vickrey (1961), et la monotonie de Blackwell (1953) sur la valeur de l’information. Toutes les preuves passent par le kernel lean4-wsl – pas de stub, pas de reimplementation Python. C’est le banc d’essai du prouveur multi-agent BG-prover (EPIC #1453) sur des théorèmes de BayesGames / Vickrey / Blackwell.
Cette extension formalise en Lean 4 le résultat central des enchères à valeur privée : le théorème de Vickrey (enchère au second prix — second-price sealed-bid), exécuté dans le kernel lean4-wsl.
Les théorèmes exécutés ci-dessous sont restatés à l’identique depuis le lake lean_game_defs_ext/ (module Bayesian), où ils sont prouvés sans aucun sorry. Le lake est un projet Lean 4 self-contained (core Lean 4, sans Mathlib) — donc ses énoncés se ré-élaborent tels quels dans le kernel notebook. On les restate ici pour exécution pédagogique vérifiée : le kernel lean4-wsl élabore réellement les vrais énoncés et produire les sorties (#check, #eval) ci-dessous.
Preuve de compilation du lake (exécution réelle, hors notebook car le kernel ne lance pas
lake) :$ cd lean_game_defs_ext && lake build Bayesian ✔ [13/13] Built Bayesian Build completed successfully (13 jobs). $ grep -rnE '^\s*sorry\b' Bayesian/*.lean | wc -l 0
Pourquoi restate inline plutôt que import Bayesian.Vickrey ? Le kernel interactif lean4-wsl (REPL lean4_jupyter) résout les import de modules lake uniquement au démarrage du process REPL, pas depuis une commande import interactive en cours de notebook (un import en milieu de flux n’est pas un module-load en Lean). Aucun notebook GameTheory/*.ipynb n’importe un lake — les notebooks Lean 2b/4b/8b/15b sont tous self-contained. Ce notebook suit ce même pattern établi (issue #4040, voie B). Le travail d’exploration import-from-lake (prelude NotebookCtx, launch via lake-env) continue en side-track sur #4251.
BayesGame2) comme structure de Harsanyi (types, actions, utilité conditionnelle par type).isBNE) : meilleure réponse par rapport à la stratégie de l’autre + distribution de types.v(vrai) = v est faiblement dominante dans une enchère au second prix à deux enchérisseurs.#eval sur des instances concrètes.| # | Section | Theme | Sortie attendue |
|---|---|---|---|
| 1 | Sommes finies Fin n |
sumFin compensée (Mathlib absent en kernel nu) |
#eval 2+2 = 4, somme 0..n |
| 2 | Types de Harsanyi | structure BayesGame2 |
construction compilée |
| 3 | Équilibre bayésien de Nash | isBNE (reducible def) |
API de vérification |
| 4 | Enchère de Vickrey | spa, dominance, théorème, rente |
Vickrey theorem + rente |
| 5 | Monotonie de Blackwell | maxFin + sumFin + signaux + 3 théorèmes | lemmes noyau-lean |
| 6 | Information peut nuire | gInfo vs gNoInfo + eq + chute |
kernel-decided contre-exemple |
| 7 | Récapitulatif | table résultats + ref lake | sortie standard |
Coût total : < 5 secondes (kernel lean4-wsl local, mathlib-tools minimal).
Concepts clés : types de Harsanyi, croyances a priori et a posteriori, meilleure réponse bayesienne, mécanisme d’enchères au second prix (Vickrey), information value theorem (Blackwell), contre-exemple en jeu (information peut nuire), kernel #eval/#check/#reduce/#decide en Lean 4.
Références : Harsanyi (1967) “Games with Incomplete Information Played by Bayesian Players”, Management Science 14(3) ; Vickrey (1961) “Counterspeculation, Auctions, and Competitive Sealed Tenders”, Journal of Finance 16(1) ; Blackwell (1953) “Equivalent Comparisons of Experiments”, Annals of Mathematical Statistics 24(2) ; le lake source bayesian_games_lean/ (EPIC #1453, registre dans docs/ledgers/3801-sota-axe2.md).
lean4-wsl (Lean 4 + elan, cf docs/reference/kernels-runtime.md).GameTheory-11-Python-BayesianGamesExt.ipynb (Python, calculs numeriques des mêmes modeles)GameTheory-02b-Lean-Definitions-Lean.ipynb (autre notebook Lean du dossier, définitions de base de la théorie des jeux)GameTheory-12-... (TBD) sur les jeux à information incomplète avancés#eval 2 + 2
#check Nat
4
Nat : Type
--% env 0
{"cmd": "#eval 2 + 2\n#check Nat\n"}
{"messages":
[{"severity": "info",
"pos": {"line": 1, "column": 0},
"endPos": {"line": 1, "column": 5},
"data": "4"},
{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data": "Nat : Type"}],
"env": 0}
Fin n (sumFin)Mathlib n’étant pas disponible (projet core-only), on définit une somme par récurrence structurelle sur n. C’est l’infrastructure d’espérance utilité des jeux bayésiens. (Source : lean_game_defs_ext/Bayesian/Sum.lean.)
def sumFin : (n : Nat) → (Fin n → Int) → Int
| 0, _ => 0
| n + 1, f => f 0 + sumFin n (fun i => f i.succ)C’est une définition classique, équivalente à Mathlib.Algebra.BigOperators.Fin.sumFin_eq_sum_range, mais sans la dépendance Mathlib. Le kernel Lean 4 l’accepte et #eval permet de calculer des sommes concrètes.
Pourquoi reinventer localement : le kernel lean4-wsl du dépôt CoursIA n’inclut pas Mathlib dans son contexte par defaut (Mathlib = plusieurs Go de fichiers .olean, charge lourde). Pour les sommes finies sur Fin n, une définition inductive locale suffit. On importe Mathlib.Tactic uniquement quand c’est nécessaire.
Sortie attendue (cellule code[0]) : #eval 2 + 2 retourne 4, #check Nat confirme le type.
Coût : < 50 ms (kernel Lean nu).
def sumFin : (n : Nat) → (Fin n → Int) → Int
| 0, _ => 0
| n + 1, f => f 0 + sumFin n (fun i => f i.succ)
@[simp] theorem sumFin_zero (f : Fin 0 → Int) : sumFin 0 f = 0 := rfl
@[simp] theorem sumFin_succ (n : Nat) (f : Fin (n + 1) → Int) :
sumFin (n + 1) f = f 0 + sumFin n (fun i => f i.succ) := rfl
@[simp] theorem sumFin_zero_fun (n : Nat) :
sumFin n (fun _ => (0 : Int)) = 0 := by
induction n with
| zero => simp
| succ n ih => simp [ih]
/-- La dominance ponctuelle se transfère aux sommes. -/
theorem sumFin_mono {n : Nat} {f g : Fin n → Int} (h : ∀ i, f i ≤ g i) :
sumFin n f ≤ sumFin n g := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
exact Int.add_le_add (h 0) (ih (fun i => h i.succ))
def sumFin : (n : Nat) → (Fin n → Int) → Int
| 0, _ => 0
| n + 1, f => f 0 + sumFin n (fun i => f i.succ)
@[simp] theorem sumFin_zero (f : Fin 0 → Int) : sumFin 0 f = 0 := rfl
@[simp] theorem sumFin_succ (n : Nat) (f : Fin (n + 1) → Int) :
sumFin (n + 1) f = f 0 + sumFin n (fun i => f i.succ) := rfl
@[simp] theorem sumFin_zero_fun (n : Nat) :
sumFin n (fun _ => (0 : Int)) = 0 := by
induction n with
| zero => simp
| succ n ih => simp [ih]
/-- La dominance ponctuelle se transfère aux sommes. -/
theorem sumFin_mono {n : Nat} {f g : Fin n → Int} (h : ∀ i, f i ≤ g i) :
sumFin n f ≤ sumFin n g := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
exact Int.add_le_add (h 0) (ih (fun i => h i.succ))
--% env 1
{"cmd": "def sumFin : (n : Nat) \u2192 (Fin n \u2192 Int) \u2192 Int\n | 0, _ => 0\n | n + 1, f => f 0 + sumFin n (fun i => f i.succ)\n\n@[simp] theorem sumFin_zero (f : Fin 0 \u2192 Int) : sumFin 0 f = 0 := rfl\n\n@[simp] theorem sumFin_succ (n : Nat) (f : Fin (n + 1) \u2192 Int) :\n sumFin (n + 1) f = f 0 + sumFin n (fun i => f i.succ) := rfl\n\n@[simp] theorem sumFin_zero_fun (n : Nat) :\n sumFin n (fun _ => (0 : Int)) = 0 := by\n induction n with\n | zero => simp\n | succ n ih => simp [ih]\n\n/-- La dominance ponctuelle se transf\u00e8re aux sommes. -/\ntheorem sumFin_mono {n : Nat} {f g : Fin n \u2192 Int} (h : \u2200 i, f i \u2264 g i) :\n sumFin n f \u2264 sumFin n g := by\n induction n with\n | zero => simp\n | succ n ih =>\n simp only [sumFin_succ]\n exact Int.add_le_add (h 0) (ih (fun i => h i.succ))\n", "env": 0}
{"env": 1}
Lecture de #eval 2 + 2 (cellule code[0]) :
#eval 2 + 2
#check NatPourquoi #eval au lieu de #reduce : #eval exécute la définition au niveau du runtime (interprète), tandis que #reduce applique les équations definissant réécrites (pure réduction). Pour 2 + 2, les deux donnent 4, mais #eval est plus rapide pour les entiers (hot path compile).
Pourquoi #check Nat : vérifie que Nat est dans le contexte et que son type est Type (le type des types dans Lean 4). C’est une sanity check que le kernel est correctement initialise. Si #check Nat échoue, le kernel n’a pas chargé Init.Prelude et il faut réinstaller Lean.
Sortie attendue :
4
Nat : TypeCoût : < 10 ms (kernel Lean nu).
Importance pédagogique : dans tout notebook Lean 4, la première cellule doit verifier que le kernel fonctionne (#eval 1 + 1 ou #check Nat). Si cette cellule échoue, tout le reste du notebook est compromis. C’est le “smoke test” du kernel.
BayesGame2 encode un jeu bayésien à deux joueurs, types et actions finis (Fin n), avec un prior commun non normalisé donné par des poids Nat (w t1 t2). Les utilités dépendent du profil de types complet et du profil d’actions. Les stratégies sont pures et contingentes au type ; interimU est l’utilité espérée interim (conditionnelle à son propre type). (Source : lean_game_defs_ext/Bayesian/Types.lean.)
structure BayesGame2 where
nT1 : Nat
nT2 : Nat
nA1 : Nat
nA2 : Nat
w : Fin nT1 → Fin nT2 → Nat
u1 : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int
u2 : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int
def Strategy1 (g : BayesGame2) := Fin g.nT1 → Fin g.nA1
def Strategy2 (g : BayesGame2) := Fin g.nT2 → Fin g.nA2
def interimU1 (g : BayesGame2) (t1 : Fin g.nT1) (a : Fin g.nA1)
(s2 : Strategy2 g) : Int :=
sumFin g.nT2 (fun t2 => (g.w t1 t2 : Int) * g.u1 t1 t2 a (s2 t2))
def interimU2 (g : BayesGame2) (t2 : Fin g.nT2) (a : Fin g.nA2)
(s1 : Strategy1 g) : Int :=
sumFin g.nT1 (fun t1 => (g.w t1 t2 : Int) * g.u2 t1 t2 (s1 t1) a)
def exAnteU1 (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Int :=
sumFin g.nT1 (fun t1 => interimU1 g t1 (s1 t1) s2)
def exAnteU2 (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Int :=
sumFin g.nT2 (fun t2 => interimU2 g t2 (s2 t2) s1)
structure BayesGame2 where
nT1 : Nat
nT2 : Nat
nA1 : Nat
nA2 : Nat
w : Fin nT1 → Fin nT2 → Nat
u1 : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int
u2 : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int
def Strategy1 (g : BayesGame2) := Fin g.nT1 → Fin g.nA1
def Strategy2 (g : BayesGame2) := Fin g.nT2 → Fin g.nA2
def interimU1 (g : BayesGame2) (t1 : Fin g.nT1) (a : Fin g.nA1)
(s2 : Strategy2 g) : Int :=
sumFin g.nT2 (fun t2 => (g.w t1 t2 : Int) * g.u1 t1 t2 a (s2 t2))
def interimU2 (g : BayesGame2) (t2 : Fin g.nT2) (a : Fin g.nA2)
(s1 : Strategy1 g) : Int :=
sumFin g.nT1 (fun t1 => (g.w t1 t2 : Int) * g.u2 t1 t2 (s1 t1) a)
def exAnteU1 (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Int :=
sumFin g.nT1 (fun t1 => interimU1 g t1 (s1 t1) s2)
def exAnteU2 (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Int :=
sumFin g.nT2 (fun t2 => interimU2 g t2 (s2 t2) s1)
--% env 2
{"cmd": "structure BayesGame2 where\n nT1 : Nat\n nT2 : Nat\n nA1 : Nat\n nA2 : Nat\n w : Fin nT1 \u2192 Fin nT2 \u2192 Nat\n u1 : Fin nT1 \u2192 Fin nT2 \u2192 Fin nA1 \u2192 Fin nA2 \u2192 Int\n u2 : Fin nT1 \u2192 Fin nT2 \u2192 Fin nA1 \u2192 Fin nA2 \u2192 Int\n\ndef Strategy1 (g : BayesGame2) := Fin g.nT1 \u2192 Fin g.nA1\ndef Strategy2 (g : BayesGame2) := Fin g.nT2 \u2192 Fin g.nA2\n\ndef interimU1 (g : BayesGame2) (t1 : Fin g.nT1) (a : Fin g.nA1)\n (s2 : Strategy2 g) : Int :=\n sumFin g.nT2 (fun t2 => (g.w t1 t2 : Int) * g.u1 t1 t2 a (s2 t2))\n\ndef interimU2 (g : BayesGame2) (t2 : Fin g.nT2) (a : Fin g.nA2)\n (s1 : Strategy1 g) : Int :=\n sumFin g.nT1 (fun t1 => (g.w t1 t2 : Int) * g.u2 t1 t2 (s1 t1) a)\n\ndef exAnteU1 (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Int :=\n sumFin g.nT1 (fun t1 => interimU1 g t1 (s1 t1) s2)\n\ndef exAnteU2 (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Int :=\n sumFin g.nT2 (fun t2 => interimU2 g t2 (s2 t2) s1)\n", "env": 1}
{"env": 2}
Lecture de sumFin (sommaire) (cellule code[1]) :
def sumFin : (n : Nat) → (Fin n → Int) → Int
| 0, _ => 0
| n + 1, f => f 0 + sumFin n (fun i => f i.succ)Pourquoi cette signature : sumFin : (n : Nat) → (Fin n → Int) → Int. On prend n : Nat (la taille de l’intervalle), puis une fonction f : Fin n → Int (les valeurs à sommer), et on retourne Int (la somme). Le tout est polymorphe en Int (on pourrait généraliser à α avec une structure additive, mais ici on spécialise pour éviter la dépendance Mathlib).
Pourquoi par induction sur n : la récurrence structurelle sur Nat est la maniere idiomatique de définir une somme finie en Lean 4 sans utiliser Mathlib.Algebra.BigOperators. Le cas de base n = 0 retourne 0 (somme vide), le cas récursif decompose en f 0 + sumFin n (f.shift).
Pourquoi Fin n plutôt que List : Fin n est une représentation type-safe des indices 0..n-1. Comparer Fin n → α à List α, Fin n garantit que la liste a exactement n éléments (pas plus, pas moins), ce qui élimine beaucoup de bugs (e.g., List.nth qui peut retourner Option au lieu de α).
Sortie attendue (avec #eval sumFin 5 (fun i => (i : Int) + 1)) : 15 (somme 1+2+3+4+5).
Coût : < 50 ms pour la compilation, < 10 ms pour #eval.
isBNE)Un profil de stratégies est un BNE si aucun type d’aucun joueur n’a de déviante d’action unilatérale profitable, en utilité interim. Les quantificateurs ne portent que sur des types Fin et des actions Fin de comparaisons Int décidables → la propriété est décidable (decide fonctionne sur les jeux concrets). (Source : lean_game_defs_ext/Bayesian/BNE.lean.)
@[reducible] def isBNE (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Prop :=
(∀ t1 : Fin g.nT1, ∀ a : Fin g.nA1,
interimU1 g t1 a s2 ≤ interimU1 g t1 (s1 t1) s2) ∧
(∀ t2 : Fin g.nT2, ∀ a : Fin g.nA2,
interimU2 g t2 a s1 ≤ interimU2 g t2 (s2 t2) s1)interimU1 g t1 a s2 est l’utilité interim du joueur 1 de type t1 pour l’action a face à la stratégie s2 (somme sur les types du joueur 2 pondérée par g.w, définition en code[2]) ; la conjonction isBNE exige que chaque type de chaque joueur joue une meilleure réponse interim.
Pourquoi @[reducible] : la définition est purement propositionnelle et doit être réduite par #decide ou #simp dans les preuves downstream. Sans @[reducible], Lean ne peut pas “déplier” isBNE dans une preuve automatique, et il faudrait des tactics manuelles.
Différence avec NE classique : dans un NE classique (jeu à information complète), chaque joueur maximise son utilité donnée la stratégie de l’autre. Dans un BNE, chaque joueur maximise son espérance d’utilité donnée la stratégie de l’autre et la distribution de ses propres types. Le BNE est donc “NE + probabilités sur les types”.
Sortie attendue (cellule code[3]) : la définition compilée, type BayesGame2 → Strategy1 → Strategy2 → Prop.
Coût : < 100 ms.
@[reducible] def isBNE (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Prop :=
(∀ t1 : Fin g.nT1, ∀ a : Fin g.nA1,
interimU1 g t1 a s2 ≤ interimU1 g t1 (s1 t1) s2) ∧
(∀ t2 : Fin g.nT2, ∀ a : Fin g.nA2,
interimU2 g t2 a s1 ≤ interimU2 g t2 (s2 t2) s1)
@[reducible] def isBNE (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Prop :=
(∀ t1 : Fin g.nT1, ∀ a : Fin g.nA1,
interimU1 g t1 a s2 ≤ interimU1 g t1 (s1 t1) s2) ∧
(∀ t2 : Fin g.nT2, ∀ a : Fin g.nA2,
interimU2 g t2 a s1 ≤ interimU2 g t2 (s2 t2) s1)
--% env 3
{"cmd": "@[reducible] def isBNE (g : BayesGame2) (s1 : Strategy1 g) (s2 : Strategy2 g) : Prop :=\n (\u2200 t1 : Fin g.nT1, \u2200 a : Fin g.nA1,\n interimU1 g t1 a s2 \u2264 interimU1 g t1 (s1 t1) s2) \u2227\n (\u2200 t2 : Fin g.nT2, \u2200 a : Fin g.nA2,\n interimU2 g t2 a s1 \u2264 interimU2 g t2 (s2 t2) s1)\n", "env": 2}
{"env": 3}
spaDeux enchérisseurs, valorisations et enchères dans Fin n, prior uniforme (poids 1). Le gagnant paie l’enchère du perdant (le second prix) ; les utilités sont mises à l’échelle par 2 pour que le partage d’égalité reste entier. Enchérer sa vraie valeur (spaTruthful) est la stratégie étudiée. (Source : lean_game_defs_ext/Bayesian/Vickrey.lean.)
@[reducible] def spa (n : Nat) : BayesGame2 where
nT1 := n
nT2 := n
nA1 := n
nA2 := n
w := fun _ _ => 1
u1 := fun v1 _ b1 b2 =>
if b2.val < b1.val then 2 * ((v1.val : Int) - b2.val)
else if b1.val = b2.val then (v1.val : Int) - b2.val
else 0
u2 := fun _ v2 b1 b2 =>
if b1.val < b2.val then 2 * ((v2.val : Int) - b1.val)
else if b1.val = b2.val then (v2.val : Int) - b1.val
else 0
/-- Enchère honnête (joueur 1) : bid = valeur. -/
@[reducible] def spaTruthful1 (n : Nat) : Strategy1 (spa n) := fun v => v
/-- Enchère honnête (joueur 2). -/
@[reducible] def spaTruthful2 (n : Nat) : Strategy2 (spa n) := fun v => v
@[reducible] def spa (n : Nat) : BayesGame2 where
nT1 := n
nT2 := n
nA1 := n
nA2 := n
w := fun _ _ => 1
u1 := fun v1 _ b1 b2 =>
if b2.val < b1.val then 2 * ((v1.val : Int) - b2.val)
else if b1.val = b2.val then (v1.val : Int) - b2.val
else 0
u2 := fun _ v2 b1 b2 =>
if b1.val < b2.val then 2 * ((v2.val : Int) - b1.val)
else if b1.val = b2.val then (v2.val : Int) - b1.val
else 0
/-- Enchère honnête (joueur 1) : bid = valeur. -/
@[reducible] def spaTruthful1 (n : Nat) : Strategy1 (spa n) := fun v => v
/-- Enchère honnête (joueur 2). -/
@[reducible] def spaTruthful2 (n : Nat) : Strategy2 (spa n) := fun v => v
--% env 4
{"cmd": "@[reducible] def spa (n : Nat) : BayesGame2 where\n nT1 := n\n nT2 := n\n nA1 := n\n nA2 := n\n w := fun _ _ => 1\n u1 := fun v1 _ b1 b2 =>\n if b2.val < b1.val then 2 * ((v1.val : Int) - b2.val)\n else if b1.val = b2.val then (v1.val : Int) - b2.val\n else 0\n u2 := fun _ v2 b1 b2 =>\n if b1.val < b2.val then 2 * ((v2.val : Int) - b1.val)\n else if b1.val = b2.val then (v2.val : Int) - b1.val\n else 0\n\n/-- Ench\u00e8re honn\u00eate (joueur 1) : bid = valeur. -/\n@[reducible] def spaTruthful1 (n : Nat) : Strategy1 (spa n) := fun v => v\n\n/-- Ench\u00e8re honn\u00eate (joueur 2). -/\n@[reducible] def spaTruthful2 (n : Nat) : Strategy2 (spa n) := fun v => v\n", "env": 3}
{"env": 4}
L’argument classique de Vickrey : enchérir sa vraie valeur domine faiblement toute autre enchère, point par point — contre n’importe quelle enchère adverse, dans n’importe quel état. Quel que soit le prix (l’enchère adverse), dévier de v ne peut que forfaiter un gain profitable (b1 < v) ou acheter à perte (b1 > v), jamais améliorer — car le prix payé ne dépend pas de sa propre enchère. La dominance ponctuelle se transfère ensuite à l’utilité interim via sumFin_mono. Pourquoi « faiblement » : l’inégalité est large — quand l’enchère adverse vaut exactement v, toute enchère ≤ v fait aussi bien, la dominance n’est donc pas stricte.
Implémentation Lean (cellule code[5]) : dominance ponctuelle puis transfert interim : - spa_truthful_dominant1 / spa_truthful_dominant2 : (spa n).u1 v t2 b1 b2 ≤ (spa n).u1 v t2 v b2 (dépliage simp only [spa], repeat' split, close par omega) ; - spa_interim_best1 / spa_interim_best2 : transfert de la dominance ponctuelle à l’utilité interim via sumFin_mono.
Référence : Vickrey (1961), section “Optimal strategy in second-price auctions”.
Sortie attendue : les quatre théorèmes compilent ; preuves restatées du lake lean_game_defs_ext/ (0 sorry).
Coût : < 100 ms.
/-- Vickrey dominance, joueur 1 : la vraie valeur domine faiblement toute autre enchère.
On déplie `spa` explicitement via `simp only [spa]` (au lieu d'un `show` defeq)
pour rester robuste aux variations d'élaboration defeq entre versions de Lean ;
la preuve est identique à celle du lake (case analysis sur qui gagne, close par `omega`).
NB : le linter signale « simp argument unused: spa » — faux positif connu :
`simp` déplie effectivement `spa` (nécessaire pour que `split` voie les `if`),
mais ne le compte pas comme règle de réécriture. -/
theorem spa_truthful_dominant1 (n : Nat) (v t2 b1 b2 : Fin n) :
(spa n).u1 v t2 b1 b2 ≤ (spa n).u1 v t2 v b2 := by
simp only [spa]
repeat' split
all_goals omega
/-- Vickrey dominance, joueur 2 (symétrique). -/
theorem spa_truthful_dominant2 (n : Nat) (t1 v b1 b2 : Fin n) :
(spa n).u2 t1 v b1 b2 ≤ (spa n).u2 t1 v b1 v := by
simp only [spa]
repeat' split
all_goals omega
/-- La dominance ponctuelle => meilleure réponse interim (joueur 1). -/
theorem spa_interim_best1 (n : Nat) (v a : Fin n) (s2 : Strategy2 (spa n)) :
interimU1 (spa n) v a s2 ≤ interimU1 (spa n) v (spaTruthful1 n v) s2 := by
apply sumFin_mono
intro t2
exact Int.mul_le_mul_of_nonneg_left
(spa_truthful_dominant1 n v t2 a (s2 t2)) (by omega)
/-- Meilleure réponse interim, joueur 2. -/
theorem spa_interim_best2 (n : Nat) (v a : Fin n) (s1 : Strategy1 (spa n)) :
interimU2 (spa n) v a s1 ≤ interimU2 (spa n) v (spaTruthful2 n v) s1 := by
apply sumFin_mono
intro t1
exact Int.mul_le_mul_of_nonneg_left
(spa_truthful_dominant2 n t1 v (s1 t1) a) (by omega)
/-- Vickrey dominance, joueur 1 : la vraie valeur domine faiblement toute autre enchère.
On déplie `spa` explicitement via `simp only [spa]` (au lieu d'un `show` defeq)
pour rester robuste aux variations d'élaboration defeq entre versions de Lean ;
la preuve est identique à celle du lake (case analysis sur qui gagne, close par `omega`).
NB : le linter signale « simp argument unused: spa » — faux positif connu :
`simp` déplie effectivement `spa` (nécessaire pour que `split` voie les `if`),
mais ne le compte pas comme règle de réécriture. -/
theorem spa_truthful_dominant1 (n : Nat) (v t2 b1 b2 : Fin n) :
(spa n).u1 v t2 b1 b2 ≤ (spa n).u1 v t2 v b2 := by
🟨 This simp argument is unused:
spa
Hint: Omit it from the simp argument list.
simp only ̵[̵s̵p̵a̵]̵
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
repeat' split
all_goals omega
/-- Vickrey dominance, joueur 2 (symétrique). -/
theorem spa_truthful_dominant2 (n : Nat) (t1 v b1 b2 : Fin n) :
(spa n).u2 t1 v b1 b2 ≤ (spa n).u2 t1 v b1 v := by
🟨 This simp argument is unused:
spa
Hint: Omit it from the simp argument list.
simp only ̵[̵s̵p̵a̵]̵
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
repeat' split
all_goals omega
/-- La dominance ponctuelle => meilleure réponse interim (joueur 1). -/
theorem spa_interim_best1 (n : Nat) (v a : Fin n) (s2 : Strategy2 (spa n)) :
interimU1 (spa n) v a s2 ≤ interimU1 (spa n) v (spaTruthful1 n v) s2 := by
apply sumFin_mono
intro t2
exact Int.mul_le_mul_of_nonneg_left
(spa_truthful_dominant1 n v t2 a (s2 t2)) (by omega)
/-- Meilleure réponse interim, joueur 2. -/
theorem spa_interim_best2 (n : Nat) (v a : Fin n) (s1 : Strategy1 (spa n)) :
interimU2 (spa n) v a s1 ≤ interimU2 (spa n) v (spaTruthful2 n v) s1 := by
apply sumFin_mono
intro t1
exact Int.mul_le_mul_of_nonneg_left
(spa_truthful_dominant2 n t1 v (s1 t1) a) (by omega)
--% env 5
{"cmd": "/-- Vickrey dominance, joueur 1 : la vraie valeur domine faiblement toute autre ench\u00e8re.\n On d\u00e9plie `spa` explicitement via `simp only [spa]` (au lieu d'un `show` defeq)\n pour rester robuste aux variations d'\u00e9laboration defeq entre versions de Lean ;\n la preuve est identique \u00e0 celle du lake (case analysis sur qui gagne, close par `omega`).\n NB : le linter signale \u00ab simp argument unused: spa \u00bb \u2014 faux positif connu :\n `simp` d\u00e9plie effectivement `spa` (n\u00e9cessaire pour que `split` voie les `if`),\n mais ne le compte pas comme r\u00e8gle de r\u00e9\u00e9criture. -/\ntheorem spa_truthful_dominant1 (n : Nat) (v t2 b1 b2 : Fin n) :\n (spa n).u1 v t2 b1 b2 \u2264 (spa n).u1 v t2 v b2 := by\n simp only [spa]\n repeat' split\n all_goals omega\n\n/-- Vickrey dominance, joueur 2 (sym\u00e9trique). -/\ntheorem spa_truthful_dominant2 (n : Nat) (t1 v b1 b2 : Fin n) :\n (spa n).u2 t1 v b1 b2 \u2264 (spa n).u2 t1 v b1 v := by\n simp only [spa]\n repeat' split\n all_goals omega\n\n/-- La dominance ponctuelle => meilleure r\u00e9ponse interim (joueur 1). -/\ntheorem spa_interim_best1 (n : Nat) (v a : Fin n) (s2 : Strategy2 (spa n)) :\n interimU1 (spa n) v a s2 \u2264 interimU1 (spa n) v (spaTruthful1 n v) s2 := by\n apply sumFin_mono\n intro t2\n exact Int.mul_le_mul_of_nonneg_left\n (spa_truthful_dominant1 n v t2 a (s2 t2)) (by omega)\n\n/-- Meilleure r\u00e9ponse interim, joueur 2. -/\ntheorem spa_interim_best2 (n : Nat) (v a : Fin n) (s1 : Strategy1 (spa n)) :\n interimU2 (spa n) v a s1 \u2264 interimU2 (spa n) v (spaTruthful2 n v) s1 := by\n apply sumFin_mono\n intro t1\n exact Int.mul_le_mul_of_nonneg_left\n (spa_truthful_dominant2 n t1 v (s1 t1) a) (by omega)\n", "env": 4}
{"messages":
[{"severity": "warning",
"pos": {"line": 10, "column": 13},
"endPos": {"line": 10, "column": 16},
"data":
"This simp argument is unused:\n spa\n\nHint: Omit it from the simp argument list.\n simp only ̵[̵s̵p̵a̵]̵\n\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`"},
{"severity": "warning",
"pos": {"line": 17, "column": 13},
"endPos": {"line": 17, "column": 16},
"data":
"This simp argument is unused:\n spa\n\nHint: Omit it from the simp argument list.\n simp only ̵[̵s̵p̵a̵]̵\n\nNote: This linter can be disabled with `set_option linter.unusedSimpArgs false`"}],
"env": 5}
Lecture de BayesGame2 (jeu bayésien fini à 2 joueurs) (cellule code[2]) :
structure BayesGame2 where
nT1 : Nat
nT2 : Nat
nA1 : Nat
nA2 : Nat
w : Fin nT1 → Fin nT2 → Nat
u1 : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int
u2 : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int
def Strategy1 (g : BayesGame2) := Fin g.nT1 → Fin g.nA1
def Strategy2 (g : BayesGame2) := Fin g.nT2 → Fin g.nA2Pourquoi cette structure : w : Fin nT1 → Fin nT2 → Nat est le prior commun non normalisé (poids Nat), u1/u2 les utilités des deux joueurs — chacune dépend du profil de types complet et du profil d’actions. interimU1/interimU2 (même cellule) sont les utilités espérées interim, exAnteU1/exAnteU2 les versions ex-ante.
Pourquoi Fin n partout : comme pour sumFin, Fin n est la représentation type-safe des indices. Cela garantit que w : Fin nT1 → Fin nT2 → Fin nA1 → Fin nA2 → Int est totalement définie sur les nT1 * nT2 * nA1 * nA2 cas.
Le prior comme distribution : w t1 t2 est un poids relatif (pas nécessairement une probabilité). Pour la vraisemblance bayésienne, on peut renormaliser : P(t1, t2) = w t1 t2 / Σ w t1' t2'. Cette séparation « poids brut vs probabilité normalisée » est commode pour les preuves.
Référence : Harsanyi (1967), formalisation des jeux à information incomplète.
Sortie attendue : la structure compilée, accessible par g.nT1, g.w, etc.
Coût : < 100 ms.
Le profil d’enchères honnêtes est un équilibre bayésien de Nash de l’enchère au second prix, pour TOUT n. Théorème général — sans decide, sans vérification d’instance — ce qui contraste avec l’enchère au premier prix, où l’enchère honnête n’est PAS un BNE (cf. Auction.lean dans le lake). La preuve combine les deux meilleures réponses interim ci-dessus dans la conjonction isBNE.
Implications profondes : 1. Truthfulness : un vendeur peut collecter les vraies valuations des acheteurs sans incitation à mentir. 2. Efficacité : l’objet va au joueur qui le valorise le plus (l’enchérisseur avec v le plus élevé gagne). 3. Revenue : le vendeur obtient le second prix, qui est inférieur à la max valuation – donc il peut être préférable d’utiliser d’autres mécanismes (cf Myerson 1981).
Implémentation Lean (cellule code[6]) : le théorème spa_truthful_bne est prouvé dans le notebook — la conjonction isBNE est close par les deux meilleures réponses interim spa_interim_best1/spa_interim_best2 (établies en 4.1), exactement comme dans le lake lean_game_defs_ext/ (restaté verbatim, 0 sorry).
Référence : Vickrey (1961) + Myerson (1981) “Optimal Auction Design”, Mathematics of Operations Research 6(1).
Sortie attendue : #check spa_truthful_bne : spa_truthful_bne (n : Nat) : isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n).
Coût : < 100 ms.
/-- **Théorème de Vickrey** (fini, deux enchérisseurs) : le profil honnête est un BNE pour tout n. -/
theorem spa_truthful_bne (n : Nat) :
isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n) :=
⟨fun t1 a => spa_interim_best1 n t1 a (spaTruthful2 n),
fun t2 a => spa_interim_best2 n t2 a (spaTruthful1 n)⟩
#check spa_truthful_bne
/-- **Théorème de Vickrey** (fini, deux enchérisseurs) : le profil honnête est un BNE pour tout n. -/
theorem spa_truthful_bne (n : Nat) :
isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n) :=
⟨fun t1 a => spa_interim_best1 n t1 a (spaTruthful2 n),
fun t2 a => spa_interim_best2 n t2 a (spaTruthful1 n)⟩
spa_truthful_bne (n : Nat) : isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n)
--% env 6
{"cmd": "/-- **Th\u00e9or\u00e8me de Vickrey** (fini, deux ench\u00e9risseurs) : le profil honn\u00eate est un BNE pour tout n. -/\ntheorem spa_truthful_bne (n : Nat) :\n isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n) :=\n \u27e8fun t1 a => spa_interim_best1 n t1 a (spaTruthful2 n),\n fun t2 a => spa_interim_best2 n t2 a (spaTruthful1 n)\u27e9\n\n#check spa_truthful_bne\n", "env": 5}
{"messages":
[{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"spa_truthful_bne (n : Nat) : isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n)"}],
"env": 6}
À l’équilibre honnête Vickrey avec valorisations {0, 1, 2}, le type haut gagne une utilité interim strictement positive (rente d’information concrète = 6 à l’échelle : gagne en payant 0 puis 1 contre les types bas, égalité à 2 pour un surplus nul). La décidabilité de isBNE (quantificateurs sur Fin de comparaisons Int) permet de le prouver par decide sur cette instance concrète.
Implémentation Lean (cellule code[7]) : kernel-décidée — spa_truthful_pos_three prouve 0 < interimU1 (spa 3) ⟨2, by decide⟩ (spaTruthful1 3 ⟨2, by decide⟩) (spaTruthful2 3) par decide, et le #eval final renvoie la valeur concrète : 6.
Pourquoi c’est décidable en kernel : pour des instances finies de BayesGame2 (nT1, nT2, nA1, nA2 tous petits, disons <= 3), le nombre de profils de stratégies est (nA1^nT1) * (nA2^nT2) – exponentiel mais petit. #decide peut énumérer exhaustivement.
Pourquoi c’est important pédagogiquement : la rente d’information Vickrey est un invariant subtil qui ne tient pas pour tous les mécanismes d’enchères (cf l’enchère anglaise ou hollandaise). C’est une frontière nette entre “mécanismes truthfulness-préservants” et “mécanismes avec rente informationnelle”.
Référence : Vickrey (1961) + Maskin-Riley (2003) “Uniqueness of equilibrium in sealed high-bid auctions”, Games and Economic Behavior 45(2).
Sortie attendue : #eval interimU1 (spa 3) (2 : Fin 3) (spaTruthful1 3 (2 : Fin 3)) (spaTruthful2 3) : 6 (rente à l’échelle : gagne en payant 0 puis 1 contre les types bas, égalité à 2 pour un surplus nul).
Coût : < 100 ms.
/-- Le type haut garde une rente d'information strictement positive (instance concrète décidable). -/
theorem spa_truthful_pos_three :
0 < interimU1 (spa 3) ⟨2, by decide⟩
(spaTruthful1 3 ⟨2, by decide⟩) (spaTruthful2 3) := by
decide
-- Valeur concrète de l'utilité interim du type haut (valuations {0,1,2}) :
#eval interimU1 (spa 3) (2 : Fin 3) (spaTruthful1 3 (2 : Fin 3)) (spaTruthful2 3)
/-- Le type haut garde une rente d'information strictement positive (instance concrète décidable). -/
theorem spa_truthful_pos_three :
0 < interimU1 (spa 3) ⟨2, by decide⟩
(spaTruthful1 3 ⟨2, by decide⟩) (spaTruthful2 3) := by
decide
-- Valeur concrète de l'utilité interim du type haut (valuations {0,1,2}) :
6
--% env 7
{"cmd": "/-- Le type haut garde une rente d'information strictement positive (instance concr\u00e8te d\u00e9cidable). -/\ntheorem spa_truthful_pos_three :\n 0 < interimU1 (spa 3) \u27e82, by decide\u27e9\n (spaTruthful1 3 \u27e82, by decide\u27e9) (spaTruthful2 3) := by\n decide\n\n-- Valeur concr\u00e8te de l'utilit\u00e9 interim du type haut (valuations {0,1,2}) :\n#eval interimU1 (spa 3) (2 : Fin 3) (spaTruthful1 3 (2 : Fin 3)) (spaTruthful2 3)\n", "env": 6}
{"messages":
[{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 5},
"data": "6"}],
"env": 7}
Lecture de la dominance de Vickrey (cellule code[5]) :
/-- Vickrey dominance, joueur 1 : la vraie valeur domine faiblement toute autre enchère.
On déplie `spa` explicitement via `simp only [spa]` (au lieu d'un `show` defeq)
pour rester robuste aux variations d'élaboration defeq entre versions de Lean ;
la preuve est identique à celle du lake (case analysis sur qui gagne, close par `omega`).
NB : le linter signale « simp argument unused: spa » — faux positif connu :
`simp` déplie effectivement `spa` (nécessaire pour que `split` voie les `if`),
mais ne le compte pas comme règle de réécriture. -/
theorem spa_truthful_dominant1 (n : Nat) (v t2 b1 b2 : Fin n) :
(spa n).u1 v t2 b1 b2 ≤ (spa n).u1 v t2 v b2 := by
simp only [spa]
repeat' split
all_goals omegaPourquoi cette signature : (spa n).u1 v t2 b1 b2 est l’utilité du joueur 1 (vraie valeur v, type adverse t2) quand il enchérit b1 contre l’enchère adverse b2 — l’énoncé dit qu’elle est maximale en b1 = v, quels que soient t2 et b2 : le prix payé (le second prix b2) ne dépend pas de sa propre enchère.
Pourquoi « dominance faible » : l’inégalité est large (≤) — quand b2 = v, toute enchère b1 ≤ v fait aussi bien.
Le théorème symétrique spa_truthful_dominant2 (même cellule) couvre le joueur 2 ; les deux transferts interim (spa_interim_best1/spa_interim_best2) assemblent la dominance dans spa_truthful_bne (section 4.2).
Référence : Vickrey (1961), section “Optimal strategy”.
Sortie attendue : les quatre théorèmes compilent (preuves simp only [spa] + repeat' split + all_goals omega, restatées du lake).
Coût : < 100 ms.
Le second résultat majeur du lake lean_game_defs_ext est la valeur de l’information pour un décideur seul (Blackwell). Un décideur fait face à un ensemble fini d’états (prior Nat non normalisé, même encodage que BayesGame2) et choisit une action. Un signal déterministe σ est une application des états vers des réalisations — autrement dit, une partition finie de l’espace d’états. On compare trois valeurs de référence :
valueNoInfo : choisir une seule action avant toute information ;valueSignal σ : observer la réalisation de σ, puis choisir optimalement dans chaque cellule de la partition ;valuePerfect : connaître l’état exact, puis choisir.Les théorèmes ci-dessous (prouvés sans sorry dans Information.lean, restatés ici pour exécution dans le kernel) disent que l’information ne nuit jamais à un décideur seul : tout signal vaut au moins valueNoInfo, et un signal plus fin (σ = h ∘ τ) vaut au moins autant que son raffinement. (Source : lean_game_defs_ext/Bayesian/Information.lean, phase 4 de #2610.)
Subtilité importante : ce résultat vaut en décision mono-joueur (pas en jeu). En jeu, comme on le verra section 6, l’information peut nuire (par exemple, si elle change la stratégie d’un adversaire qui réagissait favorablement).
Implémentation Lean (cellules code[11-13]) : trois théorèmes, restatés verbatim du lake (Information.lean, 0 sorry) : - valueSignal_const : le signal totalement non informatif (unique réalisation) vaut exactement valueNoInfo ; - valueSignal_mono (résultat amiral) : si σ = h ∘ τ (σ est un grossissement de τ), observer le signal plus fin τ vaut au moins autant que σ ; - valueNoInfo_le_valueSignal : tout signal vaut au moins valueNoInfo — l’information ne nuit jamais à un décideur seul.
Référence : Blackwell (1951) “Comparison of Experiments”, Proc. 2nd Berkeley Symp. Math. Statist. Probab.
Sortie attendue (cellules code[11-13]) : les trois théorèmes compilent (#check valueSignal_mono en sortie), preuves complètes sans sorry.
Coût : < 200 ms (3 théorèmes + infrastructure).
Avant de prouver Blackwell, deux batteries d’infrastructure restatées verbatim du lake : maxFin et ses lemmes (cellule code[8]), puis les lemmes de sommation manquants (cellules code[8-9]).
/-- Maximum of `f` over all of `Fin (n + 1)` (nonempty domain), by
structural recursion on `n`. -/
def maxFin : (n : Nat) → (Fin (n + 1) → Int) → Int
| 0, f => f 0
| n + 1, f => max (f 0) (maxFin n (fun i => f i.succ))Le domaine est non vide : maxFin est défini sur Fin (n + 1) — cas de base 0, f => f 0 ; il n’y a pas de convention « maximum sur ensemble vide ».
Lemmes (cellule code[8]) : le_maxFin (tout élément est majoré par le max), maxFin_le (le max est majoré par toute borne ponctuelle), maxFin_zero_fun, maxFin_if_distrib, et le lemme maître maxFin_sumFin_le : le max d’une somme est au plus la somme des maxima groupwise — choisir l’action optimale par groupe bat choisir une action unique pour tous les groupes.
Lemmes de sommation (cellules code[8-9]) : sumFin_congr, sumFin_add, sumFin_comm (Fubini fini), sumFin_if_distrib, sumFin_single, sumFin_partition.
Pourquoi réinventer localement : restatées de lean_game_defs_ext/Bayesian/Max.lean et Sum.lean — le kernel nu n’embarque pas Mathlib (plusieurs Go d’.olean, charge lourde) ; ces définitions courtes suffisent aux preuves de Blackwell.
Coût : < 100 ms pour définir ; < 100 ms pour #eval.
-- Infrastructure (1/2) : maximum fini `maxFin` et ses lemmes.
-- (Source : Max.lean, restates verbatim. Requis pour definir les valeurs
-- valueNoInfo / valueSignal / valuePerfect et la monotonie de Blackwell.)
/-- Maximum of `f` over all of `Fin (n + 1)` (nonempty domain), by
structural recursion on `n`. -/
def maxFin : (n : Nat) → (Fin (n + 1) → Int) → Int
| 0, f => f 0
| n + 1, f => max (f 0) (maxFin n (fun i => f i.succ))
@[simp] theorem maxFin_zero (f : Fin 1 → Int) : maxFin 0 f = f 0 := rfl
@[simp] theorem maxFin_succ (n : Nat) (f : Fin (n + 2) → Int) :
maxFin (n + 1) f = max (f 0) (maxFin n (fun i => f i.succ)) := rfl
-- Tout element est majore par le maximum.
/-- Every value of `f` is at most its maximum. -/
theorem le_maxFin : ∀ {n : Nat} (f : Fin (n + 1) → Int) (i : Fin (n + 1)),
f i ≤ maxFin n f
| 0, f, i => by
cases i using Fin.cases with
| zero => exact Int.le_refl _
| succ j => exact j.elim0
| n + 1, f, i => by
cases i using Fin.cases with
| zero =>
simp only [maxFin_succ]
omega
| succ j =>
have h := le_maxFin (fun i => f i.succ) j
simp only [maxFin_succ]
omega
-- Le maximum est majore par toute borne ponctuelle.
/-- The maximum is at most any pointwise upper bound. -/
theorem maxFin_le : ∀ {n : Nat} {f : Fin (n + 1) → Int} {b : Int},
(∀ i, f i ≤ b) → maxFin n f ≤ b
| 0, _, _, h => h 0
| n + 1, f, b, h => by
have h1 := h 0
have h2 := maxFin_le (f := fun i => f i.succ) (fun i => h i.succ)
simp only [maxFin_succ]
omega
/-- The maximum of the zero function vanishes. -/
@[simp] theorem maxFin_zero_fun (n : Nat) :
maxFin n (fun _ => (0 : Int)) = 0 := by
induction n with
| zero => rfl
| succ n ih => simp [ih]
-- **Lemme maitre** : le max d'une somme est au plus la somme des maxima
-- groupwise ( choisir l'action optimale par groupe bat choisir une action
-- unique pour tous les groupes ).
/-- Master lemma: the max of a sum is at most the sum of the groupwise
maxima. Choosing one action `a` for every group `j` at once cannot
beat choosing the best action separately inside each group. -/
theorem maxFin_sumFin_le {nA m : Nat} (F : Fin m → Fin (nA + 1) → Int) :
maxFin nA (fun a => sumFin m (fun j => F j a)) ≤
sumFin m (fun j => maxFin nA (fun a => F j a)) :=
maxFin_le (fun a => sumFin_mono (fun j => le_maxFin (F j) a))
-- Un `if` dont la condition ne depend pas de l'index sort du maximum.
/-- An `if` whose condition does not depend on the index pulls out of
the maximum (the `else 0` branch matches the zero function). -/
theorem maxFin_if_distrib {n : Nat} (c : Prop) [Decidable c]
(f : Fin (n + 1) → Int) :
maxFin n (fun a => if c then f a else 0) = if c then maxFin n f else 0 := by
by_cases h : c <;> simp [h]
#check maxFin_sumFin_le-- Infrastructure (1/2) : maximum fini `maxFin` et ses lemmes.
-- (Source : Max.lean, restates verbatim. Requis pour definir les valeurs
-- valueNoInfo / valueSignal / valuePerfect et la monotonie de Blackwell.)
/-- Maximum of `f` over all of `Fin (n + 1)` (nonempty domain), by
structural recursion on `n`. -/
def maxFin : (n : Nat) → (Fin (n + 1) → Int) → Int
| 0, f => f 0
| n + 1, f => max (f 0) (maxFin n (fun i => f i.succ))
@[simp] theorem maxFin_zero (f : Fin 1 → Int) : maxFin 0 f = f 0 := rfl
@[simp] theorem maxFin_succ (n : Nat) (f : Fin (n + 2) → Int) :
maxFin (n + 1) f = max (f 0) (maxFin n (fun i => f i.succ)) := rfl
-- Tout element est majore par le maximum.
/-- Every value of `f` is at most its maximum. -/
theorem le_maxFin : ∀ {n : Nat} (f : Fin (n + 1) → Int) (i : Fin (n + 1)),
f i ≤ maxFin n f
| 0, f, i => by
cases i using Fin.cases with
| zero => exact Int.le_refl _
| succ j => exact j.elim0
| n + 1, f, i => by
cases i using Fin.cases with
| zero =>
simp only [maxFin_succ]
omega
| succ j =>
have h := le_maxFin (fun i => f i.succ) j
simp only [maxFin_succ]
omega
-- Le maximum est majore par toute borne ponctuelle.
/-- The maximum is at most any pointwise upper bound. -/
theorem maxFin_le : ∀ {n : Nat} {f : Fin (n + 1) → Int} {b : Int},
(∀ i, f i ≤ b) → maxFin n f ≤ b
| 0, _, _, h => h 0
| n + 1, f, b, h => by
have h1 := h 0
have h2 := maxFin_le (f := fun i => f i.succ) (fun i => h i.succ)
simp only [maxFin_succ]
omega
/-- The maximum of the zero function vanishes. -/
@[simp] theorem maxFin_zero_fun (n : Nat) :
maxFin n (fun _ => (0 : Int)) = 0 := by
induction n with
| zero => rfl
| succ n ih => simp [ih]
-- **Lemme maitre** : le max d'une somme est au plus la somme des maxima
-- groupwise ( choisir l'action optimale par groupe bat choisir une action
-- unique pour tous les groupes ).
/-- Master lemma: the max of a sum is at most the sum of the groupwise
maxima. Choosing one action `a` for every group `j` at once cannot
beat choosing the best action separately inside each group. -/
theorem maxFin_sumFin_le {nA m : Nat} (F : Fin m → Fin (nA + 1) → Int) :
maxFin nA (fun a => sumFin m (fun j => F j a)) ≤
sumFin m (fun j => maxFin nA (fun a => F j a)) :=
maxFin_le (fun a => sumFin_mono (fun j => le_maxFin (F j) a))
-- Un `if` dont la condition ne depend pas de l'index sort du maximum.
/-- An `if` whose condition does not depend on the index pulls out of
the maximum (the `else 0` branch matches the zero function). -/
theorem maxFin_if_distrib {n : Nat} (c : Prop) [Decidable c]
(f : Fin (n + 1) → Int) :
maxFin n (fun a => if c then f a else 0) = if c then maxFin n f else 0 := by
by_cases h : c <;> simp [h]
maxFin_sumFin_le {nA m : Nat} (F : Fin m → Fin (nA + 1) → Int) :
(maxFin nA fun a => sumFin m fun j => F j a) ≤ sumFin m fun j => maxFin nA fun a => F j a
--% env 8
{"cmd": "-- Infrastructure (1/2) : maximum fini `maxFin` et ses lemmes.\n-- (Source : Max.lean, restates verbatim. Requis pour definir les valeurs\n-- valueNoInfo / valueSignal / valuePerfect et la monotonie de Blackwell.)\n\n/-- Maximum of `f` over all of `Fin (n + 1)` (nonempty domain), by\n structural recursion on `n`. -/\ndef maxFin : (n : Nat) \u2192 (Fin (n + 1) \u2192 Int) \u2192 Int\n | 0, f => f 0\n | n + 1, f => max (f 0) (maxFin n (fun i => f i.succ))\n\n@[simp] theorem maxFin_zero (f : Fin 1 \u2192 Int) : maxFin 0 f = f 0 := rfl\n\n@[simp] theorem maxFin_succ (n : Nat) (f : Fin (n + 2) \u2192 Int) :\n maxFin (n + 1) f = max (f 0) (maxFin n (fun i => f i.succ)) := rfl\n\n-- Tout element est majore par le maximum.\n/-- Every value of `f` is at most its maximum. -/\ntheorem le_maxFin : \u2200 {n : Nat} (f : Fin (n + 1) \u2192 Int) (i : Fin (n + 1)),\n f i \u2264 maxFin n f\n | 0, f, i => by\n cases i using Fin.cases with\n | zero => exact Int.le_refl _\n | succ j => exact j.elim0\n | n + 1, f, i => by\n cases i using Fin.cases with\n | zero =>\n simp only [maxFin_succ]\n omega\n | succ j =>\n have h := le_maxFin (fun i => f i.succ) j\n simp only [maxFin_succ]\n omega\n\n-- Le maximum est majore par toute borne ponctuelle.\n/-- The maximum is at most any pointwise upper bound. -/\ntheorem maxFin_le : \u2200 {n : Nat} {f : Fin (n + 1) \u2192 Int} {b : Int},\n (\u2200 i, f i \u2264 b) \u2192 maxFin n f \u2264 b\n | 0, _, _, h => h 0\n | n + 1, f, b, h => by\n have h1 := h 0\n have h2 := maxFin_le (f := fun i => f i.succ) (fun i => h i.succ)\n simp only [maxFin_succ]\n omega\n\n/-- The maximum of the zero function vanishes. -/\n@[simp] theorem maxFin_zero_fun (n : Nat) :\n maxFin n (fun _ => (0 : Int)) = 0 := by\n induction n with\n | zero => rfl\n | succ n ih => simp [ih]\n\n-- **Lemme maitre** : le max d'une somme est au plus la somme des maxima\n-- groupwise ( choisir l'action optimale par groupe bat choisir une action\n-- unique pour tous les groupes ).\n/-- Master lemma: the max of a sum is at most the sum of the groupwise\n maxima. Choosing one action `a` for every group `j` at once cannot\n beat choosing the best action separately inside each group. -/\ntheorem maxFin_sumFin_le {nA m : Nat} (F : Fin m \u2192 Fin (nA + 1) \u2192 Int) :\n maxFin nA (fun a => sumFin m (fun j => F j a)) \u2264\n sumFin m (fun j => maxFin nA (fun a => F j a)) :=\n maxFin_le (fun a => sumFin_mono (fun j => le_maxFin (F j) a))\n\n-- Un `if` dont la condition ne depend pas de l'index sort du maximum.\n/-- An `if` whose condition does not depend on the index pulls out of\n the maximum (the `else 0` branch matches the zero function). -/\ntheorem maxFin_if_distrib {n : Nat} (c : Prop) [Decidable c]\n (f : Fin (n + 1) \u2192 Int) :\n maxFin n (fun a => if c then f a else 0) = if c then maxFin n f else 0 := by\n by_cases h : c <;> simp [h]\n\n#check maxFin_sumFin_le", "env": 7}
{"messages":
[{"severity": "info",
"pos": {"line": 71, "column": 0},
"endPos": {"line": 71, "column": 6},
"data":
"maxFin_sumFin_le {nA m : Nat} (F : Fin m → Fin (nA + 1) → Int) :\n (maxFin nA fun a => sumFin m fun j => F j a) ≤ sumFin m fun j => maxFin nA fun a => F j a"}],
"env": 8}
-- Infrastructure (2/2) : lemmes de sommation `sumFin` manquants
-- (le notebook a deja sumFin + sumFin_zero/succ/zero_fun/mono en section 1 ;
-- on ajoute ici les lemmes requis par les preuves de Blackwell).
-- Fonctions ponctuellement egales => sommes egales.
/-- Pointwise equal functions have equal sums. -/
theorem sumFin_congr {n : Nat} {f g : Fin n → Int} (h : ∀ i, f i = g i) :
sumFin n f = sumFin n g := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
rw [h 0, ih (fun i => h i.succ)]
-- Somme de deux fonctions = somme des sommes (requis par sumFin_comm).
/-- Sums distribute over pointwise addition. -/
theorem sumFin_add {n : Nat} (f g : Fin n → Int) :
sumFin n (fun i => f i + g i) = sumFin n f + sumFin n g := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
rw [ih]
omega
-- Double somme commute (Fubini fini).
/-- Double sums commute (Fubini for finite sums). -/
theorem sumFin_comm {n m : Nat} (F : Fin n → Fin m → Int) :
sumFin n (fun i => sumFin m (fun j => F i j)) =
sumFin m (fun j => sumFin n (fun i => F i j)) := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
rw [ih (fun i j => F i.succ j), ← sumFin_add]
-- Un `if` independant de l'index sort de la somme.
/-- An `if` whose condition does not depend on the index pulls out of
the sum (the `else 0` branch matches the empty sum). -/
theorem sumFin_if_distrib {n : Nat} (c : Prop) [Decidable c] (f : Fin n → Int) :
sumFin n (fun i => if c then f i else 0) = if c then sumFin n f else 0 := by
by_cases h : c <;> simp [h]
-- Sommer l'indicateur d'un point isole donne la valeur en ce point.
/-- Summing an indicator of a single point picks out that point's value. -/
theorem sumFin_single : ∀ {n : Nat} (c : Fin n) (x : Fin n → Int),
sumFin n (fun j => if c = j then x j else 0) = x c
| 0, c, _ => c.elim0
| n + 1, c, x => by
cases c using Fin.cases with
| zero =>
have htail : ∀ i : Fin n, (if (0 : Fin (n + 1)) = i.succ then x i.succ else 0) = 0 :=
fun i => if_neg (fun h => Fin.succ_ne_zero i h.symm)
simp only [sumFin_succ]
rw [sumFin_congr htail, sumFin_zero_fun, Int.add_zero]
simp
| succ j =>
simp only [sumFin_succ]
rw [if_neg (Fin.succ_ne_zero j), Int.zero_add]
have hcond : ∀ i : Fin n,
(if j.succ = i.succ then x i.succ else 0) =
(if j = i then x i.succ else 0) := by
intro i
by_cases h : j = i
· rw [if_pos (by rw [h]), if_pos h]
· rw [if_neg (fun hs => h (Fin.succ_inj.mp hs)), if_neg h]
rw [sumFin_congr hcond, sumFin_single j (fun i => x i.succ)]
-- Decomposer une somme d'etats en groupes selon une carte classifiante.
/-- Decompose a sum over states into groups indexed by the value of a
classifying map (finite double counting). -/
theorem sumFin_partition {n m : Nat} (σ : Fin n → Fin m) (f : Fin n → Int) :
sumFin n f = sumFin m (fun k => sumFin n (fun s => if σ s = k then f s else 0)) := by
rw [sumFin_comm]
exact (sumFin_congr (fun s => sumFin_single (σ s) (fun _ => f s))).symm-- Infrastructure (2/2) : lemmes de sommation `sumFin` manquants
-- (le notebook a deja sumFin + sumFin_zero/succ/zero_fun/mono en section 1 ;
-- on ajoute ici les lemmes requis par les preuves de Blackwell).
-- Fonctions ponctuellement egales => sommes egales.
/-- Pointwise equal functions have equal sums. -/
theorem sumFin_congr {n : Nat} {f g : Fin n → Int} (h : ∀ i, f i = g i) :
sumFin n f = sumFin n g := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
rw [h 0, ih (fun i => h i.succ)]
-- Somme de deux fonctions = somme des sommes (requis par sumFin_comm).
/-- Sums distribute over pointwise addition. -/
theorem sumFin_add {n : Nat} (f g : Fin n → Int) :
sumFin n (fun i => f i + g i) = sumFin n f + sumFin n g := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
rw [ih]
omega
-- Double somme commute (Fubini fini).
/-- Double sums commute (Fubini for finite sums). -/
theorem sumFin_comm {n m : Nat} (F : Fin n → Fin m → Int) :
sumFin n (fun i => sumFin m (fun j => F i j)) =
sumFin m (fun j => sumFin n (fun i => F i j)) := by
induction n with
| zero => simp
| succ n ih =>
simp only [sumFin_succ]
rw [ih (fun i j => F i.succ j), ← sumFin_add]
-- Un `if` independant de l'index sort de la somme.
/-- An `if` whose condition does not depend on the index pulls out of
the sum (the `else 0` branch matches the empty sum). -/
theorem sumFin_if_distrib {n : Nat} (c : Prop) [Decidable c] (f : Fin n → Int) :
sumFin n (fun i => if c then f i else 0) = if c then sumFin n f else 0 := by
by_cases h : c <;> simp [h]
-- Sommer l'indicateur d'un point isole donne la valeur en ce point.
/-- Summing an indicator of a single point picks out that point's value. -/
theorem sumFin_single : ∀ {n : Nat} (c : Fin n) (x : Fin n → Int),
sumFin n (fun j => if c = j then x j else 0) = x c
| 0, c, _ => c.elim0
| n + 1, c, x => by
cases c using Fin.cases with
| zero =>
have htail : ∀ i : Fin n, (if (0 : Fin (n + 1)) = i.succ then x i.succ else 0) = 0 :=
fun i => if_neg (fun h => Fin.succ_ne_zero i h.symm)
simp only [sumFin_succ]
rw [sumFin_congr htail, sumFin_zero_fun, Int.add_zero]
simp
| succ j =>
simp only [sumFin_succ]
rw [if_neg (Fin.succ_ne_zero j), Int.zero_add]
have hcond : ∀ i : Fin n,
(if j.succ = i.succ then x i.succ else 0) =
(if j = i then x i.succ else 0) := by
intro i
by_cases h : j = i
· rw [if_pos (by rw [h]), if_pos h]
· rw [if_neg (fun hs => h (Fin.succ_inj.mp hs)), if_neg h]
rw [sumFin_congr hcond, sumFin_single j (fun i => x i.succ)]
-- Decomposer une somme d'etats en groupes selon une carte classifiante.
/-- Decompose a sum over states into groups indexed by the value of a
classifying map (finite double counting). -/
theorem sumFin_partition {n m : Nat} (σ : Fin n → Fin m) (f : Fin n → Int) :
sumFin n f = sumFin m (fun k => sumFin n (fun s => if σ s = k then f s else 0)) := by
rw [sumFin_comm]
exact (sumFin_congr (fun s => sumFin_single (σ s) (fun _ => f s))).symm
--% env 9
{"cmd": "-- Infrastructure (2/2) : lemmes de sommation `sumFin` manquants\n-- (le notebook a deja sumFin + sumFin_zero/succ/zero_fun/mono en section 1 ;\n-- on ajoute ici les lemmes requis par les preuves de Blackwell).\n\n-- Fonctions ponctuellement egales => sommes egales.\n/-- Pointwise equal functions have equal sums. -/\ntheorem sumFin_congr {n : Nat} {f g : Fin n \u2192 Int} (h : \u2200 i, f i = g i) :\n sumFin n f = sumFin n g := by\n induction n with\n | zero => simp\n | succ n ih =>\n simp only [sumFin_succ]\n rw [h 0, ih (fun i => h i.succ)]\n\n-- Somme de deux fonctions = somme des sommes (requis par sumFin_comm).\n/-- Sums distribute over pointwise addition. -/\ntheorem sumFin_add {n : Nat} (f g : Fin n \u2192 Int) :\n sumFin n (fun i => f i + g i) = sumFin n f + sumFin n g := by\n induction n with\n | zero => simp\n | succ n ih =>\n simp only [sumFin_succ]\n rw [ih]\n omega\n\n-- Double somme commute (Fubini fini).\n/-- Double sums commute (Fubini for finite sums). -/\ntheorem sumFin_comm {n m : Nat} (F : Fin n \u2192 Fin m \u2192 Int) :\n sumFin n (fun i => sumFin m (fun j => F i j)) =\n sumFin m (fun j => sumFin n (fun i => F i j)) := by\n induction n with\n | zero => simp\n | succ n ih =>\n simp only [sumFin_succ]\n rw [ih (fun i j => F i.succ j), \u2190 sumFin_add]\n\n-- Un `if` independant de l'index sort de la somme.\n/-- An `if` whose condition does not depend on the index pulls out of\n the sum (the `else 0` branch matches the empty sum). -/\ntheorem sumFin_if_distrib {n : Nat} (c : Prop) [Decidable c] (f : Fin n \u2192 Int) :\n sumFin n (fun i => if c then f i else 0) = if c then sumFin n f else 0 := by\n by_cases h : c <;> simp [h]\n\n-- Sommer l'indicateur d'un point isole donne la valeur en ce point.\n/-- Summing an indicator of a single point picks out that point's value. -/\ntheorem sumFin_single : \u2200 {n : Nat} (c : Fin n) (x : Fin n \u2192 Int),\n sumFin n (fun j => if c = j then x j else 0) = x c\n | 0, c, _ => c.elim0\n | n + 1, c, x => by\n cases c using Fin.cases with\n | zero =>\n have htail : \u2200 i : Fin n, (if (0 : Fin (n + 1)) = i.succ then x i.succ else 0) = 0 :=\n fun i => if_neg (fun h => Fin.succ_ne_zero i h.symm)\n simp only [sumFin_succ]\n rw [sumFin_congr htail, sumFin_zero_fun, Int.add_zero]\n simp\n | succ j =>\n simp only [sumFin_succ]\n rw [if_neg (Fin.succ_ne_zero j), Int.zero_add]\n have hcond : \u2200 i : Fin n,\n (if j.succ = i.succ then x i.succ else 0) =\n (if j = i then x i.succ else 0) := by\n intro i\n by_cases h : j = i\n \u00b7 rw [if_pos (by rw [h]), if_pos h]\n \u00b7 rw [if_neg (fun hs => h (Fin.succ_inj.mp hs)), if_neg h]\n rw [sumFin_congr hcond, sumFin_single j (fun i => x i.succ)]\n\n-- Decomposer une somme d'etats en groupes selon une carte classifiante.\n/-- Decompose a sum over states into groups indexed by the value of a\n classifying map (finite double counting). -/\ntheorem sumFin_partition {n m : Nat} (\u03c3 : Fin n \u2192 Fin m) (f : Fin n \u2192 Int) :\n sumFin n f = sumFin m (fun k => sumFin n (fun s => if \u03c3 s = k then f s else 0)) := by\n rw [sumFin_comm]\n exact (sumFin_congr (fun s => sumFin_single (\u03c3 s) (fun _ => f s))).symm", "env": 8}
{"env": 9}
Le problème de décision mono-joueur (Blackwell) : un décideur face à nS états (prior non normalisé w : Fin nS → Nat), nA + 1 actions, payoffs u : Fin nS → Fin (nA + 1) → Int (cellule code[10]) :
/-- A finite single-agent decision problem with an unnormalized prior.
There are `nS` states and `nA + 1` actions (the `+ 1` keeps the
action set nonempty without carrying a positivity hypothesis). -/
structure DecisionProblem where
/-- Number of states of the world -/
nS : Nat
/-- Number of actions minus one (actions are `Fin (nA + 1)`) -/
nA : Nat
/-- Unnormalized prior weight of each state -/
w : Fin nS → Nat
/-- Payoff of taking an action in a state -/
u : Fin nS → Fin (nA + 1) → Int
/-- Prior-weighted payoff of action `a` in state `s`. -/
def wu (D : DecisionProblem) (s : Fin D.nS) (a : Fin (D.nA + 1)) : Int :=
(D.w s : Int) * D.u s a
-- Un signal deterministe a `m+1` realisations = une partition de l'espace d'etats.
/-- A deterministic signal with `m + 1` possible realizations: it
announces a realization in each state, i.e. partitions the state
space into (at most) `m + 1` cells. -/
def Signal (D : DecisionProblem) (m : Nat) := Fin D.nS → Fin (m + 1)
-- Valeur d'un decideur non informe : la meilleure action unique (toutesCellules confondues).
/-- Expected payoff (unnormalized) of an uninformed decision maker:
pick the single action with the best prior-weighted payoff. -/
def valueNoInfo (D : DecisionProblem) : Int :=
maxFin D.nA (fun a => sumFin D.nS (fun s => wu D s a))
-- Valeur d'un decideur observant le signal : meilleure action par cellule, puis somme.
/-- Expected payoff of a decision maker observing signal `σ`: inside
each cell `k` of the partition, pick the best action for the prior
restricted to that cell, then add up over cells. -/
def valueSignal (D : DecisionProblem) {m : Nat} (σ : Signal D m) : Int :=
sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
-- Valeur d'un decideur parfaitement informe : meilleure action par etat.
/-- Expected payoff of a fully informed decision maker: pick the best
action separately in every state. -/
def valuePerfect (D : DecisionProblem) : Int :=
sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a))Un signal déterministe σ : Signal D m est une application des états vers m + 1 réalisations — une partition finie de l’espace d’états. Les trois valeurs de référence (valueNoInfo, valueSignal σ, valuePerfect) sont celles listées en tête de section.
L’instance concrète umbrella (pluie/soleil équiprobables ; parapluie ou non ; payoffs 2/-3/0/3) est décidée dans la même cellule : umbrella_valueNoInfo (= 2), umbrella_valuePerfect (= 5), umbrella_strict_gain (2 < 5).
Référence : Blackwell (1951) “Comparison of Experiments” ; définitions restatées de lean_game_defs_ext/Bayesian/Information.lean.
Coût : < 100 ms pour la compilation des définitions.
-- Definitions du probleme de decision mono-joueur (Blackwell).
/-- A finite single-agent decision problem with an unnormalized prior.
There are `nS` states and `nA + 1` actions (the `+ 1` keeps the
action set nonempty without carrying a positivity hypothesis). -/
structure DecisionProblem where
/-- Number of states of the world -/
nS : Nat
/-- Number of actions minus one (actions are `Fin (nA + 1)`) -/
nA : Nat
/-- Unnormalized prior weight of each state -/
w : Fin nS → Nat
/-- Payoff of taking an action in a state -/
u : Fin nS → Fin (nA + 1) → Int
/-- Prior-weighted payoff of action `a` in state `s`. -/
def wu (D : DecisionProblem) (s : Fin D.nS) (a : Fin (D.nA + 1)) : Int :=
(D.w s : Int) * D.u s a
-- Un signal deterministe a `m+1` realisations = une partition de l'espace d'etats.
/-- A deterministic signal with `m + 1` possible realizations: it
announces a realization in each state, i.e. partitions the state
space into (at most) `m + 1` cells. -/
def Signal (D : DecisionProblem) (m : Nat) := Fin D.nS → Fin (m + 1)
-- Valeur d'un decideur non informe : la meilleure action unique (toutesCellules confondues).
/-- Expected payoff (unnormalized) of an uninformed decision maker:
pick the single action with the best prior-weighted payoff. -/
def valueNoInfo (D : DecisionProblem) : Int :=
maxFin D.nA (fun a => sumFin D.nS (fun s => wu D s a))
-- Valeur d'un decideur observant le signal : meilleure action par cellule, puis somme.
/-- Expected payoff of a decision maker observing signal `σ`: inside
each cell `k` of the partition, pick the best action for the prior
restricted to that cell, then add up over cells. -/
def valueSignal (D : DecisionProblem) {m : Nat} (σ : Signal D m) : Int :=
sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
-- Valeur d'un decideur parfaitement informe : meilleure action par etat.
/-- Expected payoff of a fully informed decision maker: pick the best
action separately in every state. -/
def valuePerfect (D : DecisionProblem) : Int :=
sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a))
-- Les trois valeurs de reference, sur l'instance concrete `umbrella` :
-- (pluie/soleil equiprobables ; actions parapluie ou non ; payoffs 2/-3/0/3)
/-- Rain-or-sun decision problem used as a kernel-checked example. -/
def umbrella : DecisionProblem where
nS := 2
nA := 1
w := fun _ => 1
u := fun s a =>
if s.val = 0 then (if a.val = 0 then 2 else -3)
else (if a.val = 0 then 0 else 3)
-- Non informe, le meilleur plan (toujours le parapluie) vaut 2.
/-- Uninformed, the best plan (always take the umbrella) is worth 2. -/
theorem umbrella_valueNoInfo : valueNoInfo umbrella = 2 := by decide
#eval valueNoInfo umbrella
-- Parfaitement informe (parapluie ssi pluie), le plan vaut 5.
/-- Perfectly informed (umbrella iff rain), the plan is worth 5. -/
theorem umbrella_valuePerfect : valuePerfect umbrella = 5 := by decide
#eval valuePerfect umbrella
-- Le gain d'information parfaite est strictement positif (decide).
/-- The value of perfect information is strictly positive here. -/
theorem umbrella_strict_gain : valueNoInfo umbrella < valuePerfect umbrella := by
decide-- Definitions du probleme de decision mono-joueur (Blackwell).
/-- A finite single-agent decision problem with an unnormalized prior.
There are `nS` states and `nA + 1` actions (the `+ 1` keeps the
action set nonempty without carrying a positivity hypothesis). -/
structure DecisionProblem where
/-- Number of states of the world -/
nS : Nat
/-- Number of actions minus one (actions are `Fin (nA + 1)`) -/
nA : Nat
/-- Unnormalized prior weight of each state -/
w : Fin nS → Nat
/-- Payoff of taking an action in a state -/
u : Fin nS → Fin (nA + 1) → Int
/-- Prior-weighted payoff of action `a` in state `s`. -/
def wu (D : DecisionProblem) (s : Fin D.nS) (a : Fin (D.nA + 1)) : Int :=
(D.w s : Int) * D.u s a
-- Un signal deterministe a `m+1` realisations = une partition de l'espace d'etats.
/-- A deterministic signal with `m + 1` possible realizations: it
announces a realization in each state, i.e. partitions the state
space into (at most) `m + 1` cells. -/
def Signal (D : DecisionProblem) (m : Nat) := Fin D.nS → Fin (m + 1)
-- Valeur d'un decideur non informe : la meilleure action unique (toutesCellules confondues).
/-- Expected payoff (unnormalized) of an uninformed decision maker:
pick the single action with the best prior-weighted payoff. -/
def valueNoInfo (D : DecisionProblem) : Int :=
maxFin D.nA (fun a => sumFin D.nS (fun s => wu D s a))
-- Valeur d'un decideur observant le signal : meilleure action par cellule, puis somme.
/-- Expected payoff of a decision maker observing signal `σ`: inside
each cell `k` of the partition, pick the best action for the prior
restricted to that cell, then add up over cells. -/
def valueSignal (D : DecisionProblem) {m : Nat} (σ : Signal D m) : Int :=
sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
-- Valeur d'un decideur parfaitement informe : meilleure action par etat.
/-- Expected payoff of a fully informed decision maker: pick the best
action separately in every state. -/
def valuePerfect (D : DecisionProblem) : Int :=
sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a))
-- Les trois valeurs de reference, sur l'instance concrete `umbrella` :
-- (pluie/soleil equiprobables ; actions parapluie ou non ; payoffs 2/-3/0/3)
/-- Rain-or-sun decision problem used as a kernel-checked example. -/
def umbrella : DecisionProblem where
nS := 2
nA := 1
w := fun _ => 1
u := fun s a =>
if s.val = 0 then (if a.val = 0 then 2 else -3)
else (if a.val = 0 then 0 else 3)
-- Non informe, le meilleur plan (toujours le parapluie) vaut 2.
/-- Uninformed, the best plan (always take the umbrella) is worth 2. -/
theorem umbrella_valueNoInfo : valueNoInfo umbrella = 2 := by decide
2
-- Parfaitement informe (parapluie ssi pluie), le plan vaut 5.
/-- Perfectly informed (umbrella iff rain), the plan is worth 5. -/
theorem umbrella_valuePerfect : valuePerfect umbrella = 5 := by decide
5
-- Le gain d'information parfaite est strictement positif (decide).
/-- The value of perfect information is strictly positive here. -/
theorem umbrella_strict_gain : valueNoInfo umbrella < valuePerfect umbrella := by
decide
--% env 10
{"cmd": "-- Definitions du probleme de decision mono-joueur (Blackwell).\n\n/-- A finite single-agent decision problem with an unnormalized prior.\n There are `nS` states and `nA + 1` actions (the `+ 1` keeps the\n action set nonempty without carrying a positivity hypothesis). -/\nstructure DecisionProblem where\n /-- Number of states of the world -/\n nS : Nat\n /-- Number of actions minus one (actions are `Fin (nA + 1)`) -/\n nA : Nat\n /-- Unnormalized prior weight of each state -/\n w : Fin nS \u2192 Nat\n /-- Payoff of taking an action in a state -/\n u : Fin nS \u2192 Fin (nA + 1) \u2192 Int\n\n/-- Prior-weighted payoff of action `a` in state `s`. -/\ndef wu (D : DecisionProblem) (s : Fin D.nS) (a : Fin (D.nA + 1)) : Int :=\n (D.w s : Int) * D.u s a\n\n-- Un signal deterministe a `m+1` realisations = une partition de l'espace d'etats.\n/-- A deterministic signal with `m + 1` possible realizations: it\n announces a realization in each state, i.e. partitions the state\n space into (at most) `m + 1` cells. -/\ndef Signal (D : DecisionProblem) (m : Nat) := Fin D.nS \u2192 Fin (m + 1)\n\n-- Valeur d'un decideur non informe : la meilleure action unique (toutesCellules confondues).\n/-- Expected payoff (unnormalized) of an uninformed decision maker:\n pick the single action with the best prior-weighted payoff. -/\ndef valueNoInfo (D : DecisionProblem) : Int :=\n maxFin D.nA (fun a => sumFin D.nS (fun s => wu D s a))\n\n-- Valeur d'un decideur observant le signal : meilleure action par cellule, puis somme.\n/-- Expected payoff of a decision maker observing signal `\u03c3`: inside\n each cell `k` of the partition, pick the best action for the prior\n restricted to that cell, then add up over cells. -/\ndef valueSignal (D : DecisionProblem) {m : Nat} (\u03c3 : Signal D m) : Int :=\n sumFin (m + 1) (fun k => maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0)))\n\n-- Valeur d'un decideur parfaitement informe : meilleure action par etat.\n/-- Expected payoff of a fully informed decision maker: pick the best\n action separately in every state. -/\ndef valuePerfect (D : DecisionProblem) : Int :=\n sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a))\n\n-- Les trois valeurs de reference, sur l'instance concrete `umbrella` :\n-- (pluie/soleil equiprobables ; actions parapluie ou non ; payoffs 2/-3/0/3)\n/-- Rain-or-sun decision problem used as a kernel-checked example. -/\ndef umbrella : DecisionProblem where\n nS := 2\n nA := 1\n w := fun _ => 1\n u := fun s a =>\n if s.val = 0 then (if a.val = 0 then 2 else -3)\n else (if a.val = 0 then 0 else 3)\n\n-- Non informe, le meilleur plan (toujours le parapluie) vaut 2.\n/-- Uninformed, the best plan (always take the umbrella) is worth 2. -/\ntheorem umbrella_valueNoInfo : valueNoInfo umbrella = 2 := by decide\n#eval valueNoInfo umbrella\n\n-- Parfaitement informe (parapluie ssi pluie), le plan vaut 5.\n/-- Perfectly informed (umbrella iff rain), the plan is worth 5. -/\ntheorem umbrella_valuePerfect : valuePerfect umbrella = 5 := by decide\n#eval valuePerfect umbrella\n\n-- Le gain d'information parfaite est strictement positif (decide).\n/-- The value of perfect information is strictly positive here. -/\ntheorem umbrella_strict_gain : valueNoInfo umbrella < valuePerfect umbrella := by\n decide", "env": 9}
{"messages":
[{"severity": "info",
"pos": {"line": 60, "column": 0},
"endPos": {"line": 60, "column": 5},
"data": "2"},
{"severity": "info",
"pos": {"line": 65, "column": 0},
"endPos": {"line": 65, "column": 5},
"data": "5"}],
"env": 10}
Lecture du théorème de Vickrey (cellule code[6]) :
/-- **Théorème de Vickrey** (fini, deux enchérisseurs) : le profil honnête est un BNE pour tout n. -/
theorem spa_truthful_bne (n : Nat) :
isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n) :=
⟨fun t1 a => spa_interim_best1 n t1 a (spaTruthful2 n),
fun t2 a => spa_interim_best2 n t2 a (spaTruthful1 n)⟩
#check spa_truthful_bnePourquoi ce théorème est important : c’est la Revelation Principle en action : un mécanisme d’enchères (Vickrey/second-prix) incite les joueurs à révéler leurs vraies valuations. C’est la base de toute la théorie des mécanismes (Myerson 1981 + Maskin 1977).
Pourquoi la preuve est si courte : les deux composantes de la conjonction isBNE sont exactement spa_interim_best1/spa_interim_best2 (établies en 4.1) — le constructeur anonyme ⟨_, _⟩ les assemble. La preuve complète est restatée du lake lean_game_defs_ext/ (0 sorry).
Sortie attendue : #check spa_truthful_bne : spa_truthful_bne (n : Nat) : isBNE (spa n) (spaTruthful1 n) (spaTruthful2 n).
Référence : Vickrey (1961), Myerson (1981) “Optimal Auction Design”.
Coût : < 100 ms pour la vérification de l’énoncé.
Importance pédagogique : ce notebook est conçu comme un banc d’essai du prouveur : on donne l’énoncé et la structure de la preuve, et le BG-prover tente de la compléter. C’est exactement ce que fait EPIC #1453 (BG-prover harness) sur ce type d’énoncés.
Le kernel lean4-wsl decide reellement les valeurs exactes : sans information, le plan optimal vaut 2 (toujours prendre le parapluie — les deux états équiprobables donnent 2+0 via wu) ; avec information parfaite, 5 (parapluie seulement s’il pleut — 2+3). L’inégalité stricte 2 < 5 est close par decide : l’information parfaite vaut strictement plus que l’absence d’information, un fait vérifié par le kernel sur cette instance concrète (pas un argument de manuel). C’est le cas déterministe, une seule instance, du théorème général de Blackwell énoncé ci-dessous.
Les trois théorèmes (cellules code[11-13]), restatés verbatim du lake Information.lean :
1. Signal trivial (valueSignal_const) : valueSignal D (fun _ => (0 : Fin 1)) = valueNoInfo D — le signal totalement non informatif (unique réalisation) vaut exactement la valeur sans information. Point de repère : tout signal informatif doit faire au moins aussi bien.
2. Monotonie (valueSignal_mono, résultat amiral) : si hfactor : ∀ s, σ s = h (τ s) (σ est un grossissement de τ), alors valueSignal D σ ≤ valueSignal D τ — observer le signal plus fin τ vaut au moins autant que σ. La preuve réécrit chaque cellule de σ comme somme de cellules de τ (lemme fibre sumFin_fiber), majore chaque max par la somme des maxima (maxFin_sumFin_le), puis défait le double comptage (sumFin_partition).
3. L’information ne nuit jamais (valueNoInfo_le_valueSignal) : valueNoInfo D ≤ valueSignal D σ pour tout signal — tout signal raffine le signal trivial, corollaire de 1 + 2. Même cellule : valueSignal_le_valuePerfect (l’information parfaite domine tout signal) et valueNoInfo_le_valuePerfect.
La frontière mono-joueur / jeu : en mono-joueur, l’information est toujours bonne ; en jeu, ce n’est plus vrai — section 6.
Sortie attendue : #check valueSignal_mono en sortie de la cellule ; 0 sorry (preuves complètes restatées).
Coût : < 200 ms pour compiler les 3 théorèmes.
-- Theoremes cles de Blackwell (1/3) : signal trivial + lemme fibre.
-- (Prouves 0-sorry dans Information.lean, restates verbatim.)
-- Le signal totalement non informatif (unique realisation) vaut valueNoInfo.
/-- The totally uninformative signal (a single realization) is worth
exactly the no-information value. -/
theorem valueSignal_const (D : DecisionProblem) :
valueSignal D (fun _ => (0 : Fin 1)) = valueNoInfo D := by
unfold valueSignal valueNoInfo
simp
-- **Lemme fibre** : somme sur les etats classes par h compose tau.
/-- Fiber decomposition: summing `f` over the states classified by the
composite map `h ∘ τ` into cell `k` equals summing, over the
realizations `j` of `τ` that `h` sends to `k`, the `τ`-cell sums. -/
theorem sumFin_fiber {n m p : Nat} (τ : Fin n → Fin p) (h : Fin p → Fin m)
(k : Fin m) (f : Fin n → Int) :
sumFin n (fun s => if h (τ s) = k then f s else 0) =
sumFin p (fun j => if h j = k then
sumFin n (fun s => if τ s = j then f s else 0) else 0) := by
have push : ∀ j : Fin p,
(if h j = k then sumFin n (fun s => if τ s = j then f s else 0) else 0) =
sumFin n (fun s => if h j = k then (if τ s = j then f s else 0) else 0) :=
fun j => (sumFin_if_distrib _ _).symm
rw [sumFin_congr push, sumFin_comm]
apply sumFin_congr
intro s
have swap : ∀ j : Fin p,
(if h j = k then (if τ s = j then f s else 0) else 0) =
(if τ s = j then (if h j = k then f s else 0) else 0) := by
intro j
by_cases h1 : h j = k <;> by_cases h2 : τ s = j <;> simp [h1, h2]
rw [sumFin_congr swap, sumFin_single (τ s) (fun j => if h j = k then f s else 0)]-- Theoremes cles de Blackwell (1/3) : signal trivial + lemme fibre.
-- (Prouves 0-sorry dans Information.lean, restates verbatim.)
-- Le signal totalement non informatif (unique realisation) vaut valueNoInfo.
/-- The totally uninformative signal (a single realization) is worth
exactly the no-information value. -/
theorem valueSignal_const (D : DecisionProblem) :
valueSignal D (fun _ => (0 : Fin 1)) = valueNoInfo D := by
unfold valueSignal valueNoInfo
simp
-- **Lemme fibre** : somme sur les etats classes par h compose tau.
/-- Fiber decomposition: summing `f` over the states classified by the
composite map `h ∘ τ` into cell `k` equals summing, over the
realizations `j` of `τ` that `h` sends to `k`, the `τ`-cell sums. -/
theorem sumFin_fiber {n m p : Nat} (τ : Fin n → Fin p) (h : Fin p → Fin m)
(k : Fin m) (f : Fin n → Int) :
sumFin n (fun s => if h (τ s) = k then f s else 0) =
sumFin p (fun j => if h j = k then
sumFin n (fun s => if τ s = j then f s else 0) else 0) := by
have push : ∀ j : Fin p,
(if h j = k then sumFin n (fun s => if τ s = j then f s else 0) else 0) =
sumFin n (fun s => if h j = k then (if τ s = j then f s else 0) else 0) :=
fun j => (sumFin_if_distrib _ _).symm
rw [sumFin_congr push, sumFin_comm]
apply sumFin_congr
intro s
have swap : ∀ j : Fin p,
(if h j = k then (if τ s = j then f s else 0) else 0) =
(if τ s = j then (if h j = k then f s else 0) else 0) := by
intro j
by_cases h1 : h j = k <;> by_cases h2 : τ s = j <;> simp [h1, h2]
rw [sumFin_congr swap, sumFin_single (τ s) (fun j => if h j = k then f s else 0)]
--% env 11
{"cmd": "-- Theoremes cles de Blackwell (1/3) : signal trivial + lemme fibre.\n-- (Prouves 0-sorry dans Information.lean, restates verbatim.)\n\n-- Le signal totalement non informatif (unique realisation) vaut valueNoInfo.\n/-- The totally uninformative signal (a single realization) is worth\n exactly the no-information value. -/\ntheorem valueSignal_const (D : DecisionProblem) :\n valueSignal D (fun _ => (0 : Fin 1)) = valueNoInfo D := by\n unfold valueSignal valueNoInfo\n simp\n\n-- **Lemme fibre** : somme sur les etats classes par h compose tau.\n/-- Fiber decomposition: summing `f` over the states classified by the\n composite map `h \u2218 \u03c4` into cell `k` equals summing, over the\n realizations `j` of `\u03c4` that `h` sends to `k`, the `\u03c4`-cell sums. -/\ntheorem sumFin_fiber {n m p : Nat} (\u03c4 : Fin n \u2192 Fin p) (h : Fin p \u2192 Fin m)\n (k : Fin m) (f : Fin n \u2192 Int) :\n sumFin n (fun s => if h (\u03c4 s) = k then f s else 0) =\n sumFin p (fun j => if h j = k then\n sumFin n (fun s => if \u03c4 s = j then f s else 0) else 0) := by\n have push : \u2200 j : Fin p,\n (if h j = k then sumFin n (fun s => if \u03c4 s = j then f s else 0) else 0) =\n sumFin n (fun s => if h j = k then (if \u03c4 s = j then f s else 0) else 0) :=\n fun j => (sumFin_if_distrib _ _).symm\n rw [sumFin_congr push, sumFin_comm]\n apply sumFin_congr\n intro s\n have swap : \u2200 j : Fin p,\n (if h j = k then (if \u03c4 s = j then f s else 0) else 0) =\n (if \u03c4 s = j then (if h j = k then f s else 0) else 0) := by\n intro j\n by_cases h1 : h j = k <;> by_cases h2 : \u03c4 s = j <;> simp [h1, h2]\n rw [sumFin_congr swap, sumFin_single (\u03c4 s) (fun j => if h j = k then f s else 0)]", "env": 10}
{"env": 11}
-- Theoremes cles de Blackwell (2/3) : monotonie (resultat amiral).
-- Si sigma est un raffinement de tau (sigma = h compose tau), alors tau
-- (plus fin) vaut au moins sigma.
/-- **Blackwell monotonicity (deterministic case).** If the signal `σ`
is a coarsening of `τ` — every realization of `σ` is computed from
the realization of `τ` via `h` — then observing the finer signal
`τ` is worth at least as much as observing `σ`. -/
theorem valueSignal_mono (D : DecisionProblem) {m p : Nat}
(σ : Signal D m) (τ : Signal D p) (h : Fin (p + 1) → Fin (m + 1))
(hfactor : ∀ s, σ s = h (τ s)) :
valueSignal D σ ≤ valueSignal D τ := by
unfold valueSignal
-- Rewrite each σ-cell sum as a sum over the τ-cells it contains.
have hcell : ∀ (k : Fin (m + 1)) (a : Fin (D.nA + 1)),
sumFin D.nS (fun s => if σ s = k then wu D s a else 0) =
sumFin (p + 1) (fun j => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0) := by
intro k a
rw [sumFin_congr (fun s => by rw [hfactor s]),
sumFin_fiber τ h k (fun s => wu D s a)]
-- Bound the max over each σ-cell by the sum of maxima over its τ-cells.
have hk : ∀ k : Fin (m + 1),
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)) ≤
sumFin (p + 1) (fun j => if h j = k then
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0) := by
intro k
have step1 := maxFin_sumFin_le (fun j a => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0)
have step2 : ∀ j : Fin (p + 1),
maxFin D.nA (fun a => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0) =
(if h j = k then maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0) :=
fun j => maxFin_if_distrib _ _
calc maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0))
= maxFin D.nA (fun a =>
sumFin (p + 1) (fun j => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0)) := by
exact congrArg (maxFin D.nA) (funext (fun a => hcell k a))
_ ≤ sumFin (p + 1) (fun j =>
maxFin D.nA (fun a => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0)) := step1
_ = sumFin (p + 1) (fun j => if h j = k then
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0) :=
sumFin_congr step2
-- Sum the per-cell bounds, then undo the double counting over k.
calc sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
≤ sumFin (m + 1) (fun k => sumFin (p + 1) (fun j => if h j = k then
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0)) :=
sumFin_mono hk
_ = sumFin (p + 1) (fun j => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0))) :=
(sumFin_partition h (fun j => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)))).symm
#check valueSignal_mono-- Theoremes cles de Blackwell (2/3) : monotonie (resultat amiral).
-- Si sigma est un raffinement de tau (sigma = h compose tau), alors tau
-- (plus fin) vaut au moins sigma.
/-- **Blackwell monotonicity (deterministic case).** If the signal `σ`
is a coarsening of `τ` — every realization of `σ` is computed from
the realization of `τ` via `h` — then observing the finer signal
`τ` is worth at least as much as observing `σ`. -/
theorem valueSignal_mono (D : DecisionProblem) {m p : Nat}
(σ : Signal D m) (τ : Signal D p) (h : Fin (p + 1) → Fin (m + 1))
(hfactor : ∀ s, σ s = h (τ s)) :
valueSignal D σ ≤ valueSignal D τ := by
unfold valueSignal
-- Rewrite each σ-cell sum as a sum over the τ-cells it contains.
have hcell : ∀ (k : Fin (m + 1)) (a : Fin (D.nA + 1)),
sumFin D.nS (fun s => if σ s = k then wu D s a else 0) =
sumFin (p + 1) (fun j => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0) := by
intro k a
rw [sumFin_congr (fun s => by rw [hfactor s]),
sumFin_fiber τ h k (fun s => wu D s a)]
-- Bound the max over each σ-cell by the sum of maxima over its τ-cells.
have hk : ∀ k : Fin (m + 1),
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)) ≤
sumFin (p + 1) (fun j => if h j = k then
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0) := by
intro k
have step1 := maxFin_sumFin_le (fun j a => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0)
have step2 : ∀ j : Fin (p + 1),
maxFin D.nA (fun a => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0) =
(if h j = k then maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0) :=
fun j => maxFin_if_distrib _ _
calc maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0))
= maxFin D.nA (fun a =>
sumFin (p + 1) (fun j => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0)) := by
exact congrArg (maxFin D.nA) (funext (fun a => hcell k a))
_ ≤ sumFin (p + 1) (fun j =>
maxFin D.nA (fun a => if h j = k then
sumFin D.nS (fun s => if τ s = j then wu D s a else 0) else 0)) := step1
_ = sumFin (p + 1) (fun j => if h j = k then
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0) :=
sumFin_congr step2
-- Sum the per-cell bounds, then undo the double counting over k.
calc sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
≤ sumFin (m + 1) (fun k => sumFin (p + 1) (fun j => if h j = k then
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)) else 0)) :=
sumFin_mono hk
_ = sumFin (p + 1) (fun j => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0))) :=
(sumFin_partition h (fun j => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if τ s = j then wu D s a else 0)))).symm
valueSignal_mono (D : DecisionProblem) {m p : Nat} (σ : Signal D m) (τ : Signal D p) (h : Fin (p + 1) → Fin (m + 1))
(hfactor : ∀ (s : Fin D.nS), σ s = h (τ s)) : valueSignal D σ ≤ valueSignal D τ
--% env 12
{"cmd": "-- Theoremes cles de Blackwell (2/3) : monotonie (resultat amiral).\n-- Si sigma est un raffinement de tau (sigma = h compose tau), alors tau\n-- (plus fin) vaut au moins sigma.\n\n/-- **Blackwell monotonicity (deterministic case).** If the signal `\u03c3`\n is a coarsening of `\u03c4` \u2014 every realization of `\u03c3` is computed from\n the realization of `\u03c4` via `h` \u2014 then observing the finer signal\n `\u03c4` is worth at least as much as observing `\u03c3`. -/\ntheorem valueSignal_mono (D : DecisionProblem) {m p : Nat}\n (\u03c3 : Signal D m) (\u03c4 : Signal D p) (h : Fin (p + 1) \u2192 Fin (m + 1))\n (hfactor : \u2200 s, \u03c3 s = h (\u03c4 s)) :\n valueSignal D \u03c3 \u2264 valueSignal D \u03c4 := by\n unfold valueSignal\n -- Rewrite each \u03c3-cell sum as a sum over the \u03c4-cells it contains.\n have hcell : \u2200 (k : Fin (m + 1)) (a : Fin (D.nA + 1)),\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0) =\n sumFin (p + 1) (fun j => if h j = k then\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0) else 0) := by\n intro k a\n rw [sumFin_congr (fun s => by rw [hfactor s]),\n sumFin_fiber \u03c4 h k (fun s => wu D s a)]\n -- Bound the max over each \u03c3-cell by the sum of maxima over its \u03c4-cells.\n have hk : \u2200 k : Fin (m + 1),\n maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0)) \u2264\n sumFin (p + 1) (fun j => if h j = k then\n maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0)) else 0) := by\n intro k\n have step1 := maxFin_sumFin_le (fun j a => if h j = k then\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0) else 0)\n have step2 : \u2200 j : Fin (p + 1),\n maxFin D.nA (fun a => if h j = k then\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0) else 0) =\n (if h j = k then maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0)) else 0) :=\n fun j => maxFin_if_distrib _ _\n calc maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0))\n = maxFin D.nA (fun a =>\n sumFin (p + 1) (fun j => if h j = k then\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0) else 0)) := by\n exact congrArg (maxFin D.nA) (funext (fun a => hcell k a))\n _ \u2264 sumFin (p + 1) (fun j =>\n maxFin D.nA (fun a => if h j = k then\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0) else 0)) := step1\n _ = sumFin (p + 1) (fun j => if h j = k then\n maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0)) else 0) :=\n sumFin_congr step2\n -- Sum the per-cell bounds, then undo the double counting over k.\n calc sumFin (m + 1) (fun k => maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0)))\n \u2264 sumFin (m + 1) (fun k => sumFin (p + 1) (fun j => if h j = k then\n maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0)) else 0)) :=\n sumFin_mono hk\n _ = sumFin (p + 1) (fun j => maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0))) :=\n (sumFin_partition h (fun j => maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c4 s = j then wu D s a else 0)))).symm\n\n#check valueSignal_mono", "env": 11}
{"messages":
[{"severity": "info",
"pos": {"line": 63, "column": 0},
"endPos": {"line": 63, "column": 6},
"data":
"valueSignal_mono (D : DecisionProblem) {m p : Nat} (σ : Signal D m) (τ : Signal D p) (h : Fin (p + 1) → Fin (m + 1))\n (hfactor : ∀ (s : Fin D.nS), σ s = h (τ s)) : valueSignal D σ ≤ valueSignal D τ"}],
"env": 12}
-- Theoremes cles de Blackwell (3/3) : l'information ne nuit jamais.
-- **L'information ne nuit jamais** a un decideur seul : tout signal vaut
-- au moins valueNoInfo (tout signal raffine le signal trivial).
/-- **Information never hurts a single decision maker**: any signal is
worth at least the no-information value (every signal refines the
trivial one). -/
theorem valueNoInfo_le_valueSignal (D : DecisionProblem) {m : Nat}
(σ : Signal D m) :
valueNoInfo D ≤ valueSignal D σ := by
rw [← valueSignal_const D]
exact valueSignal_mono D (fun _ => (0 : Fin 1)) σ (fun _ => 0) (fun _ => rfl)
-- L'information parfaite domine tout signal (etat exact = signal le plus fin).
/-- Perfect information dominates any signal: knowing the state exactly
is the finest deterministic signal. -/
theorem valueSignal_le_valuePerfect (D : DecisionProblem) {m : Nat}
(σ : Signal D m) :
valueSignal D σ ≤ valuePerfect D := by
unfold valueSignal valuePerfect
have hk : ∀ k : Fin (m + 1),
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)) ≤
sumFin D.nS (fun s => if σ s = k then
maxFin D.nA (fun a => wu D s a) else 0) := by
intro k
have step1 := maxFin_sumFin_le (fun s a => if σ s = k then wu D s a else 0)
have step2 : ∀ s : Fin D.nS,
maxFin D.nA (fun a => if σ s = k then wu D s a else 0) =
(if σ s = k then maxFin D.nA (fun a => wu D s a) else 0) :=
fun s => maxFin_if_distrib _ _
exact Int.le_trans step1 (Int.le_of_eq (sumFin_congr step2))
calc sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
≤ sumFin (m + 1) (fun k => sumFin D.nS (fun s => if σ s = k then
maxFin D.nA (fun a => wu D s a) else 0)) := sumFin_mono hk
_ = sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a)) :=
(sumFin_partition σ (fun s => maxFin D.nA (fun a => wu D s a))).symm
-- Composition : pas d'information <= information parfaite.
/-- No information is at most perfect information (composition of the
two comparisons, stated directly for convenience). -/
theorem valueNoInfo_le_valuePerfect (D : DecisionProblem) :
valueNoInfo D ≤ valuePerfect D :=
Int.le_trans (valueNoInfo_le_valueSignal D (fun _ => (0 : Fin 1)))
(valueSignal_le_valuePerfect D _)
/-
Concrete check: the umbrella problem. Two equally likely states
(rain, sun), two actions (take the umbrella, leave it). Payoffs:
umbrella = 2 in rain, 0 in sun; no umbrella = -3 in rain, 3 in sun.
-/-- Theoremes cles de Blackwell (3/3) : l'information ne nuit jamais.
-- **L'information ne nuit jamais** a un decideur seul : tout signal vaut
-- au moins valueNoInfo (tout signal raffine le signal trivial).
/-- **Information never hurts a single decision maker**: any signal is
worth at least the no-information value (every signal refines the
trivial one). -/
theorem valueNoInfo_le_valueSignal (D : DecisionProblem) {m : Nat}
(σ : Signal D m) :
valueNoInfo D ≤ valueSignal D σ := by
rw [← valueSignal_const D]
exact valueSignal_mono D (fun _ => (0 : Fin 1)) σ (fun _ => 0) (fun _ => rfl)
-- L'information parfaite domine tout signal (etat exact = signal le plus fin).
/-- Perfect information dominates any signal: knowing the state exactly
is the finest deterministic signal. -/
theorem valueSignal_le_valuePerfect (D : DecisionProblem) {m : Nat}
(σ : Signal D m) :
valueSignal D σ ≤ valuePerfect D := by
unfold valueSignal valuePerfect
have hk : ∀ k : Fin (m + 1),
maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)) ≤
sumFin D.nS (fun s => if σ s = k then
maxFin D.nA (fun a => wu D s a) else 0) := by
intro k
have step1 := maxFin_sumFin_le (fun s a => if σ s = k then wu D s a else 0)
have step2 : ∀ s : Fin D.nS,
maxFin D.nA (fun a => if σ s = k then wu D s a else 0) =
(if σ s = k then maxFin D.nA (fun a => wu D s a) else 0) :=
fun s => maxFin_if_distrib _ _
exact Int.le_trans step1 (Int.le_of_eq (sumFin_congr step2))
calc sumFin (m + 1) (fun k => maxFin D.nA (fun a =>
sumFin D.nS (fun s => if σ s = k then wu D s a else 0)))
≤ sumFin (m + 1) (fun k => sumFin D.nS (fun s => if σ s = k then
maxFin D.nA (fun a => wu D s a) else 0)) := sumFin_mono hk
_ = sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a)) :=
(sumFin_partition σ (fun s => maxFin D.nA (fun a => wu D s a))).symm
-- Composition : pas d'information <= information parfaite.
/-- No information is at most perfect information (composition of the
two comparisons, stated directly for convenience). -/
theorem valueNoInfo_le_valuePerfect (D : DecisionProblem) :
valueNoInfo D ≤ valuePerfect D :=
Int.le_trans (valueNoInfo_le_valueSignal D (fun _ => (0 : Fin 1)))
(valueSignal_le_valuePerfect D _)
/-
Concrete check: the umbrella problem. Two equally likely states
(rain, sun), two actions (take the umbrella, leave it). Payoffs:
umbrella = 2 in rain, 0 in sun; no umbrella = -3 in rain, 3 in sun.
-/
--% env 13
{"cmd": "-- Theoremes cles de Blackwell (3/3) : l'information ne nuit jamais.\n\n-- **L'information ne nuit jamais** a un decideur seul : tout signal vaut\n-- au moins valueNoInfo (tout signal raffine le signal trivial).\n/-- **Information never hurts a single decision maker**: any signal is\n worth at least the no-information value (every signal refines the\n trivial one). -/\ntheorem valueNoInfo_le_valueSignal (D : DecisionProblem) {m : Nat}\n (\u03c3 : Signal D m) :\n valueNoInfo D \u2264 valueSignal D \u03c3 := by\n rw [\u2190 valueSignal_const D]\n exact valueSignal_mono D (fun _ => (0 : Fin 1)) \u03c3 (fun _ => 0) (fun _ => rfl)\n\n-- L'information parfaite domine tout signal (etat exact = signal le plus fin).\n/-- Perfect information dominates any signal: knowing the state exactly\n is the finest deterministic signal. -/\ntheorem valueSignal_le_valuePerfect (D : DecisionProblem) {m : Nat}\n (\u03c3 : Signal D m) :\n valueSignal D \u03c3 \u2264 valuePerfect D := by\n unfold valueSignal valuePerfect\n have hk : \u2200 k : Fin (m + 1),\n maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0)) \u2264\n sumFin D.nS (fun s => if \u03c3 s = k then\n maxFin D.nA (fun a => wu D s a) else 0) := by\n intro k\n have step1 := maxFin_sumFin_le (fun s a => if \u03c3 s = k then wu D s a else 0)\n have step2 : \u2200 s : Fin D.nS,\n maxFin D.nA (fun a => if \u03c3 s = k then wu D s a else 0) =\n (if \u03c3 s = k then maxFin D.nA (fun a => wu D s a) else 0) :=\n fun s => maxFin_if_distrib _ _\n exact Int.le_trans step1 (Int.le_of_eq (sumFin_congr step2))\n calc sumFin (m + 1) (fun k => maxFin D.nA (fun a =>\n sumFin D.nS (fun s => if \u03c3 s = k then wu D s a else 0)))\n \u2264 sumFin (m + 1) (fun k => sumFin D.nS (fun s => if \u03c3 s = k then\n maxFin D.nA (fun a => wu D s a) else 0)) := sumFin_mono hk\n _ = sumFin D.nS (fun s => maxFin D.nA (fun a => wu D s a)) :=\n (sumFin_partition \u03c3 (fun s => maxFin D.nA (fun a => wu D s a))).symm\n\n-- Composition : pas d'information <= information parfaite.\n/-- No information is at most perfect information (composition of the\n two comparisons, stated directly for convenience). -/\ntheorem valueNoInfo_le_valuePerfect (D : DecisionProblem) :\n valueNoInfo D \u2264 valuePerfect D :=\n Int.le_trans (valueNoInfo_le_valueSignal D (fun _ => (0 : Fin 1)))\n (valueSignal_le_valuePerfect D _)\n\n/-\n Concrete check: the umbrella problem. Two equally likely states\n (rain, sun), two actions (take the umbrella, leave it). Payoffs:\n umbrella = 2 in rain, 0 in sun; no umbrella = -3 in rain, 3 in sun.\n-/", "env": 12}
{"env": 13}
La section 5 a établi, avec Blackwell, que l’information ne nuit jamais à un décideur seul : tout signal vaut au moins valueNoInfo. Ce résultat est genuiment mono-joueur : dès qu’on passe à un jeu (plusieurs joueurs stratégiques), donner à l’un d’eux strictement plus d’information privée peut strictement réduire son paiement d’équilibre.
C’est l’un des contre-exemples les plus subtils de la théorie des jeux, et il est vérifié par le kernel sur une construction finie (deux états, jeu 2×2). On compare deux versions d’un même jeu bayésien :
gNoInfo : personne n’observe l’état θ (réduction ex-ante, un type par joueur) ;gInfo : le joueur 2 observe privément θ (deux types).Dans les deux jeux, le joueur 2 est la même personne, avec les mêmes préférences fondamentales. La seule différence est ce qu’il sait. Et pourtant — le kernel le décide sur l’instance — le joueur 2 informé gagne strictement moins (3) que le joueur 2 non informé (5). Le mécanisme : informé, le type θ=1 du joueur 2 ne peut plus s’engager à jouer l ; son action révèle alors l’état au joueur 1, dont la meilleure réponse bascule et coûte au joueur 2 plus que le gain informationnel. La capacité à s’engager vaut plus que l’information.
(Source : lean_game_defs_ext/Bayesian/InfoGames.lean, phase 4 de #2610. Contre-exemple canonique contrastant avec valueNoInfo_le_valueSignal de la section 5.)
Implémentation Lean (cellules code[14-18]) : les deux jeux sont définis, leur équilibre analysé par constructeurs canoniques + decide, et la punchline information_hurts clôt la série : en tout équilibre, exAnteU2 gInfo s1 s2 < exAnteU2 gNoInfo t1 t2 (3 < 5).
-- Les deux jeux : gInfo (joueur 2 observe l'etat) vs gNoInfo (personne).
-- Le jeu informé : le joueur 2 observe privément θ (2 types), joueur 1 a 1 type.
/-- The informed game: player 2 privately observes the state θ (their
type), player 1 has a single type. Equal prior weights. -/
def gInfo : BayesGame2 where
nT1 := 1
nT2 := 2
nA1 := 2
nA2 := 2
w := fun _ _ => 1
u1 := fun _ t2 a1 a2 =>
if t2.val = 0 then
(if a1.val = 0 then (if a2.val = 0 then 2 else 0) else 0)
else
(if a1.val = 0 then (if a2.val = 0 then 2 else 0)
else (if a2.val = 0 then 0 else 4))
u2 := fun _ t2 a1 a2 =>
if t2.val = 0 then
(if a1.val = 0 then (if a2.val = 0 then 3 else 0)
else (if a2.val = 0 then 2 else 0))
else
(if a1.val = 0 then (if a2.val = 0 then 2 else 3)
else (if a2.val = 0 then 0 else 1))
-- Le jeu non informé : personne n'observe θ, payoffs sommés sur les 2 états
-- (réduction ex-ante fidèle de gInfo, cf. infoHurts_reduction ci-dessous).
/-- The uninformed benchmark: nobody observes θ, so both players have a
single type and payoffs are summed over the two states (ex-ante
reduction of `gInfo` for an uninformed player 2). -/
def gNoInfo : BayesGame2 where
nT1 := 1
nT2 := 1
nA1 := 2
nA2 := 2
w := fun _ _ => 1
u1 := fun _ _ a1 a2 =>
if a1.val = 0 then (if a2.val = 0 then 4 else 0)
else (if a2.val = 0 then 0 else 4)
u2 := fun _ _ a1 a2 =>
if a1.val = 0 then (if a2.val = 0 then 5 else 3)
else (if a2.val = 0 then 2 else 1)
-- Vérification (kernel-décidée) : gNoInfo est bien la somme de gInfo sur θ.
-- Ce n'est pas un jeu indépendant -- c'est la MEME situation, le joueur 2
-- voyant juste moins.
/-- Sanity check: `gNoInfo`'s payoffs are exactly `gInfo`'s summed over
the two states — the uninformed game is the faithful ex-ante
reduction, not an unrelated game. -/
theorem infoHurts_reduction :
∀ a1 a2 : Fin 2,
gNoInfo.u1 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 =
gInfo.u1 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 +
gInfo.u1 ⟨0, by decide⟩ ⟨1, by decide⟩ a1 a2 ∧
gNoInfo.u2 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 =
gInfo.u2 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 +
gInfo.u2 ⟨0, by decide⟩ ⟨1, by decide⟩ a1 a2 := by
decide
/-! ### Canonical strategy constructors (informed game) -/-- Les deux jeux : gInfo (joueur 2 observe l'etat) vs gNoInfo (personne).
-- Le jeu informé : le joueur 2 observe privément θ (2 types), joueur 1 a 1 type.
/-- The informed game: player 2 privately observes the state θ (their
type), player 1 has a single type. Equal prior weights. -/
def gInfo : BayesGame2 where
nT1 := 1
nT2 := 2
nA1 := 2
nA2 := 2
w := fun _ _ => 1
u1 := fun _ t2 a1 a2 =>
if t2.val = 0 then
(if a1.val = 0 then (if a2.val = 0 then 2 else 0) else 0)
else
(if a1.val = 0 then (if a2.val = 0 then 2 else 0)
else (if a2.val = 0 then 0 else 4))
u2 := fun _ t2 a1 a2 =>
if t2.val = 0 then
(if a1.val = 0 then (if a2.val = 0 then 3 else 0)
else (if a2.val = 0 then 2 else 0))
else
(if a1.val = 0 then (if a2.val = 0 then 2 else 3)
else (if a2.val = 0 then 0 else 1))
-- Le jeu non informé : personne n'observe θ, payoffs sommés sur les 2 états
-- (réduction ex-ante fidèle de gInfo, cf. infoHurts_reduction ci-dessous).
/-- The uninformed benchmark: nobody observes θ, so both players have a
single type and payoffs are summed over the two states (ex-ante
reduction of `gInfo` for an uninformed player 2). -/
def gNoInfo : BayesGame2 where
nT1 := 1
nT2 := 1
nA1 := 2
nA2 := 2
w := fun _ _ => 1
u1 := fun _ _ a1 a2 =>
if a1.val = 0 then (if a2.val = 0 then 4 else 0)
else (if a2.val = 0 then 0 else 4)
u2 := fun _ _ a1 a2 =>
if a1.val = 0 then (if a2.val = 0 then 5 else 3)
else (if a2.val = 0 then 2 else 1)
-- Vérification (kernel-décidée) : gNoInfo est bien la somme de gInfo sur θ.
-- Ce n'est pas un jeu indépendant -- c'est la MEME situation, le joueur 2
-- voyant juste moins.
/-- Sanity check: `gNoInfo`'s payoffs are exactly `gInfo`'s summed over
the two states — the uninformed game is the faithful ex-ante
reduction, not an unrelated game. -/
theorem infoHurts_reduction :
∀ a1 a2 : Fin 2,
gNoInfo.u1 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 =
gInfo.u1 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 +
gInfo.u1 ⟨0, by decide⟩ ⟨1, by decide⟩ a1 a2 ∧
gNoInfo.u2 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 =
gInfo.u2 ⟨0, by decide⟩ ⟨0, by decide⟩ a1 a2 +
gInfo.u2 ⟨0, by decide⟩ ⟨1, by decide⟩ a1 a2 := by
decide
/-! ### Canonical strategy constructors (informed game) -/
--% env 14
{"cmd": "-- Les deux jeux : gInfo (joueur 2 observe l'etat) vs gNoInfo (personne).\n\n-- Le jeu inform\u00e9 : le joueur 2 observe priv\u00e9ment \u03b8 (2 types), joueur 1 a 1 type.\n/-- The informed game: player 2 privately observes the state \u03b8 (their\n type), player 1 has a single type. Equal prior weights. -/\ndef gInfo : BayesGame2 where\n nT1 := 1\n nT2 := 2\n nA1 := 2\n nA2 := 2\n w := fun _ _ => 1\n u1 := fun _ t2 a1 a2 =>\n if t2.val = 0 then\n (if a1.val = 0 then (if a2.val = 0 then 2 else 0) else 0)\n else\n (if a1.val = 0 then (if a2.val = 0 then 2 else 0)\n else (if a2.val = 0 then 0 else 4))\n u2 := fun _ t2 a1 a2 =>\n if t2.val = 0 then\n (if a1.val = 0 then (if a2.val = 0 then 3 else 0)\n else (if a2.val = 0 then 2 else 0))\n else\n (if a1.val = 0 then (if a2.val = 0 then 2 else 3)\n else (if a2.val = 0 then 0 else 1))\n\n-- Le jeu non inform\u00e9 : personne n'observe \u03b8, payoffs somm\u00e9s sur les 2 \u00e9tats\n-- (r\u00e9duction ex-ante fid\u00e8le de gInfo, cf. infoHurts_reduction ci-dessous).\n/-- The uninformed benchmark: nobody observes \u03b8, so both players have a\n single type and payoffs are summed over the two states (ex-ante\n reduction of `gInfo` for an uninformed player 2). -/\ndef gNoInfo : BayesGame2 where\n nT1 := 1\n nT2 := 1\n nA1 := 2\n nA2 := 2\n w := fun _ _ => 1\n u1 := fun _ _ a1 a2 =>\n if a1.val = 0 then (if a2.val = 0 then 4 else 0)\n else (if a2.val = 0 then 0 else 4)\n u2 := fun _ _ a1 a2 =>\n if a1.val = 0 then (if a2.val = 0 then 5 else 3)\n else (if a2.val = 0 then 2 else 1)\n\n-- V\u00e9rification (kernel-d\u00e9cid\u00e9e) : gNoInfo est bien la somme de gInfo sur \u03b8.\n-- Ce n'est pas un jeu ind\u00e9pendant -- c'est la MEME situation, le joueur 2\n-- voyant juste moins.\n/-- Sanity check: `gNoInfo`'s payoffs are exactly `gInfo`'s summed over\n the two states \u2014 the uninformed game is the faithful ex-ante\n reduction, not an unrelated game. -/\ntheorem infoHurts_reduction :\n \u2200 a1 a2 : Fin 2,\n gNoInfo.u1 \u27e80, by decide\u27e9 \u27e80, by decide\u27e9 a1 a2 =\n gInfo.u1 \u27e80, by decide\u27e9 \u27e80, by decide\u27e9 a1 a2 +\n gInfo.u1 \u27e80, by decide\u27e9 \u27e81, by decide\u27e9 a1 a2 \u2227\n gNoInfo.u2 \u27e80, by decide\u27e9 \u27e80, by decide\u27e9 a1 a2 =\n gInfo.u2 \u27e80, by decide\u27e9 \u27e80, by decide\u27e9 a1 a2 +\n gInfo.u2 \u27e80, by decide\u27e9 \u27e81, by decide\u27e9 a1 a2 := by\n decide\n\n/-! ### Canonical strategy constructors (informed game) -/", "env": 13}
{"env": 14}
Lecture de la rente d’information Vickrey (cellule code[7]) :
/-- Le type haut garde une rente d'information strictement positive (instance concrète décidable). -/
theorem spa_truthful_pos_three :
0 < interimU1 (spa 3) ⟨2, by decide⟩
(spaTruthful1 3 ⟨2, by decide⟩) (spaTruthful2 3) := by
decide
-- Valeur concrète de l'utilité interim du type haut (valuations {0,1,2}) :
#eval interimU1 (spa 3) (2 : Fin 3) (spaTruthful1 3 (2 : Fin 3)) (spaTruthful2 3)Pourquoi by decide : les quantificateurs ne portent que sur des Fin et des comparaisons Int — sur l’instance concrète spa 3, Lean énumère et tranche 0 < interimU1 ... automatiquement.
Qu’est-ce que la “rente d’information” : c’est l’utilité supplémentaire que le joueur de type haut obtient grâce à son information privée. Dans Vickrey, le joueur de type haut H peut deviner que l’autre joueur est de type bas L (si la distribution a priori le suggère), donc il ajuste son enchère en conséquence.
Détail du calcul (valuations {0, 1, 2}, type haut = 2, prior uniforme) : le type haut gagne contre 0 en payant 0, contre 1 en payant 1, et fait égalité contre 2 (surplus nul) — d’où la rente 6 à l’échelle 2 affichée par le #eval.
Référence : Vickrey (1961) + Maskin-Riley (2003) sur l’unicité de l’équilibre Vickrey.
Sortie attendue : #eval interimU1 (spa 3) (2 : Fin 3) (spaTruthful1 3 (2 : Fin 3)) (spaTruthful2 3) : 6.
Coût : < 200 ms pour decide sur l’instance 3×3.
Pour comparer les paiements d’équilibre, il faut caractériser les BNE de chaque jeu. La technique (canonique en théorie des jeux finis en Lean) : réduire toute stratégie à un constructeur canonique (mkS1g/mkS2g, une η-expansion sur les littéraux Fin), puis laisser le kernel décider l’énoncé fini résultant par calcul. L’unicité et les paiements exacts tombent alors par decide.
(Cellules code[15-17] : constructeurs et analyse d’équilibre des deux jeux.)
-- Constructeurs canoniques + eta-expansions (jeu informé).
-- Stratégies du joueur 1 = constantes (un seul type).
/-- Player 1's strategies in `gInfo` are constants (one type). -/
def mkS1g (x : Fin 2) : Strategy1 gInfo := fun _ => x
-- Stratégies du joueur 2 = deux actions contingentes au type θ.
/-- Player 2's strategies in `gInfo`, from the two type-contingent
actions. -/
def mkS2g (y z : Fin 2) : Strategy2 gInfo :=
fun t2 => if t2.val = 0 then y else z
-- Toute stratégie du joueur 1 est une constante canonique.
/-- Every strategy of player 1 is a canonical constant. -/
theorem s1g_eta (s1 : Strategy1 gInfo) : s1 = mkS1g (s1 ⟨0, by decide⟩) := by
funext t1
cases t1 using Fin.cases with
| zero => rfl
| succ j => exact j.elim0
-- Toute stratégie du joueur 2 est déterminée par ses deux valeurs.
/-- Every strategy of player 2 is determined by its two values. -/
theorem s2g_eta (s2 : Strategy2 gInfo) :
s2 = mkS2g (s2 ⟨0, by decide⟩) (s2 ⟨1, by decide⟩) := by
funext t2
cases t2 using Fin.cases with
| zero => rfl
| succ j =>
cases j using Fin.cases with
| zero => rfl
| succ j' => exact j'.elim0
/-! ### Equilibrium analysis of the informed game -/-- Constructeurs canoniques + eta-expansions (jeu informé).
-- Stratégies du joueur 1 = constantes (un seul type).
/-- Player 1's strategies in `gInfo` are constants (one type). -/
def mkS1g (x : Fin 2) : Strategy1 gInfo := fun _ => x
-- Stratégies du joueur 2 = deux actions contingentes au type θ.
/-- Player 2's strategies in `gInfo`, from the two type-contingent
actions. -/
def mkS2g (y z : Fin 2) : Strategy2 gInfo :=
fun t2 => if t2.val = 0 then y else z
-- Toute stratégie du joueur 1 est une constante canonique.
/-- Every strategy of player 1 is a canonical constant. -/
theorem s1g_eta (s1 : Strategy1 gInfo) : s1 = mkS1g (s1 ⟨0, by decide⟩) := by
funext t1
cases t1 using Fin.cases with
| zero => rfl
| succ j => exact j.elim0
-- Toute stratégie du joueur 2 est déterminée par ses deux valeurs.
/-- Every strategy of player 2 is determined by its two values. -/
theorem s2g_eta (s2 : Strategy2 gInfo) :
s2 = mkS2g (s2 ⟨0, by decide⟩) (s2 ⟨1, by decide⟩) := by
funext t2
cases t2 using Fin.cases with
| zero => rfl
| succ j =>
cases j using Fin.cases with
| zero => rfl
| succ j' => exact j'.elim0
/-! ### Equilibrium analysis of the informed game -/
--% env 15
{"cmd": "-- Constructeurs canoniques + eta-expansions (jeu inform\u00e9).\n\n-- Strat\u00e9gies du joueur 1 = constantes (un seul type).\n/-- Player 1's strategies in `gInfo` are constants (one type). -/\ndef mkS1g (x : Fin 2) : Strategy1 gInfo := fun _ => x\n\n-- Strat\u00e9gies du joueur 2 = deux actions contingentes au type \u03b8.\n/-- Player 2's strategies in `gInfo`, from the two type-contingent\n actions. -/\ndef mkS2g (y z : Fin 2) : Strategy2 gInfo :=\n fun t2 => if t2.val = 0 then y else z\n\n-- Toute strat\u00e9gie du joueur 1 est une constante canonique.\n/-- Every strategy of player 1 is a canonical constant. -/\ntheorem s1g_eta (s1 : Strategy1 gInfo) : s1 = mkS1g (s1 \u27e80, by decide\u27e9) := by\n funext t1\n cases t1 using Fin.cases with\n | zero => rfl\n | succ j => exact j.elim0\n\n-- Toute strat\u00e9gie du joueur 2 est d\u00e9termin\u00e9e par ses deux valeurs.\n/-- Every strategy of player 2 is determined by its two values. -/\ntheorem s2g_eta (s2 : Strategy2 gInfo) :\n s2 = mkS2g (s2 \u27e80, by decide\u27e9) (s2 \u27e81, by decide\u27e9) := by\n funext t2\n cases t2 using Fin.cases with\n | zero => rfl\n | succ j =>\n cases j using Fin.cases with\n | zero => rfl\n | succ j' => exact j'.elim0\n\n/-! ### Equilibrium analysis of the informed game -/", "env": 14}
{"env": 15}
-- Équilibre du jeu informé : joueur 2 révèle l'état, joueur 1 joue B.
-- Paiement d'équilibre du joueur 2 = 3 (kernel-décidé).
-- (B, suivre-l'état) est un BNE du jeu informé.
/-- (B, follow-the-state) is a BNE of the informed game. -/
theorem gInfo_bne :
isBNE gInfo (mkS1g ⟨1, by decide⟩) (mkS2g ⟨0, by decide⟩ ⟨1, by decide⟩) := by
decide
-- Sur stratégies canoniques : unicité du BNE de gInfo.
/-- Over canonical strategies, the BNE of `gInfo` is unique: player 1
plays B and player 2 plays l on θ=0, r on θ=1. -/
theorem gInfo_unique_aux :
∀ x y z : Fin 2,
isBNE gInfo (mkS1g x) (mkS2g y z) →
x = ⟨1, by decide⟩ ∧ y = ⟨0, by decide⟩ ∧ z = ⟨1, by decide⟩ := by
decide
-- Sur stratégies canoniques : tout BNE de gInfo paie 3 au joueur 2.
/-- Over canonical strategies, every BNE of `gInfo` pays player 2
exactly 3. -/
theorem gInfo_exAnteU2_aux :
∀ x y z : Fin 2,
isBNE gInfo (mkS1g x) (mkS2g y z) →
exAnteU2 gInfo (mkS1g x) (mkS2g y z) = 3 := by
decide
-- Le jeu informé a un BNE essentiellement unique.
/-- The informed game has an essentially unique BNE. -/
theorem gInfo_unique (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)
(h : isBNE gInfo s1 s2) :
s1 = mkS1g ⟨1, by decide⟩ ∧ s2 = mkS2g ⟨0, by decide⟩ ⟨1, by decide⟩ := by
rw [s1g_eta s1, s2g_eta s2] at h
have hu := gInfo_unique_aux _ _ _ h
exact ⟨by rw [s1g_eta s1, hu.1], by rw [s2g_eta s2, hu.2.1, hu.2.2]⟩
-- En tout BNE du jeu informé, le joueur 2 gagne 3.
/-- In every BNE of the informed game, player 2 earns 3. -/
theorem gInfo_bne_payoff (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)
(h : isBNE gInfo s1 s2) : exAnteU2 gInfo s1 s2 = 3 := by
rw [s1g_eta s1, s2g_eta s2] at h ⊢
exact gInfo_exAnteU2_aux _ _ _ h
/-! ### Equilibrium analysis of the uninformed game -/
#eval exAnteU2 gInfo (mkS1g ⟨1, by decide⟩) (mkS2g ⟨0, by decide⟩ ⟨1, by decide⟩)-- Équilibre du jeu informé : joueur 2 révèle l'état, joueur 1 joue B.
-- Paiement d'équilibre du joueur 2 = 3 (kernel-décidé).
-- (B, suivre-l'état) est un BNE du jeu informé.
/-- (B, follow-the-state) is a BNE of the informed game. -/
theorem gInfo_bne :
isBNE gInfo (mkS1g ⟨1, by decide⟩) (mkS2g ⟨0, by decide⟩ ⟨1, by decide⟩) := by
decide
-- Sur stratégies canoniques : unicité du BNE de gInfo.
/-- Over canonical strategies, the BNE of `gInfo` is unique: player 1
plays B and player 2 plays l on θ=0, r on θ=1. -/
theorem gInfo_unique_aux :
∀ x y z : Fin 2,
isBNE gInfo (mkS1g x) (mkS2g y z) →
x = ⟨1, by decide⟩ ∧ y = ⟨0, by decide⟩ ∧ z = ⟨1, by decide⟩ := by
decide
-- Sur stratégies canoniques : tout BNE de gInfo paie 3 au joueur 2.
/-- Over canonical strategies, every BNE of `gInfo` pays player 2
exactly 3. -/
theorem gInfo_exAnteU2_aux :
∀ x y z : Fin 2,
isBNE gInfo (mkS1g x) (mkS2g y z) →
exAnteU2 gInfo (mkS1g x) (mkS2g y z) = 3 := by
decide
-- Le jeu informé a un BNE essentiellement unique.
/-- The informed game has an essentially unique BNE. -/
theorem gInfo_unique (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)
(h : isBNE gInfo s1 s2) :
s1 = mkS1g ⟨1, by decide⟩ ∧ s2 = mkS2g ⟨0, by decide⟩ ⟨1, by decide⟩ := by
rw [s1g_eta s1, s2g_eta s2] at h
have hu := gInfo_unique_aux _ _ _ h
exact ⟨by rw [s1g_eta s1, hu.1], by rw [s2g_eta s2, hu.2.1, hu.2.2]⟩
-- En tout BNE du jeu informé, le joueur 2 gagne 3.
/-- In every BNE of the informed game, player 2 earns 3. -/
theorem gInfo_bne_payoff (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)
(h : isBNE gInfo s1 s2) : exAnteU2 gInfo s1 s2 = 3 := by
rw [s1g_eta s1, s2g_eta s2] at h ⊢
exact gInfo_exAnteU2_aux _ _ _ h
/-! ### Equilibrium analysis of the uninformed game -/
3
--% env 16
{"cmd": "-- \u00c9quilibre du jeu inform\u00e9 : joueur 2 r\u00e9v\u00e8le l'\u00e9tat, joueur 1 joue B.\n-- Paiement d'\u00e9quilibre du joueur 2 = 3 (kernel-d\u00e9cid\u00e9).\n\n-- (B, suivre-l'\u00e9tat) est un BNE du jeu inform\u00e9.\n/-- (B, follow-the-state) is a BNE of the informed game. -/\ntheorem gInfo_bne :\n isBNE gInfo (mkS1g \u27e81, by decide\u27e9) (mkS2g \u27e80, by decide\u27e9 \u27e81, by decide\u27e9) := by\n decide\n\n-- Sur strat\u00e9gies canoniques : unicit\u00e9 du BNE de gInfo.\n/-- Over canonical strategies, the BNE of `gInfo` is unique: player 1\n plays B and player 2 plays l on \u03b8=0, r on \u03b8=1. -/\ntheorem gInfo_unique_aux :\n \u2200 x y z : Fin 2,\n isBNE gInfo (mkS1g x) (mkS2g y z) \u2192\n x = \u27e81, by decide\u27e9 \u2227 y = \u27e80, by decide\u27e9 \u2227 z = \u27e81, by decide\u27e9 := by\n decide\n\n-- Sur strat\u00e9gies canoniques : tout BNE de gInfo paie 3 au joueur 2.\n/-- Over canonical strategies, every BNE of `gInfo` pays player 2\n exactly 3. -/\ntheorem gInfo_exAnteU2_aux :\n \u2200 x y z : Fin 2,\n isBNE gInfo (mkS1g x) (mkS2g y z) \u2192\n exAnteU2 gInfo (mkS1g x) (mkS2g y z) = 3 := by\n decide\n\n-- Le jeu inform\u00e9 a un BNE essentiellement unique.\n/-- The informed game has an essentially unique BNE. -/\ntheorem gInfo_unique (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)\n (h : isBNE gInfo s1 s2) :\n s1 = mkS1g \u27e81, by decide\u27e9 \u2227 s2 = mkS2g \u27e80, by decide\u27e9 \u27e81, by decide\u27e9 := by\n rw [s1g_eta s1, s2g_eta s2] at h\n have hu := gInfo_unique_aux _ _ _ h\n exact \u27e8by rw [s1g_eta s1, hu.1], by rw [s2g_eta s2, hu.2.1, hu.2.2]\u27e9\n\n-- En tout BNE du jeu inform\u00e9, le joueur 2 gagne 3.\n/-- In every BNE of the informed game, player 2 earns 3. -/\ntheorem gInfo_bne_payoff (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)\n (h : isBNE gInfo s1 s2) : exAnteU2 gInfo s1 s2 = 3 := by\n rw [s1g_eta s1, s2g_eta s2] at h \u22a2\n exact gInfo_exAnteU2_aux _ _ _ h\n\n/-! ### Equilibrium analysis of the uninformed game -/\n\n#eval exAnteU2 gInfo (mkS1g \u27e81, by decide\u27e9) (mkS2g \u27e80, by decide\u27e9 \u27e81, by decide\u27e9)", "env": 15}
{"messages":
[{"severity": "info",
"pos": {"line": 46, "column": 0},
"endPos": {"line": 46, "column": 5},
"data": "3"}],
"env": 16}
-- Équilibre du jeu non informé : joueur 2 joue l (strictement dominant),
-- joueur 1 joue T. Paiement d'équilibre du joueur 2 = 5 (kernel-décidé).
-- Stratégies canoniques du jeu non informé (un type chaque).
/-- Player 1's strategies in `gNoInfo` are constants. -/
def mkS1n (x : Fin 2) : Strategy1 gNoInfo := fun _ => x
/-- Player 2's strategies in `gNoInfo` are constants. -/
def mkS2n (y : Fin 2) : Strategy2 gNoInfo := fun _ => y
-- Eta-expansions.
theorem s1n_eta (s1 : Strategy1 gNoInfo) : s1 = mkS1n (s1 ⟨0, by decide⟩) := by
funext t1
cases t1 using Fin.cases with
| zero => rfl
| succ j => exact j.elim0
theorem s2n_eta (s2 : Strategy2 gNoInfo) : s2 = mkS2n (s2 ⟨0, by decide⟩) := by
funext t2
cases t2 using Fin.cases with
| zero => rfl
| succ j => exact j.elim0
-- (T, l) est un BNE du jeu non informé.
/-- (T, l) is a BNE of the uninformed game. -/
theorem gNoInfo_bne :
isBNE gNoInfo (mkS1n ⟨0, by decide⟩) (mkS2n ⟨0, by decide⟩) := by
decide
-- Sur stratégies canoniques : tout BNE de gNoInfo paie 5 au joueur 2.
/-- Over canonical strategies, every BNE of `gNoInfo` pays player 2
exactly 5 (the BNE (T, l) is in fact unique, by strict dominance
of l). -/
theorem gNoInfo_exAnteU2_aux :
∀ x y : Fin 2,
isBNE gNoInfo (mkS1n x) (mkS2n y) →
exAnteU2 gNoInfo (mkS1n x) (mkS2n y) = 5 := by
decide
-- En tout BNE du jeu non informé, le joueur 2 gagne 5.
/-- In every BNE of the uninformed game, player 2 earns 5. -/
theorem gNoInfo_bne_payoff (s1 : Strategy1 gNoInfo) (s2 : Strategy2 gNoInfo)
(h : isBNE gNoInfo s1 s2) : exAnteU2 gNoInfo s1 s2 = 5 := by
rw [s1n_eta s1, s2n_eta s2] at h ⊢
exact gNoInfo_exAnteU2_aux _ _ h
/-! ### Punchline -/
#eval exAnteU2 gNoInfo (mkS1n ⟨0, by decide⟩) (mkS2n ⟨0, by decide⟩)-- Équilibre du jeu non informé : joueur 2 joue l (strictement dominant),
-- joueur 1 joue T. Paiement d'équilibre du joueur 2 = 5 (kernel-décidé).
-- Stratégies canoniques du jeu non informé (un type chaque).
/-- Player 1's strategies in `gNoInfo` are constants. -/
def mkS1n (x : Fin 2) : Strategy1 gNoInfo := fun _ => x
/-- Player 2's strategies in `gNoInfo` are constants. -/
def mkS2n (y : Fin 2) : Strategy2 gNoInfo := fun _ => y
-- Eta-expansions.
theorem s1n_eta (s1 : Strategy1 gNoInfo) : s1 = mkS1n (s1 ⟨0, by decide⟩) := by
funext t1
cases t1 using Fin.cases with
| zero => rfl
| succ j => exact j.elim0
theorem s2n_eta (s2 : Strategy2 gNoInfo) : s2 = mkS2n (s2 ⟨0, by decide⟩) := by
funext t2
cases t2 using Fin.cases with
| zero => rfl
| succ j => exact j.elim0
-- (T, l) est un BNE du jeu non informé.
/-- (T, l) is a BNE of the uninformed game. -/
theorem gNoInfo_bne :
isBNE gNoInfo (mkS1n ⟨0, by decide⟩) (mkS2n ⟨0, by decide⟩) := by
decide
-- Sur stratégies canoniques : tout BNE de gNoInfo paie 5 au joueur 2.
/-- Over canonical strategies, every BNE of `gNoInfo` pays player 2
exactly 5 (the BNE (T, l) is in fact unique, by strict dominance
of l). -/
theorem gNoInfo_exAnteU2_aux :
∀ x y : Fin 2,
isBNE gNoInfo (mkS1n x) (mkS2n y) →
exAnteU2 gNoInfo (mkS1n x) (mkS2n y) = 5 := by
decide
-- En tout BNE du jeu non informé, le joueur 2 gagne 5.
/-- In every BNE of the uninformed game, player 2 earns 5. -/
theorem gNoInfo_bne_payoff (s1 : Strategy1 gNoInfo) (s2 : Strategy2 gNoInfo)
(h : isBNE gNoInfo s1 s2) : exAnteU2 gNoInfo s1 s2 = 5 := by
rw [s1n_eta s1, s2n_eta s2] at h ⊢
exact gNoInfo_exAnteU2_aux _ _ h
/-! ### Punchline -/
5
--% env 17
{"cmd": "-- \u00c9quilibre du jeu non inform\u00e9 : joueur 2 joue l (strictement dominant),\n-- joueur 1 joue T. Paiement d'\u00e9quilibre du joueur 2 = 5 (kernel-d\u00e9cid\u00e9).\n\n-- Strat\u00e9gies canoniques du jeu non inform\u00e9 (un type chaque).\n/-- Player 1's strategies in `gNoInfo` are constants. -/\ndef mkS1n (x : Fin 2) : Strategy1 gNoInfo := fun _ => x\n\n/-- Player 2's strategies in `gNoInfo` are constants. -/\ndef mkS2n (y : Fin 2) : Strategy2 gNoInfo := fun _ => y\n\n-- Eta-expansions.\ntheorem s1n_eta (s1 : Strategy1 gNoInfo) : s1 = mkS1n (s1 \u27e80, by decide\u27e9) := by\n funext t1\n cases t1 using Fin.cases with\n | zero => rfl\n | succ j => exact j.elim0\n\ntheorem s2n_eta (s2 : Strategy2 gNoInfo) : s2 = mkS2n (s2 \u27e80, by decide\u27e9) := by\n funext t2\n cases t2 using Fin.cases with\n | zero => rfl\n | succ j => exact j.elim0\n\n-- (T, l) est un BNE du jeu non inform\u00e9.\n/-- (T, l) is a BNE of the uninformed game. -/\ntheorem gNoInfo_bne :\n isBNE gNoInfo (mkS1n \u27e80, by decide\u27e9) (mkS2n \u27e80, by decide\u27e9) := by\n decide\n\n-- Sur strat\u00e9gies canoniques : tout BNE de gNoInfo paie 5 au joueur 2.\n/-- Over canonical strategies, every BNE of `gNoInfo` pays player 2\n exactly 5 (the BNE (T, l) is in fact unique, by strict dominance\n of l). -/\ntheorem gNoInfo_exAnteU2_aux :\n \u2200 x y : Fin 2,\n isBNE gNoInfo (mkS1n x) (mkS2n y) \u2192\n exAnteU2 gNoInfo (mkS1n x) (mkS2n y) = 5 := by\n decide\n\n-- En tout BNE du jeu non inform\u00e9, le joueur 2 gagne 5.\n/-- In every BNE of the uninformed game, player 2 earns 5. -/\ntheorem gNoInfo_bne_payoff (s1 : Strategy1 gNoInfo) (s2 : Strategy2 gNoInfo)\n (h : isBNE gNoInfo s1 s2) : exAnteU2 gNoInfo s1 s2 = 5 := by\n rw [s1n_eta s1, s2n_eta s2] at h \u22a2\n exact gNoInfo_exAnteU2_aux _ _ h\n\n/-! ### Punchline -/\n\n#eval exAnteU2 gNoInfo (mkS1n \u27e80, by decide\u27e9) (mkS2n \u27e80, by decide\u27e9)", "env": 16}
{"messages":
[{"severity": "info",
"pos": {"line": 49, "column": 0},
"endPos": {"line": 49, "column": 5},
"data": "5"}],
"env": 17}
Les deux #eval ci-dessus tranchent : le même joueur 2 gagne 3 quand il observe l’état (jeu informé) contre 5 quand il ne l’observe pas (jeu non informé). Les deux jeux ont la même échelle de poids prior (chaque valeur est deux fois l’espérance vraie, cf. infoHurts_reduction), donc 3 < 5 est une comparaison fidèle.
Non informé, l domine strictement pour le joueur 2 : l’équilibre unique (T, l) lui vaut 5. Informé, le type θ=1 ne peut plus s’engager à jouer l (r devient strictement dominant pour ce type) ; son action révèle alors θ au joueur 1, dont la meilleure réponse bascule de T vers B (2+0 < 0+4), laissant le joueur 2 avec 2+1 = 3 < 5. Connaître l’état détruit la capacité à s’engager — le joueur 2 paierait pour NE PAS voir le signal.
C’est l’exact pendant du théorème de Blackwell (section 5) : mono-joueur, l’information ne nuit jamais ; multi-joueur, elle peut nuire strictement. Les deux directions sont décidées par le kernel sur des instances concrètes.
-- **Punchline (kernel-décidée).**
-- L'information peut nuire dans un jeu : en tout équilibre, le joueur 2
-- informé gagne strictement moins (3) qu'en tout équilibre du jeu où personne
-- n'observe l'état (5). Contraste avec valueNoInfo_le_valueSignal (section 5) :
-- avec un décideur seul, l'information ne nuit jamais.
/-- **Information can hurt in games.** In every equilibrium, the
informed player 2 earns strictly less (3) than in every equilibrium
of the game where nobody observes the state (5): observing the
signal destroys player 2's ability to commit to `l`, reveals the
state through their action, and triggers a best-response switch by
player 1 that costs more than the informational gain. Contrast with
`valueNoInfo_le_valueSignal` (`Information.lean`): with a single
decision maker, information never hurts. -/
theorem information_hurts
(s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)
(t1 : Strategy1 gNoInfo) (t2 : Strategy2 gNoInfo)
(hI : isBNE gInfo s1 s2) (hN : isBNE gNoInfo t1 t2) :
exAnteU2 gInfo s1 s2 < exAnteU2 gNoInfo t1 t2 := by
rw [gInfo_bne_payoff s1 s2 hI, gNoInfo_bne_payoff t1 t2 hN]
decide
#check information_hurts-- **Punchline (kernel-décidée).**
-- L'information peut nuire dans un jeu : en tout équilibre, le joueur 2
-- informé gagne strictement moins (3) qu'en tout équilibre du jeu où personne
-- n'observe l'état (5). Contraste avec valueNoInfo_le_valueSignal (section 5) :
-- avec un décideur seul, l'information ne nuit jamais.
/-- **Information can hurt in games.** In every equilibrium, the
informed player 2 earns strictly less (3) than in every equilibrium
of the game where nobody observes the state (5): observing the
signal destroys player 2's ability to commit to `l`, reveals the
state through their action, and triggers a best-response switch by
player 1 that costs more than the informational gain. Contrast with
`valueNoInfo_le_valueSignal` (`Information.lean`): with a single
decision maker, information never hurts. -/
theorem information_hurts
(s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)
(t1 : Strategy1 gNoInfo) (t2 : Strategy2 gNoInfo)
(hI : isBNE gInfo s1 s2) (hN : isBNE gNoInfo t1 t2) :
exAnteU2 gInfo s1 s2 < exAnteU2 gNoInfo t1 t2 := by
rw [gInfo_bne_payoff s1 s2 hI, gNoInfo_bne_payoff t1 t2 hN]
decide
information_hurts (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo) (t1 : Strategy1 gNoInfo) (t2 : Strategy2 gNoInfo)
(hI : isBNE gInfo s1 s2) (hN : isBNE gNoInfo t1 t2) : exAnteU2 gInfo s1 s2 < exAnteU2 gNoInfo t1 t2
--% env 18
{"cmd": "-- **Punchline (kernel-d\u00e9cid\u00e9e).**\n\n-- L'information peut nuire dans un jeu : en tout \u00e9quilibre, le joueur 2\n-- inform\u00e9 gagne strictement moins (3) qu'en tout \u00e9quilibre du jeu o\u00f9 personne\n-- n'observe l'\u00e9tat (5). Contraste avec valueNoInfo_le_valueSignal (section 5) :\n-- avec un d\u00e9cideur seul, l'information ne nuit jamais.\n/-- **Information can hurt in games.** In every equilibrium, the\n informed player 2 earns strictly less (3) than in every equilibrium\n of the game where nobody observes the state (5): observing the\n signal destroys player 2's ability to commit to `l`, reveals the\n state through their action, and triggers a best-response switch by\n player 1 that costs more than the informational gain. Contrast with\n `valueNoInfo_le_valueSignal` (`Information.lean`): with a single\n decision maker, information never hurts. -/\ntheorem information_hurts\n (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo)\n (t1 : Strategy1 gNoInfo) (t2 : Strategy2 gNoInfo)\n (hI : isBNE gInfo s1 s2) (hN : isBNE gNoInfo t1 t2) :\n exAnteU2 gInfo s1 s2 < exAnteU2 gNoInfo t1 t2 := by\n rw [gInfo_bne_payoff s1 s2 hI, gNoInfo_bne_payoff t1 t2 hN]\n decide\n\n#check information_hurts", "env": 17}
{"messages":
[{"severity": "info",
"pos": {"line": 23, "column": 0},
"endPos": {"line": 23, "column": 6},
"data":
"information_hurts (s1 : Strategy1 gInfo) (s2 : Strategy2 gInfo) (t1 : Strategy1 gNoInfo) (t2 : Strategy2 gNoInfo)\n (hI : isBNE gInfo s1 s2) (hN : isBNE gNoInfo t1 t2) : exAnteU2 gInfo s1 s2 < exAnteU2 gNoInfo t1 t2"}],
"env": 18}
Lecture de gInfo vs gNoInfo (contre-exemple) (cellule code[14]) :
/-- The informed game: player 2 privately observes the state θ (their
type), player 1 has a single type. Equal prior weights. -/
def gInfo : BayesGame2 where
nT1 := 1
nT2 := 2
nA1 := 2
nA2 := 2
w := fun _ _ => 1
u1 := fun _ t2 a1 a2 =>
if t2.val = 0 then
(if a1.val = 0 then (if a2.val = 0 then 2 else 0) else 0)
else
(if a1.val = 0 then (if a2.val = 0 then 2 else 0)
else (if a2.val = 0 then 0 else 4))
u2 := fun _ t2 a1 a2 =>
if t2.val = 0 then
(if a1.val = 0 then (if a2.val = 0 then 3 else 0)
else (if a2.val = 0 then 2 else 0))
else
(if a1.val = 0 then (if a2.val = 0 then 2 else 3)
else (if a2.val = 0 then 0 else 1))
-- Le jeu non informé : personne n'observe θ, payoffs sommés sur les 2 états
-- (réduction ex-ante fidèle de gInfo, cf. infoHurts_reduction ci-dessous).
/-- The uninformed benchmark: nobody observes θ, so both players have a
single type and payoffs are summed over the two states (ex-ante
reduction of `gInfo` for an uninformed player 2). -/
def gNoInfo : BayesGame2 where
nT1 := 1
nT2 := 1
nA1 := 2
nA2 := 2
w := fun _ _ => 1
u1 := fun _ _ a1 a2 =>
if a1.val = 0 then (if a2.val = 0 then 4 else 0)
else (if a2.val = 0 then 0 else 4)
u2 := fun _ _ a1 a2 =>
if a1.val = 0 then (if a2.val = 0 then 5 else 3)
else (if a2.val = 0 then 2 else 1)Deux jeux, une seule différence : dans gInfo le joueur 2 observe privément θ (deux types), dans gNoInfo personne ne l’observe (un type chacun) ; gNoInfo est la réduction ex-ante fidèle de gInfo — ses payoffs sont exactement ceux de gInfo sommés sur les deux états, vérifié par infoHurts_reduction.
Le phénomène attendu : le paiement d’équilibre du joueur 2 est strictement inférieur dans gInfo (3) que dans gNoInfo (5) — recevoir le signal détruit sa capacité à s’engager sur l (punchline information_hurts).
Référence : Osborne-Rubinstein (1994) “A Course in Game Theory” ; construction de lean_game_defs_ext/Bayesian/InfoGames.lean.
Sortie attendue (cellules code[14-18]) : 2 jeux définis, équilibres décidés (gInfo_bne, gNoInfo_bne, unicité sur stratégies canoniques), punchline information_hurts (3 < 5).
Coût : < 500 ms pour l’ensemble (def + eq + comparaison).
Ce notebook a restaté et exécuté le résultat central — le théorème de Vickrey (spa_truthful_bne, valable pour tout n, 0 sorry) — dans le kernel lean4-wsl. Le lake lean_game_defs_ext/Bayesian prouve en outre, également sans sorry :
isBNE_scaleW (BNE.lean) : le statut de BNE est invariant par remise à l’échelle du prior (indépendance de normalisation — les poids Nat représentent toute mesure de probabilité proportionnelle).exAnteU1/2_le_of_interim_best, bne_exAnte) : l’optimalité interim implique l’optimalité ex-ante contre toute déviation contingente au type.Information.lean, valueSignal_mono) : pour un décideur seul, un signal plus fin (σ = h ∘ τ) vaut au moins autant — l’information ne nuit jamais à un joueur solitaire (mais peut nuire strictement dans un jeu — exécuté section 6 ci-dessous, cf. InfoGames.lean : joueur 2 informé = 3 < 5 non informé). Exécuté section 5 ci-dessus (instance umbrella décidée : valueNoInfo = 2 < valuePerfect = 5).Auction.lean) : l’enchère honnête n’y est pas un BNE (truthful_not_bne_two/three).Ces résultats se vérifient par la compilation du lake ci-dessus (lake build Bayesian, 0 sorry). Le pattern self-contained de ce notebook (restate inline, kernel élabore les vrais énoncés) est exactement celui des notebooks 2b/4b/8b/15b.
L’extension à l’import direct d’un lake depuis le kernel lean4-wsl (prelude NotebookCtx, lancement via lake-env) est étudiée en side-track sur l’issue #4251 (Part of #4038).