Lescanne , Deconstruction of Infinite Extensive Games Using Coinduction

Equilibria for infinite games using coinduction.

• what is the Weierstrass function?

a counterexample of the fact that a finite sum of functions differentiable everywhere is differentiable everywhere whereas an infinite sum can be differentiable nowhere.

He's representing strategies as the whole game plus "which way to go from here?".

Coinductive definitions (for extensional games):

Game := Payoff | Agent Game Game Strategy := Payoff | Left | Right

Predicates:

s2u s:Strategy a:Agent u:Utility : Pred := cases s of

f: Payoff : s2u s a f(a)

Left : s2u sl a u => s2u u

Right : s2u sr a u => s2u u

leads to a leaf

lleaf s: Strategy := cases s of

f: Payoff : true

Left : lleaf sl => lleaf

Right : lleaf sr => lleaf

alleaf s: Strategy := cases s of

f: Payoff : true

: lleaf and alleaf sl and alleaf sr

convertibility (all the strategies where all players but one are held constant):

convertible a s1 s2: Strategy :=

leaves are equal if they are equal

head(s1) = head(s2) = a : equal with any switched choice and convertible children

head(s1) = head(s2) ! a : only equal with same choice and convertible children

Nash eqbr:

(lleaf s) and (forall a: Agent s' : Strategy, (lleaf s') and (convertible a s s') , (forall u u' : Payoff, (s2u s a u) and (s2u s' a u'), u ≥ u' )).

Subgame perfect eqbr:

SGPE :=

Payoff : true

Left: alleaf Left and SGPE s and SGPE sr and forall u, v, (s2u sl a u and s2u sr a v) -> u >= v

Right: alleaf Right and SGPE s and SGPE sr and forall u, v, (s2u sl a u and s2u sr a v) -> u <= v