EconCSLib.Math.FixedPoint.Brouwer_product

Brouwer's fixed-point theorem for products of standard simplices, proved by retraction onto a single standard simplex.

Setup

Let I be a finite linearly ordered type and card : I → ℕ+. Define:

• ProductSimplices card — the product Πᵢ stdSimplex ℝ (Fin (card i)) of standard simplices.
• BigSimplex card — the single standard simplex stdSimplex ℝ (Fin (total_card card)) where total_card card = ∑ i, card i.

The idea is that BigSimplex naturally embeds ProductSimplices as a retract.

Key constructions

• embed_from_product — embeds a product point into the big simplex by concatenating the blocks; the i-th block occupies coordinates [prefix_sum i, prefix_sum i + card i).
• project_to_product — projects a big-simplex point back to the product; the i-th component is the renormalised restriction to block i (using tPush to handle the degenerate case where a block sum is zero).
• project_embed_id — project_to_product ∘ embed_from_product = id.

Main result

• Brouwer_Product — every continuous self-map of ProductSimplices card has a fixed point.

Proof strategy

Given f : ProductSimplices card → ProductSimplices card, define the lifted map f_lifted = embed_from_product ∘ f ∘ project_to_product on BigSimplex card. Since project_embed_id holds, a fixed point of f_lifted on the big simplex projects to a fixed point of f on the product. Continuity of the lifted map follows from continuity of the embed/project maps. Apply Brouwer to f_lifted.

References

• Brouwer, L. E. J., "Über Abbildung von Mannigfaltigkeiten", Math. Ann. 71 (1912).

noncomputable def total_card {I : Type u_1} [Fintype I] [Inhabited I] (card : I → ℕ+) : ℕ+

Total number of coordinates: the sum of card i over all i.

Equations

• total_card card = ⟨∑ i : I, ↑(card i), ⋯⟩

@[reducible, inline]

abbrev BigSimplex {I : Type u_1} [Fintype I] [Inhabited I] (card : I → ℕ+) : Set (Fin ↑(total_card card) → ℝ)

The big simplex on total_card card coordinates.

Equations

• BigSimplex card = stdSimplex ℝ (Fin ↑(total_card card))

@[reducible, inline]

abbrev ProductSimplices {I : Type u_1} (card : I → ℕ+) : Type u_1

The product of simplices indexed by I.

Equations

• ProductSimplices card = ((i : I) → ↑(stdSimplex ℝ (Fin ↑(card i))))

noncomputable def prefix_sum {I : Type u_1} [Fintype I] [LinearOrder I] (card : I → ℕ+) (i : I) : ℕ

Cumulative sum of card over indices strictly less than i.

Equations

• prefix_sum card i = ∑ j : I with j < i, ↑(card j)

