EconCSLib.Foundation.Profile

Compatibility shim for the older standalone Profile N S vocabulary.

The canonical profile abstraction for strategic games is now G.Profile in StrategicGame.Basic, together with StrategicGame.deviate.

This file remains only to minimize breakage while Stage 2 is in progress. It should not be treated as the primary public interface.

@[reducible, inline]

abbrev Profile (N : Type u_1) (S : N → Type u_2) : Type (max u_1 u_2)

A strategy profile: a dependent function assigning a value to each index.

Compatibility alias only. Prefer game-bound profile aliases such as G.Profile.

Equations

• Profile N S = ((i : N) → S i)

@[reducible, inline]

abbrev deviate {N : Type u_1} {S : N → Type u_2} [DecidableEq N] (σ : Profile N S) (i : N) (s' : S i) : Profile N S

Unilateral deviation: index i switches to s', all others keep their value. This is Function.update with a game-theoretic name.

Equations

• deviate σ i s' = Function.update σ i s'

def Profile.«term_[_↦_]» : Lean.TrailingParserDescr

σ[i ↦ s'] is the profile where index i holds s' and all others are as in σ.

Scoped to keep the postfix […] bracket from clashing with list literals (… []) in importing files; open scoped Profile to use it.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Profile.deviate_self {N : Type u_1} {S : N → Type u_2} [DecidableEq N] (σ : Profile N S) (i : N) : deviate σ i (σ i) = σ

Deviating to the same value is the identity.

@[simp]

theorem Profile.deviate_same {N : Type u_1} {S : N → Type u_2} [DecidableEq N] (σ : Profile N S) (i : N) (s' : S i) : deviate σ i s' i = s'

At the deviated index, the profile returns the new value.

@[simp]

theorem Profile.deviate_of_ne {N : Type u_1} {S : N → Type u_2} [DecidableEq N] (σ : Profile N S) (i : N) (s' : S i) {j : N} (h : j ≠ i) : deviate σ i s' j = σ j

At any other index, the profile is unchanged.