Definition Field-Generic Value Predicates
✓ definition formalized

Field-Generic Value Predicates

For a finite matrix game $A : I \times J \to \mathbb{K}$ with payoff in any linearly ordered field $\mathbb{K}$, the maxmin / minmax / saddle-value notions admit the following predicate characterisations that do not invoke any sSup / sInf:

Maximin (predicate form). $v$ is a maximin value of $A$ when

$$ \bigl(\exists x \in \Delta(I),\ \forall j \in J,\ v \le \sum_i x_i\, A(i,j)\bigr) \quad\text{and}\quad \bigl(\forall w,\ (\exists x \in \Delta(I),\ \forall j,\ w \le \sum_i x_i\, A(i,j)) \Rightarrow w \le v\bigr). $$

That is: some row strategy guarantees at least $v$ against every column (existence), and no strictly larger value is achievable (maximality).

Minimax (predicate form). Dual: $v$ is a minimax value when some column strategy caps player I's payoff at $v$, and no strictly smaller cap is achievable.

Value (saddle-point form). $v$ is the value of $A$ when there are row and column strategies $x, y$ with

$$ \forall j,\ v \le \sum_i x_i\, A(i,j) \qquad\text{and}\qquad \forall i,\ \sum_j y_j\, A(i,j) \le v. $$

The saddle-point form is the existential combination of the two one-sided guarantee statements; it is equivalent to "value exists and equals $v$" without invoking $\sup$ / $\inf$.

Relationship to sSup-based definitions

When $\mathbb{K}$ admits order completeness (e.g. $\mathbb{K} = \mathbb{R}$ via Real.instConditionallyCompleteLinearOrder), the sSup-based Maximin and Minimax Values definitions are available, and:

  • IsMaximin A v ↔ v = A.maximin (assuming the supremum is attained),
  • IsMinimax A v ↔ v = A.minimax,
  • IsValue A v is equivalent to the conjunction of the above when the minimax theorem (Von Neumann Minimax Theorem) holds.

The Lean library realises IsMaximin, IsMinimax, IsValue in EconCSLib.StrategicGame.Minimax. The bridge lemmas between the predicate and sSup forms are tracked as Phase 2 follow-up of #54.

Why this matters

An ordered-field-generic value route constructs the value as a witness over any linearly ordered field, not as a supremum, so it is naturally phrased via IsValue rather than via value. The symmetrisation route Minimax.minimax (Ordered-Field Minimax Statement) is exactly this: it delivers the optimal value and strategies over any [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] without requiring order completeness, so the predicate forms are the natural interface for it.

References

  • [MFoGT, Chapter 2, Section 2.2] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Saddle-point characterisation of value.

Also in