DecInfer-02-Théorème de représentation de von Neumann–Morgenstern (companion formel natif)

Ce notebook est le companion formel du lake decision_theory_lean (lib Utility), qui prouve la direction sound du théorème de représentation d’utilité espérée de von Neumann–Morgenstern : si une fonction d’utilité u représente une préférence P (P p q ↔︎ E_p[u] ≥ E_q[u]), alors P est rationnelle (satisfait les quatre axiomes vNM), sans sorry.

La cohérence de de Finetti (prix non arbitrage ⟺ bornes de probabilité, lib Coherence) a son companion dédié : DecInfer-02b-Lean-Coherence.

Ce notebook est le fondement formel du classement par espérance d’utilité — la justification décisionnelle des notebooks DecInfer-01 (Infer.NET) et PyMC-1 (PyMC), où l’utilité espérée est calculée sous incertitude bayésienne.

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

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

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

1. Import des modules `Utility` du lake `decision_theory_lean`

Le lake porte des libs indépendantes (Utility, Gittins, Coherence). On importe uniquement les modules de Utility (Basic, Axioms, Representation) — la lib Utility est déclarée via roots := #[Utility], qui ne build **pas** l'umbrella racineUtility.olean(on importe donc les modules directement). On éviteGittins(sorries HOLD). La libCoherence` — également sorry-free — a son companion dédié DecInfer-02b-Lean-Coherence : ce notebook cible le seul théorème vNM.

import Utility.Basic
import Utility.Axioms
import Utility.Representation
open Utility

import Utility.Basic

import Utility.Axioms

import Utility.Representation

open Utility

--% env 0

Raw input

{"cmd": "import Utility.Basic\nimport Utility.Axioms\nimport Utility.Representation\nopen Utility\n"}

Raw output

{"env": 0}

2. Preuve sans `sorry` — `#print axioms`

Le théorème phare expected_utility_rep_is_rational (direction sound : représentation ⟹ rationalité) ne dépend que des 3 axiomes standards de Lean (propext, Classical.choice, Quot.sound) — pas de sorryAx — ce qui prouve que la preuve est complète.

#print axioms expected_utility_rep_is_rational

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

--% env 1

Raw input

{"cmd": "#print axioms expected_utility_rep_is_rational", "env": 0}

Raw output

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

3. Loteries, espérance et mélange convexe

Le module Utility/Basic.lean pose les primitives de la décision dans le risque :

Lottery α — une loterie : poids non négatifs par issue, sommant à 1 (distribution à support fini sur α).
expectation p f — l’espérance de f (typiquement une utilité) sous p : ∑ a, p.probs a * f a.
mix t p r — le mélange convexe t • p + (1 - t) • r (valide pour t ∈ [0,1]).
expectation_mix — l’identité affine clé : E_{mix}[f] = t·E_p[f] + (1-t)·E_r[f] (cœur algébrique de l’indépendance).
expectation_affine — E_p[a·u + b] = a·E_p[u] + b (cœur de l’unicité affine de l’utilité).

#check Lottery
#check expectation
#check mix
#check expectation_mix
#check expectation_affine

#check Lottery Utility.Lottery.{u_2} (α : Type u_2) [Fintype α] : Type u_2

#check expectation Utility.expectation.{u_1} {α : Type u_1} [Fintype α] (p : Lottery α) (f : α → ℝ) : ℝ

#check mix Utility.mix.{u_1} {α : Type u_1} [Fintype α] (t : ℝ) (p r : Lottery α) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Lottery α

#check expectation_mix Utility.expectation_mix.{u_1} {α : Type u_1} [Fintype α] (t : ℝ) (p r : Lottery α) (f : α → ℝ) (ht0 : 0 ≤ t)
  (ht1 : t ≤ 1) : expectation (mix t p r ht0 ht1) f = t * expectation p f + (1 - t) * expectation r f

#check expectation_affine Utility.expectation_affine.{u_1} {α : Type u_1} [Fintype α] (p : Lottery α) (a b : ℝ) (u : α → ℝ) :
  (expectation p fun x => a * u x + b) = a * expectation p u + b

--% env 2

Raw input

