Ce notebook est le companion formel du lake decision_theory_lean (lib Coherence), qui prouve la cohérence de de Finetti : un système de prix arbitrage-incohérent est exploitable par un Dutch Book — un panier de paris au gain négatif dans tous les états du monde — et, dans le cadre mono-livret, la cohérence coïncide exactement avec les bornes de probabilité (SingleCoherent q ↔︎ ProbBounds q), avec zéro sorry.
Il est extrait des sections 7-8 d’origine de DecInfer-02 (extraction G4b, #14873 — la base les remplace par un renvoi et renumérote sa suite) : le théorème de représentation vNM justifie de ranger par espérance d’utilité ; la cohérence de de Finetti justifie que l’espérance elle-même — la mesure de probabilité sous-jacente — est la seule non-exploitable.
#check natif dans le kernel LeanCe 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.
Coherence du lake decision_theory_leanimport Coherence.DutchBook
import Coherence.Probability
open Coherence
import Coherence.DutchBook
import Coherence.Probability
open Coherence
--% env 0
{"cmd": "import Coherence.DutchBook\nimport Coherence.Probability\nopen Coherence\n"}
{"env": 0}
Le théorème vNM justifie de ranger par espérance d’utilité. Mais sur quoi repose l’espérance elle-même ? Le lake répond dans sa lib Coherence (modules de l’EPIC #11703, extraits ici de DecInfer-02) : la thèse de de Finetti (1937) — un prix d’agent rationnel sur des événements ne peut pas être arbitré. Si vos prix violent l’additivité (q(A) + q(B) ≠ q(A∩B) + q(A∪B)), un adversaire construit un Dutch Book : un panier de paris dont le gain est négatif dans tous les états du monde — une perte sûre. La cohérence force l’additivité, donc la mesure de probabilité.
#print axioms non_additive_implies_dutch_book
#print axioms coherent_on_implies_additive 'Coherence.non_additive_implies_dutch_book' depends on axioms: [propext, Classical.choice, Quot.sound]
'Coherence.coherent_on_implies_additive' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 1
{"cmd": "#print axioms non_additive_implies_dutch_book\n#print axioms coherent_on_implies_additive", "env": 0}
{"messages":
[{"severity": "info",
"pos": {"line": 1, "column": 0},
"endPos": {"line": 1, "column": 6},
"data":
"'Coherence.non_additive_implies_dutch_book' depends on axioms: [propext, Classical.choice, Quot.sound]"},
{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data":
"'Coherence.coherent_on_implies_additive' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
"env": 1}
non_additive_implies_dutch_book : si q A + q B ≠ q (A∩B) + q (A∪B), il existe des mises (sA, sB, sAB, sAU) sur les quatre tickets A, B, A∩B, A∪B dont le gain ieGain est strictement négatif en tout état (IsIEArbitrage). Le témoin est explicite : l’identité d’inclusion-exclusion des indicatrices 𝟙_A + 𝟙_B − 𝟙_{A∩B} − 𝟙_{A∪B} = 0 rend le gain indépendant de l’état, égal à δ := q(A∪B) + q(A∩B) − q(A) − q(B) — le signe des mises se choisit contre δ.coherent_on_implies_additive : la contraposée — pas d’arbitrage (CoherentOn) ⟹ additivité sur la paire (A, B).#print axioms ne liste que les axiomes standard de Mathlib : aucun sorryAx.C’est exactement le pendant probabiliste de la section 5 de DecInfer-02 : là, la représentation forçait la rationalité ; ici, la non-exploitabilité force la mesure.
Le module Coherence.Probability pousse la correspondance jusqu’à une caractérisation si et seulement si, dans le cadre fini mono-livret : une fonction de prix q est exploitable par un Dutch Book à un seul ticket si et seulement si elle viole une borne de probabilité. Chaque borne violée vient avec son témoin explicite — pas d’argument abstrait de séparation :
#check ticketGain
#check SingleCoherent
#check ProbBounds
#check single_coherent_iff_prob_bounds
#print axioms single_coherent_iff_prob_bounds Coherence.ticketGain.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) (A : Event Ω) (s : ℝ) (ω : Ω) : ℝ
Coherence.SingleCoherent.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) : Prop
Coherence.ProbBounds.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) : Prop
Coherence.single_coherent_iff_prob_bounds.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) [Nonempty Ω] :
SingleCoherent q ↔ ProbBounds q
'Coherence.single_coherent_iff_prob_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 2
{"cmd": "#check ticketGain\n#check SingleCoherent\n#check ProbBounds\n#check single_coherent_iff_prob_bounds\n#print axioms single_coherent_iff_prob_bounds", "env": 1}
{"messages":
[{"severity": "info",
"pos": {"line": 1, "column": 0},
"endPos": {"line": 1, "column": 6},
"data":
"Coherence.ticketGain.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) (A : Event Ω) (s : ℝ) (ω : Ω) : ℝ"},
{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data":
"Coherence.SingleCoherent.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) : Prop"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"Coherence.ProbBounds.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) : Prop"},
{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data":
"Coherence.single_coherent_iff_prob_bounds.{u_1} {Ω : Type u_1} [Fintype Ω] [DecidableEq Ω] (q : Price Ω) [Nonempty Ω] :\n SingleCoherent q ↔ ProbBounds q"},
{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 6},
"data":
"'Coherence.single_coherent_iff_prob_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
"env": 2}
single_coherent_iff_prob_bounds : SingleCoherent q ↔︎ ProbBounds q (non-négativité, majoration par 1, q ∅ = 0, q univ = 1), 0 sorry. Chaque direction de violation a son witness d’une ligne dans le module :
| Borne violée | Mise s |
Gain en tout état |
|---|---|---|
q A < 0 |
vendre (s = −1) |
q A − 𝟙_A ≤ q A < 0 |
q A > 1 |
acheter (s = +1) |
𝟙_A − q A < 0 (car 𝟙_A ≤ 1) |
q univ < 1 |
s = −1 sur l’univers |
q univ − 1 < 0 |
q ∅ > 0 |
s = +1 sur le vide |
−q ∅ < 0 (car 𝟙_∅ = 0) |
La réciproque vient de priceFromWeights_coherent_on : les prix issus de poids q A = Σ_{ω ∈ A} p(ω) sont cohérents, par l’argument d’espérance E_p[gain] = 0 (expected_ticket_gain_zero) — l’agent adverse ne peut pas gagner en moyenne sous la mesure qu’il vous fait payer. Le coherent_iff_probability complet (livrets de taille arbitraire, reconstruction q A = Σ_{ω∈A} q {ω}) reste un jalon ouvert du lake, documenté dans le module — le même honnête « une direction prouvée + réciproque ouverte » que la lib Utility de DecInfer-02 (sound prouvé, Herstein–Milnor ouvert).
Ce companion expose la cohérence de de Finetti (1937) telle que prouvée dans la lib Coherence du lake decision_theory_lean : un système de prix arbitrage-incohérent est exploitable par un Dutch Book à quatre tickets (non_additive_implies_dutch_book, witness constructif), et dans le cadre mono-livret la cohérence coïncide exactement avec les bornes de probabilité (single_coherent_iff_prob_bounds, quatre témoins explicites). 0 sorry — #print axioms ne liste que les axiomes standard de Mathlib.
Avec le théorème de représentation vNM de DecInfer-02, la boucle est fermée des deux côtés : vNM justifie de ranger par espérance d’utilité, de Finetti justifie que l’espérance elle-même — la mesure sous-jacente — est la seule non-exploitable. Le jalon ouvert (coherent_iff_probability en taille arbitraire) reste documenté dans le module.