Mixed strategies on the standard simplex

This file equips standardSimplex 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.

def Brouwer.standardSimplex (k : Type u_1) (α : Type u_2) [Semiring k] [PartialOrder k] [Fintype α] : Set (α → k)

The standard simplex as a set of coordinate functions. Keeping this representation gives its points the subspace topology of the finite product used in the fixed-point proof.

Equations

• Brouwer.standardSimplex k α = {f : α → k | (∀ (i : α), 0 ≤ f i) ∧ ∑ i : α, f i = 1}

theorem Brouwer.isCompact_standardSimplex (α : Type u_1) [Fintype α] : IsCompact (standardSimplex ℝ α)

The real standard simplex is a closed subset of the unit cube.

instance Brouwer.instCompactSpaceElemForallRealStandardSimplex (α : Type u_1) [Fintype α] : CompactSpace ↑(standardSimplex ℝ α)

@[instance_reducible]

instance stdSimplex.funlike (k : Type u_2) [CommRing k] [LinearOrder k] (α : Type u_3) [Fintype α] : FunLike (↑(Brouwer.standardSimplex 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 : ↑(Brouwer.standardSimplex k α)) : ⇑f = ↑f

theorem stdSimplex.funlike_eval2 (k : Type u_2) [CommRing k] [LinearOrder k] (α : Type u_3) [Fintype α] (f : ↑(Brouwer.standardSimplex 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 : α) : ↑(Brouwer.standardSimplex 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

@[instance_reducible]

noncomputable instance stdSimplex.SInhabitedOfInhabited (k : Type u_2) [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] (α : Type u_3) [Fintype α] [DecidableEq α] [Inhabited α] : Inhabited ↑(Brouwer.standardSimplex 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 ↑(Brouwer.standardSimplex k α)

theorem stdSimplex.wsum_magic_ineq {k : Type u_2} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] {α : Type u_3} [Fintype α] [PosMulMono k] {σ : ↑(Brouwer.standardSimplex 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 α = Brouwer.standardSimplex ℝ α