Brouwer's fixed-point theorem on a simplex

This file derives Brouwer's fixed-point theorem for a continuous self-map of the standard simplex from Scarf's lemma. The combinatorial type TT n l of integer points of the scaled simplex carries an IndexedLOrder; applying Scarf's lemma to finer and finer subdivisions and passing to a convergent subsequence of the resulting colorful points produces a fixed point.

instance Pi.Lex.finite {α : Type u_1} {β : α → Type u_2} [Finite α] [∀ (a : α), Finite (β a)] : Finite (Lex ((i : α) → (fun (a : α) => β 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))

The combinatorial type of integer points of the l-scaled n-simplex.

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))

The point of the standard simplex associated to an integer point of TT n l.

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

The strict order on TT n l at index i, comparing the i-th coordinate first.

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)) : IndexedLOrder.ltAt i a b ↔ Ilt i a b

theorem TT.Ilt_keyprop (n l : ℕ+) (i : Fin ↑n) (a b : ↑(TT n l)) : a i < b i → IndexedLOrder.ltAt 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}

A chosen index where x does not exceed y, for two simplex points.

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

The Scarf coloring induced on TT n l by a self-map f of the simplex.

Equations

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

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

A colorful room produced by Scarf lemma for the l-th subdivision.

Equations

• roomSeq f l' = Classical.choice ⋯

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

A point of the colorful room roomSeq, as an integer point of TT.

Equations

• roomPointSeq f l' = ↑(IndexedLOrder.pickColorfulPoint ⋯)

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

The subsequence of indices generated by iterating a step function.

Equations

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

theorem exists_subseq_constant_of_finite_image {α : Type u_1} {s : Finset α} (e : ℕ → α) (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' : ℕ), (↑(roomSeq f (g l'))).2 = a}

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

A constant-index colorful subsequence package extracted from roomSeq.

Equations

• gpkg f = Classical.choice ⋯

@[reducible, inline]

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

The index subsequence selected by gpkg.

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' : ℕ), (↑(roomSeq f (g l'))).2 = C) (i : Fin ↑n) : i ∉ C → Filter.Tendsto (fun (l' : ℕ) => ↑(TTtostdSimplex (roomPointSeq f (g l'))) i) Filter.atTop (nhds 0)

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

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

A convergent colorful subsequence package, with its limit point.

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) (↑(roomSeq 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