EconCSLib.Math.FixedPoint.Brouwer

Brouwer's fixed-point theorem for self-maps of the standard simplex, proved via Scarf's combinatorial lemma.

Main result

• Brouwer — every continuous map f : stdSimplex ℝ (Fin n) → stdSimplex ℝ (Fin n) has a fixed point.

Setup

The proof works by discrete approximation. For each level l : ℕ+, define the discrete triangulation lattice

TT n l = { x : Πₗ (_ : Fin n), Fin (l+1) | ∑ i, (x i : ℕ) = l }

Each element of TT n l is a tuple of nonneg integers summing to l, which embeds into the standard simplex via TTtostdSimplex x j = x j / l.

The instance TT.ILO : IndexedLOrder (Fin n) (TT n l) gives TT n l a family of linear orders indexed by Fin n: for direction i, the order on TT n l is the lexicographic order on (x i, x).

Proof strategy

1. Coloring (Fcolor): For each x : TT n l, pick a coordinate j where (f x)_j ≥ x_j — i.e., f moves x in the j-th direction. This is well-defined since ∑ x j = 1 = ∑ (f x) j forces at least one coordinate to increase.

2. Scarf's lemma (TT.ILO.Scarf): Applied with the coloring Fcolor, yields a colorful room (σ, C) at level l — a set of n lattice points covering all n directions.

3. Limit (room_seq, hpkg): As l → ∞, extract a subsequence of colorful rooms via exists_subseq_constant_of_finite_image (pigeonhole on the finite color set C), then use compactness of the simplex to obtain a convergent subsequence of the representative room points.

4. Fixed point: The limit point z satisfies f(z) ≥ z coordinatewise (by passing the coloring property through the limit). Since ∑ z_j = 1 = ∑ f(z)_j, coordinatewise inequality forces f(z) = z.

References

• Brouwer, L. E. J., "Über Abbildung von Mannigfaltigkeiten", Math. Ann. 71 (1912).
• Scarf, H. E., "The Computation of Economic Equilibria", Yale University Press, 1973.
• Todd, M. J., "The Computation of Fixed Points and Applications", Lecture Notes in Economics and Mathematical Systems 124, Springer, 1976.

instance Pi.Lex.finite {I : Type u_1} {X : I → Type u_2} [DecidableEq I] [Finite I] [∀ (a : I), Finite (X a)] : Finite (Lex ((i : I) → (fun (a : I) => X a) i))

A dependent product of finite, indexed by finite, is a finite.

@[reducible, inline]

abbrev TT (n l : ℕ+) : Set (Lex ((i : Fin ↑n) → (fun (x : Fin ↑n) => Fin (↑l + 1)) i))

Equations

• TT n l = {x : Lex ((i : Fin ↑n) → (fun (x : Fin ↑n) => Fin (↑l + 1)) i) | ∑ i : Fin ↑n, ↑(x i) = ↑l}

instance TT.finite (n l : ℕ+) : Finite ↑(TT n l)

@[implicit_reducible]

instance TT.inhabited (n l : ℕ+) : Inhabited ↑(TT n l)

Equations

• TT.inhabited n l = { default := ⟨fun (i : Fin ↑n) => if i = 0 then Fin.last ↑l else 0, ⋯⟩ }

@[implicit_reducible]

instance TT.funlike (n l : ℕ+) : FunLike (↑(TT n l)) (Fin ↑n) (Fin (↑l + 1))

Equations

