Mixed strategies on the standard simplex

This file equips stdSimplex over a finite type with a FunLike coercion and records the basic arithmetic facts about pure strategies and weighted sums used when reasoning about mixed strategies, including the key inequality wsum_magic_ineq relating a weighted sum to a uniform bound.

@[implicit_reducible]

instance stdSimplex.funlike (k : Type u_2) [CommRing k] [LinearOrder k] (α : Type u_3) [Fintype α] : FunLike (↑(stdSimplex k α)) α k

Equations

• stdSimplex.funlike k α = { coe := Subtype.val, coe_injective := ⋯ }

theorem stdSimplex.funlike_eval1 (k : Type u_2) [CommRing k] [LinearOrder k] (α : Type u_3) [Fintype α] (f : ↑(stdSimplex k α)) : ⇑f = ↑f

theorem stdSimplex.funlike_eval2 (k : Type u_2) [CommRing k] [LinearOrder k] (α : Type u_3) [Fintype α] (f : ↑(stdSimplex k α)) (x : α) : ↑f x = f x

@[reducible, inline]

abbrev stdSimplex.pure {k : Type u_2} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {α : Type u_3} [Fintype α] [DecidableEq α] (i : α) : ↑(stdSimplex k α)

The pure strategy concentrated at i, as a point of the standard simplex.

Equations

• stdSimplex.pure i = ⟨fun (j : α) => if i = j then 1 else 0, ⋯⟩

theorem stdSimplex.pure_eval_eq {k : Type u_2} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {α : Type u_3} [Fintype α] [DecidableEq α] {i j : α} (h : i = j) : (pure i) j = 1

theorem stdSimplex.pure_eval_neq {k : Type u_2} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {α : Type u_3} [Fintype α] [DecidableEq α] {i j : α} (h : ¬i = j) : (pure i) j = 0

@[implicit_reducible]

noncomputable instance stdSimplex.SInhabitedOfInhabited (k : Type u_2) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] (α : Type u_3) [Fintype α] [DecidableEq α] [Inhabited α] : Inhabited ↑(stdSimplex k α)

Equations

• stdSimplex.SInhabitedOfInhabited k α = { default := stdSimplex.pure default }

instance stdSimplex.SNonempty_of_Inhabited (k : Type u_2) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {α : Type u_4} [Fintype α] [Inhabited α] : Nonempty ↑(stdSimplex k α)

theorem stdSimplex.wsum_magic_ineq {k : Type u_2} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {α : Type u_3} [Fintype α] [PosMulMono k] {σ : ↑(stdSimplex k α)} {f : α → k} {c : k} : ∑ i : α, σ i * f i = c → ∃ (i : α), 0 < σ i ∧ f i ≤ c

@[reducible, inline]

abbrev MixedStrategy (α : Type u_1) [Fintype α] : Set (α → ℝ)

The standard simplex over α with real coefficients, used as mixed strategies.

Equations

• MixedStrategy α = stdSimplex ℝ α