Lean declarations

theorem stdSimplex.continuous_coord EconCSLib @ cef01c7, EconCSLib.Math.Simplex
The `i`-th coordinate projection on `stdSimplex ℝ I` is continuous.
```
theorem stdSimplex.continuous_coord (i : I) :
    Continuous fun x : stdSimplex ℝ I => x.val i
```
theorem wsum_continuous EconCSLib @ cef01c7, EconCSLib.Math.Simplex
`wsum (·) f` is continuous on the standard simplex over ℝ.
```
theorem wsum_continuous (f : I → ℝ) :
    Continuous fun x : stdSimplex ℝ I => wsum x f
```

Modules: EconCSLib.Math.Simplex

Continuity on the Real Standard Simplex

Specialized to the field $\mathbb{R}$, the standard simplex carries the subspace topology from $\mathbb{R}^I$, and two basic continuity facts are needed by every existence-via-compactness argument:

stdSimplex.continuous_coord i -- the i-th coordinate projection $x \mapsto x_i$ is continuous on stdSimplex ℝ I.
wsum_continuous f -- for any f : I → ℝ, the map $x \mapsto \operatorname{wsum} x\, f$ is continuous on stdSimplex ℝ I.

Combined with Mathlib's compactness of the real standard simplex (stdSimplex.instCompactSpace_coe), these continuity facts deliver the existence of optimal mixed strategies via the extreme-value theorem. This is the analytic ingredient of the Loomis route to the minimax theorem and of Brouwer-based proofs of Nash existence.

References

[MSZ, Chapter 5] Maschler, Solan, and Zamir, Game Theory. Continuity of the expected payoff in the mixed-strategy profile.

Continuity on the Real Standard Simplex

References

Used by

Also in