{"cmd": "#check Lottery\n#check expectation\n#check mix\n#check expectation_mix\n#check expectation_affine", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data": "Utility.Lottery.{u_2} (α : Type u_2) [Fintype α] : Type u_2"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Utility.expectation.{u_1} {α : Type u_1} [Fintype α] (p : Lottery α) (f : α → ℝ) : ℝ"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Utility.mix.{u_1} {α : Type u_1} [Fintype α] (t : ℝ) (p r : Lottery α) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : Lottery α"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Utility.expectation_mix.{u_1} {α : Type u_1} [Fintype α] (t : ℝ) (p r : Lottery α) (f : α → ℝ) (ht0 : 0 ≤ t)\n  (ht1 : t ≤ 1) : expectation (mix t p r ht0 ht1) f = t * expectation p f + (1 - t) * expectation r f"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Utility.expectation_affine.{u_1} {α : Type u_1} [Fintype α] (p : Lottery α) (a b : ℝ) (u : α → ℝ) :\n  (expectation p fun x => a * u x + b) = a * expectation p u + b"}],
 "env": 2}

Lecture : l’algèbre de l’espérance

Symbole Lean	Lecture
`Lottery α`	distribution à support fini (`probs`, `nonneg`, `sum_one`)
`expectation p f`	`∑ a, p.probs a * f a`
`mix t p r`	mélange convexe `t·p + (1-t)·r`
`expectation_mix`	`E_{mix}[f] = t·E_p[f] + (1-t)·E_r[f]` (affinité)
`expectation_affine`	`E_p[a·u+b] = a·E_p[u] + b` (unicité affine)

4. Les quatre axiomes de rationalité de von Neumann–Morgenstern

Le module Utility/Axioms.lean formalise les quatre axiomes qu’une préférence sur les loteries doit satisfaire pour admettre une représentation en utilité espérée :

Pref α = Lottery α → Lottery α → Prop — une préférence (P p q se lit « p ≽ q »).
IsComplete P — complétude : toute paire de loteries est comparable.
IsTransitive P — transitivité : les chaînes de préférence ne cyclent pas.
IsIndependent P — indépendance (substitution) : un mélange commun préserve la préférence.
IsContinuous P — continuité (Archimède) : pas de loterie infiniment meilleure ; des mélanges intermédiaires existent.
IsRational P — une préférence rationnelle satisfait les quatre axiomes (structure).

#check Pref
#check IsComplete
#check IsTransitive
#check IsIndependent
#check IsContinuous
#check IsRational

#check Pref Utility.Pref.{u_2} (α : Type u_2) [Fintype α] : Type u_2

#check IsComplete Utility.IsComplete.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop

#check IsTransitive Utility.IsTransitive.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop

#check IsIndependent Utility.IsIndependent.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop

#check IsContinuous Utility.IsContinuous.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop

#check IsRational Utility.IsRational.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop

--% env 3

Raw input

{"cmd": "#check Pref\n#check IsComplete\n#check IsTransitive\n#check IsIndependent\n#check IsContinuous\n#check IsRational", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data": "Utility.Pref.{u_2} (α : Type u_2) [Fintype α] : Type u_2"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Utility.IsComplete.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Utility.IsTransitive.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Utility.IsIndependent.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Utility.IsContinuous.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Utility.IsRational.{u_1} {α : Type u_1} [Fintype α] (P : Pref α) : Prop"}],
 "env": 3}

Lecture : les quatre piliers de la rationalité

Axiome	Lecture
`Pref α`	relation binaire sur les loteries (`p ≽ q`)
`IsComplete`	toute paire comparable
`IsTransitive`	`p ≽ q ≽ r ⟹ p ≽ r`
`IsIndependent`	`p ≽ q ⟹ mix t p r ≽ mix t q r`
`IsContinuous`	`p ≽ q ≽ r ⟹ ∃ t, mix t p r ~ q` (Archimède)
`IsRational`	satisfait les quatre (structure)

5. Le théorème de représentation : direction sound + stabilité affine

Le module Utility/Representation.lean prouve la direction sound du théorème vNM : si u représente P, alors P satisfait chacun des quatre axiomes (les axiomes se réduisent à des faits élémentaires sur l’ordre et la structure affine de ℝ).

IsExpectedUtilityRep u P — u représente P : P p q ↔︎ E_p[u] ≥ E_q[u].
rep_complete / rep_transitive / rep_independent / rep_continuous — u représentée ⟹ chaque axiome.
expected_utility_rep_is_rational (flagship) — IsExpectedUtilityRep u P → IsRational P (direction sound).
affine_rep_is_rep — stabilité affine : a·u + b (a > 0) représente aussi P (unicité de l’utilité à transformation affine positive près).
rep_strict_iff / rep_indifference_iff / strict_irrefl — préférence stricte et indifférence sous une représentation.

