feat: add Kakutani fixed-point theorem eval problem

LeanEval/Topology/Kakutani.lean

@@ -0,0 +1,49 @@
+import Mathlib
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+/-!
+# Kakutani fixed-point theorem
+
+§33 of Oliver Knill's *Some Fundamental Theorems in Mathematics* (an
+additional statement in the section on game theory; Nash's 1951 proof of
+equilibrium existence uses Kakutani directly). The set-valued
+generalization of Brouwer: every upper-hemicontinuous correspondence from
+a nonempty compact convex `K ⊆ ℝᵈ` to itself with nonempty convex closed
+values has a fixed point `x ∈ F x`.
+
+mathlib has Brouwer-related lattices/logics under `grep -ri kakutani` only
+the Riesz–Markov–Kakutani representation theorem for positive functionals
+— a different theorem entirely. The fixed-point theorem itself is not in
+mathlib.
+-/
+
+/-- A correspondence `F : α → Set β` is **upper hemicontinuous** in the
+closed-graph sense if its graph `{(x, y) | y ∈ F x}` is closed in `α × β`.
+For closed-valued maps into a compact space this coincides with the
+sequential/topological definition. -/
+def IsUpperHemicontinuous {α β : Type*}
+    [TopologicalSpace α] [TopologicalSpace β] (F : α → Set β) : Prop :=
+  IsClosed {p : α × β | p.2 ∈ F p.1}
+
+/-- **Kakutani fixed-point theorem.** Every upper-hemicontinuous
+correspondence `F` from a nonempty compact convex `K ⊆ ℝᵈ` to itself, with
+nonempty convex closed values, has a fixed point `x ∈ F x`. -/
+@[eval_problem]
+theorem kakutani_fixed_point {d : ℕ}
+    {K : Set (EuclideanSpace ℝ (Fin d))}
+    (_hK_compact : IsCompact K) (_hK_convex : Convex ℝ K)
+    (_hK_nonempty : K.Nonempty)
+    (F : EuclideanSpace ℝ (Fin d) → Set (EuclideanSpace ℝ (Fin d)))
+    (_hF_uhc : IsUpperHemicontinuous F)
+    (_hF_nonempty : ∀ x ∈ K, (F x).Nonempty)
+    (_hF_convex : ∀ x ∈ K, Convex ℝ (F x))
+    (_hF_closed : ∀ x ∈ K, IsClosed (F x))
+    (_hF_maps : ∀ x ∈ K, F x ⊆ K) :
+    ∃ x ∈ K, x ∈ F x := by
+  sorry
+
+end Topology
+end LeanEval

manifests/problems.toml

@@ -673,3 +673,14 @@ module = "LeanEval.Geometry.Uniformization"
 holes = ["uniformization"]
 submitter = "Junyan Xu"
 source = "John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1."
+
+[[problem]]
+id = "kakutani_fixed_point"
+title = "Kakutani fixed-point theorem"
+test = false
+module = "LeanEval.Topology.Kakutani"
+holes = ["kakutani_fixed_point"]
+submitter = "Kim Morrison"
+notes = "§33 of Oliver Knill's 'Some Fundamental Theorems in Mathematics' (additional statement of the game-theory section; underlies Nash's 1951 equilibrium-existence proof). The set-valued generalization of Brouwer: every upper-hemicontinuous correspondence F from a nonempty compact convex K ⊆ ℝᵈ to itself with nonempty convex closed values has a fixed point x ∈ F x. Mathlib's `grep -ri kakutani` returns only the Riesz-Markov-Kakutani representation theorem (a different theorem); the fixed-point theorem itself is not in mathlib."
+source = "S. Kakutani, A generalization of Brouwer's fixed point theorem, Duke Math. J. 8 (1941), 457-459. Listed as an additional statement of §33 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
+informal_solution = "Reduce to Brouwer by an approximation argument. Cover K by ε-balls and pick a finite subcover; on each ball define f_ε(x) := average of some selection from F(x) over the cover, producing a continuous single-valued ε-approximation f_ε : K → K. Apply Brouwer to f_ε to get a fixed point x_ε with x_ε ∈ F(x_ε) up to ε-error in the closed-graph sense. Take ε → 0 along a convergent subsequence (K compact); the limit point x is in the graph of F by upper hemicontinuity (closed graph), so x ∈ F(x)."