Lean declarations

def stdSimplex.pure EconCSLib @ cef01c7, EconCSLib.Math.Simplex

Point-mass simplex element at `i₀`.

def stdSimplex.pure [DecidableEq I] (i₀ : I) : stdSimplex 𝕜 I where
  val i := if i = i₀ then 1 else 0
  property := ⟨fun i => by simp only; split_ifs <;> norm_num,
               by simp [Finset.sum_ite_eq', Finset.mem_univ]⟩

theorem stdSimplex.pure_apply EconCSLib @ cef01c7, EconCSLib.Math.Simplex

theorem stdSimplex.pure_apply [DecidableEq I] (i₀ i : I) :
    (stdSimplex.pure (𝕜 := 𝕜) i₀).val i = if i = i₀ then 1 else 0

theorem wsum_pure_apply EconCSLib @ cef01c7, EconCSLib.Math.Simplex

theorem wsum_pure_apply [DecidableEq I] (i₀ : I) (f : I → 𝕜) :
    wsum (stdSimplex.pure (𝕜 := 𝕜) i₀) f = f i₀

theorem wsum_pure EconCSLib @ cef01c7, EconCSLib.Math.Simplex

theorem wsum_pure [DecidableEq I] (i₀ : I) (f : I → 𝕜) :
    wsum ⟨fun i => if i = i₀ then 1 else 0,
          fun i => by simp only; split_ifs <;> norm_num,
          by simp [Finset.sum_ite_eq', Finset.mem_univ]⟩ f = f i₀

Modules: EconCSLib.Math.Simplex

Point Mass on the Standard Simplex

For a finite index I with decidable equality and a chosen vertex i₀ ∈ I, the point mass stdSimplex.pure i₀ is the simplex element that puts unit weight on i₀: $$ (\operatorname{pure} i_0)_i \;=\; \begin{cases} 1 & i = i_0,\\ 0 & i \ne i_0. \end{cases} $$

The two key facts:

stdSimplex.pure_apply -- the coordinate formula above (rfl-true).
wsum_pure_apply -- weighted-sum collapse: $\operatorname{wsum}\,(\operatorname{pure} i_0)\, f \;=\; f(i_0)$.

A legacy version wsum_pure is also exposed for code that builds the point mass inline as an anonymous-structure simplex element; new code should prefer stdSimplex.pure together with wsum_pure_apply.

The point mass is the bridge between pure and mixed strategies: it embeds any pure action into the mixed-strategy simplex without disturbing its weighted-sum semantics. This embedding is what justifies "pure strategies are a special case of mixed strategies".

References

[MSZ, Chapter 5] Maschler, Solan, and Zamir, Game Theory. Pure strategies as Dirac mixed strategies.

Used by

Pointwise Bounds Are Simplex Bounds

Point Mass on the Standard Simplex

References

Used by

Also in