#check IsExpectedUtilityRep
#check rep_complete
#check rep_independent
#check expected_utility_rep_is_rational
#check affine_rep_is_rep
#check rep_strict_iff

#check IsExpectedUtilityRep Utility.IsExpectedUtilityRep.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) : Prop

#check rep_complete Utility.rep_complete.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P) :
  Utility.IsComplete P

#check rep_independent Utility.rep_independent.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P) :
  IsIndependent P

#check expected_utility_rep_is_rational Utility.expected_utility_rep_is_rational.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α)
  (h : IsExpectedUtilityRep u P) : IsRational P

#check affine_rep_is_rep Utility.affine_rep_is_rep.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P)
  (a : ℝ) (ha : 0 < a) (b : ℝ) : IsExpectedUtilityRep (fun x => a * u x + b) P

#check rep_strict_iff Utility.rep_strict_iff.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P)
  (p q : Lottery α) : StrictPref P p q ↔ expectation p u > expectation q u

--% env 4

Raw input

{"cmd": "#check IsExpectedUtilityRep\n#check rep_complete\n#check rep_independent\n#check expected_utility_rep_is_rational\n#check affine_rep_is_rep\n#check rep_strict_iff", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Utility.IsExpectedUtilityRep.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) : Prop"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Utility.rep_complete.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P) :\n  Utility.IsComplete P"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Utility.rep_independent.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P) :\n  IsIndependent P"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Utility.expected_utility_rep_is_rational.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α)\n  (h : IsExpectedUtilityRep u P) : IsRational P"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Utility.affine_rep_is_rep.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P)\n  (a : ℝ) (ha : 0 < a) (b : ℝ) : IsExpectedUtilityRep (fun x => a * u x + b) P"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "Utility.rep_strict_iff.{u_1} {α : Type u_1} [Fintype α] (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P)\n  (p q : Lottery α) : StrictPref P p q ↔ expectation p u > expectation q u"}],
 "env": 4}

Lecture : la direction sound, prouvée entièrement

Théorème	Conclusion
`expected_utility_rep_is_rational`	représentation ⟹ rationalité (sound, flagship)
`affine_rep_is_rep`	`a·u + b` (`a>0`) représente aussi `P` (unicité affine)
`rep_strict_iff`	`p ≻ q ⟺ E_p[u] > E_q[u]`
`rep_indifference_iff`	`p ~ q ⟺ E_p[u] = E_q[u]`

Le jalon laissé ouvert (honnêtement)

La réciproque — toute préférence rationnelle admet une représentation en utilité espérée — est la moitié substantielle du théorème vNM (Herstein & Milnor, 1953). Elle exige un argument de séparation / algèbre linéaire non trivial, et est laissée comme jalon suivant, délibérément non sorry-backed : la lib reste entièrement sorry-free. Seules les différences d’utilité (pas les niveaux) sont identifiées par les données de choix — c’est l’unicité affine.

6. La chaîne causale complète

Les modules de la lib Utility composent une chaîne unique, des loteries à la rationalité :

Basic — Lottery/expectation/mix + expectation_mix/expectation_affine (l’algèbre affine de l’espérance).
Axioms — Pref/les 4 axiomes/IsRational (le cadre de la rationalité).
Representation — IsExpectedUtilityRep ⟶ les 4 axiomes sous représentation ⟶ flagship expected_utility_rep_is_rational + stabilité affine.

La chaîne se prolonge en amont côté probabilités — lib Coherence (Basic/DutchBook/Probability, Dutch Book à quatre tickets puis SingleCoherent q ↔︎ ProbBounds q) — traitée dans le companion dédié DecInfer-02b-Lean-Coherence.

7. Au-delà de l’utilité : pourquoi ces prix sont des probabilités (de Finetti)

