EconCSLib.Math.FixedPoint.KKM

The Knaster–Kuratowski–Mazurkiewicz (KKM) fixed-point lemma and its variants.

The KKM lemma is a fundamental result in combinatorial topology with broad applications in game theory, economics, and fair division. The open-cover variant stated here is the topological engine of Stromquist's proof of envy-free existence (Stromquist, "How to Cut a Cake Fairly", Amer. Math. Monthly 87, 1980, pp. 640–644).

Setup

We work with the standard (n-1)-simplex

  stdSimplex ℝ (Fin n) = { x : Fin n → ℝ | 0 ≤ xᵢ for all i, ∑ xᵢ = 1 }

inside Fin n → ℝ with the subspace topology. The face opposite vertex i is

  simplexFaceOpp i = { x ∈ stdSimplex ℝ (Fin n) | xᵢ = 0 }

the sub-face where coordinate i is zero. In Stromquist's notation, simplexFaceOpp i is the face Sᵢ where the i-th piece of cake is empty.

Main results

• kkm_closed_cover — classical KKM: if the simplex is covered by n closed sets satisfying the KKM combinatorial condition, their common intersection is nonempty.

• kkm_open_cover — open-cover variant (Stromquist 1980, p.642): if the simplex is covered by n open sets U₀, …, Uₙ₋₁ with Uᵢ ∩ simplexFaceOpp i = ∅, then ⋂ᵢ Uᵢ is nonempty.

Proof strategy

kkm_closed_cover is proved via Brouwer's fixed-point theorem (EconCSLib.Math.FixedPoint.Brouwer): assuming no common intersection point exists, construct a continuous self-map of the simplex that pushes each point away from the closed sets it misses (using Metric.infDist), apply Brouwer to get a fixed point, and derive a contradiction via the KKM combinatorial condition.

kkm_open_cover reduces to kkm_closed_cover via a partition of unity argument: obtain continuous functions φ i : C(Fin n → ℝ, ℝ) subordinate to U i (via exists_continuous_sum_one_of_isOpen_isCompact) with tsupport (φ i) ⊆ U i and ∑ i, φ i = 1 on the simplex. Define F j = stdSimplex ∩ {x | ∀ k, φ k x ≤ φ j x}. Each F j is closed; the KKM condition holds because for x ∈ face(σ) the face- avoidance hypothesis forces φ k x = 0 for k ∉ σ, so some j ∈ σ attains the max. Applying kkm_closed_cover yields x with φ j x = 1/n > 0 for every j, hence x ∈ tsupport (φ j) ⊆ U j.

References

• Knaster, Kuratowski, Mazurkiewicz, "Ein Beweis des Fixpunktsatzes für n-dimensionale Simplexe", Fund. Math. 14 (1929), pp. 132–137.
• Stromquist, "How to Cut a Cake Fairly", Amer. Math. Monthly 87 (1980), pp. 640–644.
• Su, "Rental Harmony: Sperner's Lemma in Fair Division", Amer. Math. Monthly 106 (1999).

Faces of the standard simplex

def simplexFaceOpp {n : ℕ} (i : Fin n) : Set (Fin n → ℝ)

The face of the standard simplex opposite vertex i: the set of simplex points whose i-th coordinate is zero.

In cake-cutting language (Stromquist 1980): simplexFaceOpp i is the face Sᵢ consisting of all divisions where the i-th piece has measure zero (is "empty"). The KKM open-cover condition requires Uᵢ ∩ simplexFaceOpp i = ∅ — no division in Uᵢ has an empty i-th piece.

Equations

• simplexFaceOpp i = {x : Fin n → ℝ | x i = 0} ∩ stdSimplex ℝ (Fin n)

KKM combinatorial condition

def IsKKMCover {n : ℕ} (F : Fin n → Set (Fin n → ℝ)) : Prop

The KKM condition for a cover F : Fin n → Set _ of the standard simplex: for each subset σ ⊆ Fin n, the face of the simplex supported on σ (points with zero weight outside σ) is covered by ⋃_{i ∈ σ} F i.

This is the combinatorial heart of the KKM lemma: each face is covered by the subfamily indexed by that face's vertices.

Equations

• IsKKMCover F = ∀ (σ : Finset (Fin n)), stdSimplex ℝ (Fin n) ∩ {x : Fin n → ℝ | ∀ i ∉ σ, x i = 0} ⊆ ⋃ i ∈ σ, F i

Classical KKM lemma

theorem kkm_closed_cover {n : ℕ} (hn : 0 < n) (F : Fin n → Set (Fin n → ℝ)) (hclosed : ∀ (i : Fin n), IsClosed (F i)) (hkkm : IsKKMCover F) : ∃ x ∈ stdSimplex ℝ (Fin n), ∀ (i : Fin n), x ∈ F i

Knaster–Kuratowski–Mazurkiewicz lemma (closed-cover version).

If the standard (n-1)-simplex stdSimplex ℝ (Fin n) is covered by n closed sets F 0, …, F (n-1) satisfying the KKM combinatorial condition (IsKKMCover F), then their common intersection with the simplex is nonempty.

Proof: By contradiction using Brouwer's fixed-point theorem. Assuming no common intersection, define g(x)(j) = (x j + infDist x (F j)) / (1 + D(x)) where D(x) = ∑ j, infDist x (F j) > 0. Then g is a continuous self-map of the simplex with no fixed point (the fixed-point equation forces D(x₀) = 0 via the KKM condition), contradicting Brouwer.

Open-cover variant (Stromquist's lemma)

theorem kkm_open_cover {n : ℕ} (hn : 0 < n) (U : Fin n → Set (Fin n → ℝ)) (hopen : ∀ (i : Fin n), IsOpen (U i)) (hface : ∀ (i : Fin n), simplexFaceOpp i ⊆ (U i)ᶜ) (hcover : stdSimplex ℝ (Fin n) ⊆ ⋃ (i : Fin n), U i) : ∃ x ∈ stdSimplex ℝ (Fin n), ∀ (i : Fin n), x ∈ U i

KKM lemma — open-cover variant (Stromquist 1980, p.642).

If the standard (n-1)-simplex is covered by n open sets U 0, …, U (n-1) such that no U i intersects the face simplexFaceOpp i (where coordinate i is zero), then some point of the simplex lies in every U i.

This is the topological engine of Stromquist's EF existence proof: the U i are the "unique preference" unions (sets of divisions where some player uniquely prefers piece i), and the point in ⋂ᵢ Uᵢ is the fair division.

Proof: Reduce to kkm_closed_cover via a partition of unity. Obtain φ i : C(Fin n → ℝ, ℝ) with tsupport (φ i) ⊆ U i and ∑ i, φ i = 1 on the simplex (using exists_continuous_sum_one_of_isOpen_isCompact). Set F j = stdSimplex ∩ {x | ∀ k, φ k x ≤ φ j x} (closed). For x ∈ face(σ): φ k x = 0 for k ∉ σ (by face-avoidance), so the max is attained by some j ∈ σ, giving x ∈ F j. Hence IsKKMCover F holds. The fixed point x from kkm_closed_cover satisfies φ j x = 1/n > 0 for all j, so x ∈ support (φ j) ⊆ tsupport (φ j) ⊆ U j.