theorem index_split_existence {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (k : Fin ↑(total_card card)) : ∃ (p : (i : I) × Fin ↑(card i)), prefix_sum card p.fst ≤ ↑k ∧ ↑k < prefix_sum card p.fst + ↑(card p.fst) ∧ ↑p.snd = ↑k - prefix_sum card p.fst

A flat index k belongs to a unique block i with an in-block index j.

noncomputable def index_split {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (k : Fin ↑(total_card card)) : (i : I) × Fin ↑(card i)

Split a flat index k into its block/index pair (i, j).

Equations

• index_split card k = Classical.choose ⋯

theorem index_split_spec {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (k : Fin ↑(total_card card)) : have p := index_split card k; prefix_sum card p.fst ≤ ↑k ∧ ↑k < prefix_sum card p.fst + ↑(card p.fst) ∧ ↑p.snd = ↑k - prefix_sum card p.fst

Specification of index_split: bounds and value relation for (i, j).

noncomputable def index_combine {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (p : (i : I) × Fin ↑(card i)) : Fin ↑(total_card card)

Combine a block/index pair (i, j) back into a flat index.

Equations

• index_combine card p = ⟨prefix_sum card p.fst + ↑p.snd, ⋯⟩

theorem index_split_combine_inverse {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (p : (i : I) × Fin ↑(card i)) : index_split card (index_combine card p) = p

index_split is a left inverse to index_combine.

theorem index_combine_split_inverse {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (k : Fin ↑(total_card card)) : index_combine card (index_split card k) = k

index_combine is a left inverse to index_split.

noncomputable def blockWeight {I : Type u_1} [Fintype I] [Inhabited I] (card : I → ℕ+) (i : I) : ℝ

Weight (size fraction) of block i: (card i) / (total_card card).

Equations

• blockWeight card i = ↑↑(card i) / ↑↑(total_card card)

noncomputable def blockSum {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (i : I) (x : ↑(BigSimplex card)) : ℝ

Sum of coordinates of x over the block i.

Equations

• blockSum card i x = ∑ j : Fin ↑(card i), ↑x (index_combine card ⟨i, j⟩)

noncomputable def uniformProduct {I : Type u_1} (card : I → ℕ+) : ProductSimplices card

The uniform point in each block simplex.

Equations

• uniformProduct card i = ⟨fun (x : Fin ↑(card i)) => 1 / ↑↑(card i), ⋯⟩

noncomputable def z_uniform {I : Type u_1} [Fintype I] [Inhabited I] (card : I → ℕ+) : ↑(BigSimplex card)

The uniform point in the big simplex.

Equations

• z_uniform card = ⟨fun (x : Fin ↑(total_card card)) => 1 / ↑↑(total_card card), ⋯⟩

noncomputable def deficit {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (x : ↑(BigSimplex card)) : ℝ

Total positive shortfall of block sums relative to block weights.

Equations

• deficit card x = ∑ i : I, max 0 (blockWeight card i - blockSum card i x)

noncomputable def tPush {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (x : ↑(BigSimplex card)) : ℝ

Amount to push x toward z_uniform (always in [0, 1]).

Equations

• tPush card x = deficit card x / (1 + deficit card x)

noncomputable def pushTowardsZ {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (x : ↑(BigSimplex card)) : ↑(BigSimplex card)

Convex push of x toward z_uniform by amount tPush.

Equations

• pushTowardsZ card x = ⟨fun (k : Fin ↑(total_card card)) => (1 - tPush card x) * ↑x k + tPush card x * ↑(z_uniform card) k, ⋯⟩

noncomputable def project_to_product {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (x : ↑(BigSimplex card)) : ProductSimplices card

Retraction from the big simplex to the product of simplices.

Equations

• project_to_product card x i = ⟨fun (j : Fin ↑(card i)) => ↑(pushTowardsZ card x) (index_combine card ⟨i, j⟩) / blockSum card i (pushTowardsZ card x), ⋯⟩

noncomputable def embed_from_product {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (y : ProductSimplices card) : ↑(BigSimplex card)

Embedding of the product of simplices into the big simplex.

Equations

• embed_from_product card y = ⟨fun (k : Fin ↑(total_card card)) => have p := index_split card k; ↑(y p.fst) p.snd * ↑↑(card p.fst) / ↑↑(total_card card), ⋯⟩

theorem project_embed_id {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (y : ProductSimplices card) : project_to_product card (embed_from_product card y) = y

project_to_product ∘ embed_from_product = id.

theorem blockWeight_pos {I : Type u_1} [Fintype I] [Inhabited I] (card : I → ℕ+) (i : I) : 0 < blockWeight card i

theorem blockSum_nonneg {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (i : I) (x : ↑(BigSimplex card)) : 0 ≤ blockSum card i x

blockSum card i x is always nonnegative.

theorem deficit_nonneg {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (x : ↑(BigSimplex card)) : 0 ≤ deficit card x

deficit card x is always nonnegative.

theorem tPush_mem_Icc {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (x : ↑(BigSimplex card)) : tPush card x ∈ Set.Icc 0 1

tPush card x is always in [0, 1].

theorem blockSum_pushTowardsZ_formula {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (i : I) (x : ↑(BigSimplex card)) : blockSum card i (pushTowardsZ card x) = (1 - tPush card x) * blockSum card i x + tPush card x * blockWeight card i

The block sum after pushing towards z_uniform follows a linear formula.

theorem blockSum_pushTowardsZ_pos {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (i : I) (x : ↑(BigSimplex card)) : 0 < blockSum card i (pushTowardsZ card x)

The block sum after pushing towards z_uniform is always positive.

theorem blockSum_continuous {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (i : I) : Continuous (blockSum card i)

Continuity of blockSum card i.

theorem deficit_continuous {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) : Continuous (deficit card)

Continuity of deficit card.

theorem tPush_continuous {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) : Continuous (tPush card)

Continuity of tPush card.

theorem pushTowardsZ_continuous {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) : Continuous (pushTowardsZ card)

Continuity of pushTowardsZ card.

theorem project_continuous {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) : Continuous (project_to_product card)

Continuity of project_to_product.

theorem embed_continuous {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) : Continuous (embed_from_product card)

Continuity of embed_from_product.

theorem Brouwer_Product {I : Type u_1} [Fintype I] [DecidableEq I] [Inhabited I] [LinearOrder I] (card : I → ℕ+) (f : ProductSimplices card → ProductSimplices card) (hf : Continuous f) : ∃ (x : ProductSimplices card), f x = x

Brouwer fixed point theorem for a product of simplices, via a retraction.