Brouwer's fixed-point theorem on a product of simplices

This file extends Brouwer's fixed-point theorem from a single standard simplex to a finite product of standard simplices. A continuous retraction collapses the big simplex onto the product, so a fixed point of a continuous self-map of the product is obtained from the single-simplex theorem.

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

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

Equations

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

@[reducible, inline]

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

The big simplex on totalCard card coordinates.

Equations

• BigSimplex card = stdSimplex ℝ (Fin ↑(totalCard 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 prefixSum {I : Type u_1} [Fintype I] [LinearOrder I] (card : I → ℕ+) (i : I) : ℕ

Cumulative sum of card over indices strictly less than i.

Equations

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

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

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

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

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

Equations

• indexSplit card k = Classical.choose ⋯

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

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

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

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

Equations

• indexCombine card p = ⟨prefixSum 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)) : indexSplit card (indexCombine card p) = p

indexSplit is a left inverse to indexCombine.

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

indexCombine is a left inverse to indexSplit.

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

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

Equations

• blockWeight card i = ↑↑(card i) / ↑↑(totalCard 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 (indexCombine 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 zUniform {I : Type u_1} [Fintype I] [Inhabited I] (card : I → ℕ+) : ↑(BigSimplex card)

The uniform point in the big simplex.

Equations

• zUniform card = ⟨fun (x : Fin ↑(totalCard card)) => 1 / ↑↑(totalCard 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 zUniform (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 zUniform by amount tPush.

Equations

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

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 zUniform 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 zUniform is always positive.

noncomputable def projectToProduct {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

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

noncomputable def embedFromProduct {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

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

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

projectToProduct ∘ embedFromProduct = id.

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 (projectToProduct card)

Continuity of projectToProduct.

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

Continuity of embedFromProduct.

theorem Brouwer_Product {I : Type u_1} [Inhabited I] [LinearOrder I] (card : I → ℕ+) [Finite 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.