• TT.funlike n l = { coe := fun (a : ↑(TT n l)) => ↑a, coe_injective' := ⋯ }

noncomputable def TTtostdSimplex {n l : ℕ+} (x : ↑(TT n l)) : ↑(stdSimplex ℝ (Fin ↑n))

Equations

• TTtostdSimplex x = ⟨fun (i : Fin ↑n) => ↑↑(x i) / ↑↑l, ⋯⟩

@[implicit_reducible]

noncomputable instance TT.CoestdSimplex (n l : ℕ+) : CoeOut ↑(TT n l) ↑(stdSimplex ℝ (Fin ↑n))

Equations

• TT.CoestdSimplex n l = { coe := TTtostdSimplex }

@[reducible, inline]

abbrev TT.Ilt {n l : ℕ+} (i : Fin ↑n) (x y : ↑(TT n l)) : Prop

Equations

• TT.Ilt i x y = (toLex (x i, x) < toLex (y i, y))

instance TT.IST (n l : ℕ+) (i : Fin ↑n) : IsStrictTotalOrder (↑(TT n l)) (Ilt i)

@[implicit_reducible]

noncomputable instance TT.ILO {n l : ℕ+} : IndexedLOrder (Fin ↑n) ↑(TT n l)

Equations

• TT.ILO = { IST := fun (i : Fin ↑n) => linearOrderOfSTO (TT.Ilt i) }

theorem TT.Ilt_def (n l : ℕ+) (i : Fin ↑n) (a b : ↑(TT n l)) : a < b ↔ Ilt i a b

theorem TT.Ilt_keyprop (n l : ℕ+) (i : Fin ↑n) (a b : ↑(TT n l)) : a i < b i → a < b

theorem size_bound_key (n l : ℕ+) (σ : Finset ↑(TT n l)) (C : Finset (Fin ↑n)) (h : IndexedLOrder.isDominant σ C) (h2 : σ.Nonempty) : ↑l < ∑ k ∈ C, (Finset.image (fun (x : ↑(TT n l)) => ↑(x k)) σ).min' ⋯ + C.card

theorem size_bound_in (n l : ℕ+) (σ : Finset ↑(TT n l)) (C : Finset (Fin ↑n)) (h : IndexedLOrder.isDominant σ C) (x : ↑(TT n l)) : x ∈ σ → ∀ y ∈ σ, ∀ (i : Fin ↑n), |↑↑(x i) - ↑↑(y i)| < 2 * (↑↑n + 1)

theorem size_bound_out (n l : ℕ+) (σ : Finset ↑(TT n l)) (C : Finset (Fin ↑n)) (h : IndexedLOrder.isDominant σ C) (x : ↑(TT n l)) : x ∈ σ → ∀ i ∉ C, ↑↑(x i) < ↑↑n + 1

instance stdSimplex.upidx {n : ℕ+} (x y : ↑(stdSimplex ℝ (Fin ↑n))) : Nonempty ↑{i : Fin ↑n | ↑x i ≤ ↑y i}

noncomputable def stdSimplex.pick {n : ℕ+} (x y : ↑(stdSimplex ℝ (Fin ↑n))) : ↑{i : Fin ↑n | ↑x i ≤ ↑y i}

Equations

• stdSimplex.pick x y = Classical.choice ⋯

noncomputable def Fcolor {n l : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (x : ↑(TT n l)) : Fin ↑n

Equations

• Fcolor f x = ↑(stdSimplex.pick (TTtostdSimplex x) (f (TTtostdSimplex x)))

noncomputable def room_seq {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (l' : ℕ) : ↥(IndexedLOrder.colorful (Fcolor f))

Equations

• room_seq f l' = Classical.choice ⋯

noncomputable def room_point_seq {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (l' : ℕ) : ↑(TT n ⟨l' + 1, ⋯⟩)

Equations

• room_point_seq f l' = ↑(IndexedLOrder.pick_colorful_point ⋯)

def mk_subseq (f : ℕ → ℕ) (h : ∀ (n : ℕ), n < f n) : ℕ → ℕ

Equations

• mk_subseq f h 0 = f 0
• mk_subseq f h n.succ = f (mk_subseq f h n)

theorem exists_subseq_constant_of_finite_image {X : Type u_1} {s : Finset X} (e : ℕ → X) (he : ∀ (n : ℕ), e n ∈ s) : ∃ a ∈ s, ∃ (g : ℕ ↪o ℕ), ∀ (n : ℕ), e (g n) = a

theorem constant_index_set_nonempty {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : Nonempty ↑{(a, g) : Finset (Fin ↑n) × (ℕ ↪o ℕ) | ∀ (l' : ℕ), (↑(room_seq f (g l'))).2 = a}

noncomputable def gpkg {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : ↑{(a, g) : Finset (Fin ↑n) × (ℕ ↪o ℕ) | ∀ (l' : ℕ), (↑(room_seq f (g l'))).2 = a}

Equations

• gpkg f = Classical.choice ⋯

@[reducible, inline]

noncomputable abbrev g1 {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : ℕ ↪o ℕ

Equations

• g1 f = (↑(gpkg f)).2

theorem dominant_coords_tend_to_zero {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (C : Finset (Fin ↑n)) (g : ℕ ↪o ℕ) (h_const : ∀ (l' : ℕ), (↑(room_seq f (g l'))).2 = C) (i : Fin ↑n) : i ∉ C → Filter.Tendsto (fun (l' : ℕ) => ↑(TTtostdSimplex (room_point_seq f (g l'))) i) Filter.atTop (nhds 0)

@[reducible]

def hpkg_aux {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : Nonempty ↑{(z, h) : ↑(stdSimplex ℝ (Fin ↑n)) × (ℕ → ℕ) | StrictMono h ∧ Filter.Tendsto ((fun (l' : ℕ) => TTtostdSimplex (room_point_seq f ((g1 f) l'))) ∘ h) Filter.atTop (nhds z)}

Equations

• ⋯ = ⋯

noncomputable def hpkg {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : ↑{(z, h) : ↑(stdSimplex ℝ (Fin ↑n)) × (ℕ → ℕ) | StrictMono h ∧ Filter.Tendsto ((fun (l' : ℕ) => TTtostdSimplex (room_point_seq f ((g1 f) l'))) ∘ h) Filter.atTop (nhds z)}

Equations

• hpkg f = Classical.choice ⋯

theorem tendsto_diam_to_zero {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) : Filter.Tendsto (fun (k : ℕ) => Metric.diam ↑(Finset.image (fun (x : ↑(TT n ⟨(g1 f) ((↑(hpkg f)).2 k) + 1, ⋯⟩)) => TTtostdSimplex x) (↑(room_seq f ((g1 f) ((↑(hpkg f)).2 k)))).1)) Filter.atTop (nhds 0)

theorem f_coords_ge_z_coords {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (hf : Continuous f) (i : Fin ↑n) : i ∈ (↑(gpkg f)).1 → ↑(f (↑(hpkg f)).1) i ≥ ↑(↑(hpkg f)).1 i

theorem Brouwer {n : ℕ+} (f : ↑(stdSimplex ℝ (Fin ↑n)) → ↑(stdSimplex ℝ (Fin ↑n))) (hf : Continuous f) : ∃ (x : ↑(stdSimplex ℝ (Fin ↑n))), f x = x