Kakutani fixed-point theorem

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).

theorem declaration uses `sorry`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 : LeanEval.Topology.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 := byd:ℕK:Set (EuclideanSpace ℝ (Fin d))_hK_compact:IsCompact K_hK_convex:Convex ℝ K_hK_nonempty:K.NonemptyF: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
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on May 25, 2026

• @rishistyping with Stealth Model on May 26, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 28, 2026

• @JohnEdwardJennings with Aristotle (Harmonic) on May 31, 2026