Lean declarations

def SocialChoice.FairDivision.Divisible.strom_A EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Existence

private def strom_A (i j : Fin n) : Set (Fin n → ℝ) :=
  {x : Fin n → ℝ | ∀ k : Fin n, strom_value n μ x j k ≤ strom_value n μ x j i}

lemma SocialChoice.FairDivision.Divisible.strom_A_closed EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Existence
```
private lemma strom_A_closed (i j : Fin n) : IsClosed (strom_A n μ i j)
```
lemma SocialChoice.FairDivision.Divisible.strom_A_covers EconCSLib @ cef01c7, EconCSLib.SocialChoice.FairDivision.Divisible.Existence
```
private lemma strom_A_covers (j : Fin n) :
    stdSimplex ℝ (Fin n) ⊆ ⋃ i, strom_A n μ i j
```

Modules: EconCSLib.SocialChoice.FairDivision.Divisible.Existence

Stromquist Preference Sets A(i, j)

For each agent $j \in \mathrm{Fin}\ n$ and piece index $i \in \mathrm{Fin}\ n$, the preference set $A(i, j)$ is the set of simplex points where piece $i$ is a value-maximizer for agent $j$: $$ A(i, j) \;=\; \{x \in S \mid \forall k \in \mathrm{Fin}\ n,\ v(x, j, k) \le v(x, j, i)\}. $$

In Lean: strom_A i j.

Closedness

strom_A_closed: $A(i, j)$ is closed in $\mathrm{Fin}\ n \to \mathbb{R}$.

Proof

The defining condition is a conjunction of $n$ inequalities of the form $v(x, j, k) \le v(x, j, i)$. Each inequality cuts out a closed half-space because both sides are continuous in $x$ ([[social_choice.fair_division.divisible.stromquist_value_continuous]]). The intersection of finitely many closed sets is closed.

Cover property

strom_A_covers: for each fixed $j$, the family $\{A(i, j) : i \in \mathrm{Fin}\ n\}$ covers the simplex $S$.

Proof. For any $x \in S$, agent $j$'s values $v(x, j, k)$ over $k$ form a finite collection of reals; some $i$ achieves the maximum. That $i$ witnesses $x \in A(i, j)$.

Why this matters for KKM

The pair (closed $A(i, j)$, family that covers the simplex) is exactly the input shape for a KKM-type argument: combined with the "facets-don't- touch" property of strom_A (strom_A does not intersect the face opposite vertex $i$), this lets the KKM lemma find a common point in $\bigcap_i \bigcup_j A(i, j)$ — which yields a fair division.

The unique-preference refinement ([[social_choice.fair_division.divisible.stromquist_unique_preference_sets]]) strengthens the cover to one with pairwise-disjoint witnesses, giving the final EF assignment.

References

Stromquist, W. (1980). "How to Cut a Cake Fairly". Amer. Math. Monthly 87: 640–644.
Su, F. E. (1999). "Rental Harmony: Sperner's Lemma in Fair Division". Amer. Math. Monthly 106.

Used by