Cette section — la thèse de de Finetti (1937) : un prix d’agent rationnel ne peut pas être arbitré, la cohérence force l’additivité donc la mesure de probabilité — et la suivante (caractérisation mono-livret SingleCoherent q ↔︎ ProbBounds q, quatre témoins explicites) ont déménagé dans le companion dédié DecInfer-02b-Lean-Coherence (extraction G4b, #14873) : elles forment un socle probabiliste autonome, distinct du théorème de représentation vNM qui reste le sujet de ce notebook.

8. Exemple guidé et exercices

Exercice 1 — Loteries, mélange et espérance (Python)

Ancrez l’intuition : une loterie = dictionnaire {issue: probabilité} sommant à 1. Implémentez expectation (utilité espérée) et mix (mélange convexe), puis vérifiez que l’espérance est affine sous le mélange.

def expectation(lottery, utility):
    # Esperance de la fonction d'utilite sous la loterie
    # lottery : {issue: prob}, utility : {issue: float}
    # TODO etudiant : somme des prob * utility
    return None  # TODO

def mix(t, lottery_p, lottery_r):
    # Mélange convexe t*p + (1-t)*r (t dans [0,1])
    # TODO etudiant : pour chaque issue, t*proba_p + (1-t)*proba_r
    return None  # TODO

Exercice 2 — Une préférence représentée est transitive (Lean)

Prouvez la transitivité d’une préférence représentée, sans utiliser rep_transitive. Indice : sous une représentation, P p q ⟺ E_p[u] ≥ E_q[u]. La transitivité suit de celle de ≥ sur ℝ (linarith avec les deux hypothèses décantées).

-- TODO etudiant : remplacer le sorry
-- example (u : α → ℝ) (P : Pref α) (h : IsExpectedUtilityRep u P)
--     (p q r : Lottery α) (hpq : P p q) (hqr : P q r) : P p r := by
--   sorry

Exercice 3 — Pourquoi l’utilité est unique à transformation affine près (Python)

Illustrez la stabilité affine (affine_rep_is_rep). Si u représente P, alors a·u + b (a > 0) représente aussi P : le classement des loteries par espérance est invariant. Implémentez la transformation et vérifiez que l’ordre des loteries est préservé (mais pas les valeurs absolues — d’où le fait que seules les différences d’utilité sont identifiées par les données de choix).

def affine_transform(u, a, b):
    # Transformee affine a*u + b (a > 0)
    # TODO etudiant : retourner {issue: a*val + b}
    return None  # TODO

def preserves_order(lottery_p, lottery_q, u, a, b):
    # Si E_p[u] >= E_q[u] alors E_p[a*u+b] >= E_q[a*u+b] ?
    # TODO etudiant : verifier la preservation de l'ordre (a > 0)
    return None  # TODO

Conclusion

Ce companion natif exhibe la preuve formelle sans sorry de la direction sound du théorème de représentation d’utilité espérée de von Neumann–Morgenstern dans le kernel Lean lui-même : #check et #print axioms rendent les signatures et les axiomes réels produits par le compilateur, sans intermédiaire Python.

Le résultat phare expected_utility_rep_is_rational fonde le classement par espérance d’utilité : toute préférence qu’une utilité représente est rationnelle. Combinée à la stabilité affine (affine_rep_is_rep), c’est la justification formelle de pourquoi DecInfer-01 et PyMC-1 rangent les décisions par espérance d’utilité, et pourquoi seules les différences d’utilité (et non les niveaux) sont identifiées.

La lib Coherence étend le socle en amont — de Finetti (1937) côté probabilités, exactement comme vNM côté utilité — : voir DecInfer-02b-Lean-Coherence.

Jalon ouvert : la réciproque (existence d’une représentation pour toute préférence rationnelle, Herstein–Milnor 1953) n’est pas formalisée ; la lib reste sorry-free.

Retour au sommet

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

1. Import des modules Utility du lake decision_theory_lean

2. Preuve sans sorry — #print axioms

3. Loteries, espérance et mélange convexe

Lecture : l’algèbre de l’espérance

4. Les quatre axiomes de rationalité de von Neumann–Morgenstern

Lecture : les quatre piliers de la rationalité

5. Le théorème de représentation : direction sound + stabilité affine

Lecture : la direction sound, prouvée entièrement

Le jalon laissé ouvert (honnêtement)

6. La chaîne causale complète

7. Au-delà de l’utilité : pourquoi ces prix sont des probabilités (de Finetti)

8. Exemple guidé et exercices

Exercice 1 — Loteries, mélange et espérance (Python)

Exercice 2 — Une préférence représentée est transitive (Lean)

Exercice 3 — Pourquoi l’utilité est unique à transformation affine près (Python)

Conclusion

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

1. Import des modules `Utility` du lake `decision_theory_lean`

2. Preuve sans `sorry` — `#print axioms`