Chapter 28: Pigeon-hole and double counting

A proposed formalization of Chapter 28 of Proofs from THE BOOK (Aigner–Ziegler). The supplied proofs are undergoing verification with the repository's pinned Lean toolchain.

• Pigeon-hole principle, including the strong form (1).
• 1. Numbers: Claims 1 and 2, and the sharpness examples.
• 2. Sequences: Erdős–Szekeres (book proof), sharpness for mn numbers, the dimension of Kₙ (dim K₃ = dim K₄ = 3, dim K₁₂ ≤ 4, monotonicity, and dim(Kₙ) ≥ log₂ log₂ n).
• 3. Sums: contiguous block sums divisible by n.
• Double counting (3).
• 4. Numbers again: Hₙ − 1 < t̄(n) ≤ Hₙ and log n − 1 < t̄(n) < log n + 1.
• 5. Graphs: handshaking lemma (4), Reiman's bound (6) for C₄-free graphs, the graph Gp (no C₄, p² + p + 1 vertices, degrees, the trace argument giving p + 1 points on the conic, p² solutions of x² + y² + z² = 0, and |E(Gp)| = (n−1)/4 · (1 + √(4n−3))).
• 6. Sperner's lemma (double-counting proof, abstract form and for the standard triangulation) and Brouwer's fixed point theorem for n = 2 (and n = 1).

===================== Part: Basic =====================

Pigeon-hole and double counting — basic results

Sections 1, 3, the double counting principle, Section 4 (numbers again) and the first part of Section 5 (graphs) of Chapter 28.

theorem chapter28.ite_of_pos {α : Sort u_1} {c : Prop} [Decidable c] (hc : c) (a b : α) : (if c then a else b) = a

Reduce an if whose condition holds.

theorem chapter28.ite_of_neg {α : Sort u_1} {c : Prop} [Decidable c] (hc : ¬c) (a b : α) : (if c then a else b) = b

Reduce an if whose condition fails.

theorem chapter28.dite_of_neg {α : Sort u_1} {c : Prop} [Decidable c] (hc : ¬c) (a : c → α) (b : ¬c → α) : (if h : c then a h else b h) = b hc

Reduce a dependent if whose condition fails.

theorem chapter28.pigeon_hole_principle (n r : ℕ) (h : r < n) (object_to_boxes : Fin n → Fin r) : ∃ (box : Fin r) (object₁ : Fin n) (object₂ : Fin n), object₁ ≠ object₂ ∧ object_to_boxes object₁ = box ∧ object_to_boxes object₂ = box

theorem chapter28.handshaking {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} [DecidableRel G.Adj] : ∑ v : α, G.degree v = 2 * G.edgeFinset.card

Handshaking lemma: The sum of vertex degrees equals twice the number of edges.

This is also available in Mathlib as SimpleGraph.sum_degrees_eq_twice_card_edges, which uses darts (oriented edges) as the intermediate counting object. Our proof follows the book's double-counting argument more faithfully: we count incidence pairs (v, e) with v ∈ e, swap the summation order via Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow, then observe each edge contributes exactly 2.

theorem chapter28.claim1_coprime (n : ℕ) (S : Finset (Fin (2 * n))) (hS : n < S.card) : ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ (↑a + 1).Coprime (↑b + 1)

Claim 1 (Coprime pair): From any n+1 numbers in {0,...,2n-1} (representing {1,...,2n}), two must be coprime (as values +1).

theorem chapter28.claim2_divisible (n : ℕ) (hn : 0 < n) (S : Finset ℕ) (hS_sub : ∀ x ∈ S, 1 ≤ x ∧ x ≤ 2 * n) (hS_card : S.card = n + 1) : ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ a ∣ b

Claim 2: Any n+1 numbers from {1, 2, ..., 2n} contain two where one divides the other.

theorem chapter28.claim4_contiguous_sum (n : ℕ) (hn : 0 < n) (a : Fin n → ℤ) : ∃ (l : Fin n) (r : Fin n), l ≤ r ∧ ↑n ∣ ∑ i ∈ Finset.Icc l r, a i

Claim 4 (Contiguous sum divisible by n): Given n integers, there exists a nonempty contiguous subsequence whose sum is divisible by n.

Double Counting

theorem chapter28.double_counting {α : Type u_2} {β : Type u_3} (R : Finset α) (C : Finset β) (r : α → β → Prop) [(a : α) → (b : β) → Decidable (r a b)] : ∑ p ∈ R, (Finset.bipartiteAbove r C p).card = ∑ q ∈ C, (Finset.bipartiteBelow r R q).card

Double counting: the sum over rows of the number of related columns equals the sum over columns of the number of related rows. This is a direct wrapper around Mathlib's Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow.

5. Graphs — C₄-free edge bound

theorem chapter28.sum_choose_deg_le_choose_card {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hC4 : ∀ (a b c d : V), a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a)) : ∑ v : V, (G.degree v).choose 2 ≤ (Fintype.card V).choose 2

In a C₄-free graph, the sum of C(d(v), 2) over all vertices is at most C(n, 2).

This is the key combinatorial inequality: each pair of vertices can have at most one common neighbor (otherwise they'd form a 4-cycle), so the number of "cherries" (paths of length 2) is at most the number of vertex pairs.

theorem chapter28.c4_free_edge_bound {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hC4 : ∀ (a b c d : V), a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → ¬(G.Adj a b ∧ G.Adj b c ∧ G.Adj c d ∧ G.Adj d a)) (n : ℕ) (hn : Fintype.card V = n) : G.edgeFinset.card ≤ ⌊↑n / 4 * (1 + √(4 * ↑n - 3))⌋₊

If a simple graph on n vertices contains no 4-cycle (C₄), then |E| ≤ ⌊n/4 · (1 + √(4n − 3))⌋.

The proof uses sum_choose_deg_le_choose_card together with the handshaking lemma and Cauchy–Schwarz / Jensen.

4. Numbers again

theorem chapter28.sum_divisor_count (n : ℕ) : ∑ j ∈ Finset.Icc 1 n, j.divisors.card = ∑ i ∈ Finset.Icc 1 n, n / i

Double counting for divisor sums: Σ_{j=1}^{n} (number of divisors of j) = Σ_{i=1}^{n} ⌊n/i⌋.

Both sides count pairs (i, j) with 1 ≤ i ≤ n, 1 ≤ j ≤ n, and i ∣ j. LHS groups by j (divisors of j), RHS groups by i (multiples of i up to n).

theorem chapter28.avg_divisor_count_le_harmonic (n : ℕ) : ∑ j ∈ Finset.Icc 1 n, ↑j.divisors.card ≤ ↑n * ∑ i ∈ Finset.Icc 1 n, 1 / ↑i

The average number of divisors is bounded by the harmonic sum: ∑ j in [1,n], t(j) ≤ n * Hₙ where t(j) = #(divisors j) and Hₙ = ∑ 1/i.

theorem chapter28.avg_divisor_count_lower_bound (n : ℕ) (hn : 0 < n) : ↑n * ∑ i ∈ Finset.Icc 1 n, 1 / ↑i - ↑n < ∑ j ∈ Finset.Icc 1 n, ↑j.divisors.card

Lower bound: ∑ t(j) > n·Hₙ − n, i.e., t̄(n) > Hₙ − 1 > log n − 1.

===================== Part: PigeonHole =====================

The pigeon-hole principle: strong form and sharpness of the claims in Section 1

theorem chapter28.pigeon_hole_strong {N : Type u_1} {R : Type u_2} [Fintype N] [Fintype R] [DecidableEq R] (hR : 0 < Fintype.card R) (f : N → R) : ∃ (a : R), ⌈↑(Fintype.card N) / ↑(Fintype.card R)⌉₊ ≤ {x : N | f x = a}.card

Pigeon-hole principle, strong form (1). If f : N → R with |R| = r > 0 and |N| = n, then some a ∈ R has |f⁻¹(a)| ≥ ⌈n / r⌉.

theorem chapter28.claim1_sharp (n : ℕ) : ∃ (S : Finset (Fin (2 * n))), S.card = n ∧ ∀ a ∈ S, ∀ b ∈ S, a ≠ b → ¬(↑a + 1).Coprime (↑b + 1)

Sharpness of Claim 1: {2, 4, …, 2n} has n elements, no two of which are relatively prime. (Numbers in {1, …, 2n} are represented as a + 1 for a : Fin (2n).)

theorem chapter28.claim2_sharp (n : ℕ) : ∃ (S : Finset ℕ), (∀ x ∈ S, 1 ≤ x ∧ x ≤ 2 * n) ∧ S.card = n ∧ ∀ a ∈ S, ∀ b ∈ S, a ≠ b → ¬a ∣ b

Sharpness of Claim 2: {n + 1, n + 2, …, 2n} has n elements, none of which divides another one.

===================== Part: ErdosSzekeres =====================

Section 2 of Chapter 28: Sequences

• The Erdős–Szekeres theorem on monotone subsequences, with the book's proof (label every element by the length of a longest increasing subsequence starting there, and apply the pigeon-hole principle in the strong form (1)).
• The sharpness remark: for mn numbers the statement fails in general.
• The dimension of the complete graph Kₙ and the bound dim(Kₙ) ≥ log₂ log₂ n.

noncomputable def chapter28.incSeqs {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (f : ι → ℝ) (S : Finset ι) (i : ι) : Finset (Finset ι)

The increasing subsequences (inside S) starting at i.

Equations

• chapter28.incSeqs f S i = {t ∈ S.powerset | i ∈ t ∧ (∀ j ∈ t, i ≤ j) ∧ StrictMonoOn f ↑t}

theorem chapter28.mem_incSeqs {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] {f : ι → ℝ} {S : Finset ι} {i : ι} {t : Finset ι} : t ∈ incSeqs f S i ↔ t ⊆ S ∧ i ∈ t ∧ (∀ j ∈ t, i ≤ j) ∧ StrictMonoOn f ↑t

noncomputable def chapter28.incLen {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (f : ι → ℝ) (S : Finset ι) (i : ι) : ℕ

The length tᵢ of a longest increasing subsequence (inside S) starting at i.

Equations

• chapter28.incLen f S i = (chapter28.incSeqs f S i).sup Finset.card

theorem chapter28.incLen_spec {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (f : ι → ℝ) (S : Finset ι) {i : ι} (hi : i ∈ S) : ∃ t ⊆ S, i ∈ t ∧ (∀ j ∈ t, i ≤ j) ∧ StrictMonoOn f ↑t ∧ t.card = incLen f S i

theorem chapter28.le_incLen {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (f : ι → ℝ) (S : Finset ι) {i : ι} {t : Finset ι} (htS : t ⊆ S) (hit : i ∈ t) (hmin : ∀ j ∈ t, i ≤ j) (hmono : StrictMonoOn f ↑t) : t.card ≤ incLen f S i

theorem chapter28.one_le_incLen {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (f : ι → ℝ) (S : Finset ι) {i : ι} (hi : i ∈ S) : 1 ≤ incLen f S i

theorem chapter28.incLen_lt_of_lt {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (f : ι → ℝ) (S : Finset ι) {i j : ι} (hi : i ∈ S) (hj : j ∈ S) (hij : i < j) (hf : f i < f j) : incLen f S j < incLen f S i

The key observation: if i < j and aᵢ < aⱼ, then tᵢ > tⱼ.

theorem chapter28.erdos_szekeres_book {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (m n : ℕ) (f : ι → ℝ) (S : Finset ι) (hf : Set.InjOn f ↑S) (hS : m * n < S.card) : (∃ t ⊆ S, m < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ t ⊆ S, n < t.card ∧ StrictAntiOn f ↑t

Erdős–Szekeres (book proof), finset version. If f is injective on a finite set S of indices with |S| > m n, then there is an increasing subsequence of length m + 1 or a decreasing subsequence of length n + 1.

theorem chapter28.claim3_erdos_szekeres (m n : ℕ) (f : Fin (m * n + 1) → ℝ) (hf : Function.Injective f) : (∃ (t : Finset (Fin (m * n + 1))), m < t.card ∧ StrictMonoOn f ↑t) ∨ ∃ (t : Finset (Fin (m * n + 1))), n < t.card ∧ StrictAntiOn f ↑t

Claim 3 (Erdős–Szekeres): In any sequence a₁, …, a_{mn+1} of mn + 1 distinct real numbers there is an increasing subsequence of length m + 1 or a decreasing subsequence of length n + 1 (or both).

def chapter28.esSharpSeq (m x : ℕ) : ℝ

The counterexample sequence of length mn used for the sharpness remark: n decreasing blocks, each block an increasing run of length m.

Equations

• chapter28.esSharpSeq m x = ↑(x % m) - ↑m * ↑(x / m)

theorem chapter28.erdos_szekeres_sharp (m n : ℕ) : (Function.Injective fun (x : Fin (m * n)) => esSharpSeq m ↑x) ∧ (∀ (t : Finset (Fin (m * n))), StrictMonoOn (fun (x : Fin (m * n)) => esSharpSeq m ↑x) ↑t → t.card ≤ m) ∧ ∀ (t : Finset (Fin (m * n))), StrictAntiOn (fun (x : Fin (m * n)) => esSharpSeq m ↑x) ↑t → t.card ≤ n

Sharpness remark. For mn numbers the Erdős–Szekeres statement is no longer true in general: the sequence esSharpSeq of length m n is injective and has neither an increasing subsequence of length m + 1 nor a decreasing subsequence of length n + 1.

===================== Part: KnDimension =====================

The dimension of the complete graph Kₙ (Section 2 of Chapter 28)

Let N = {1, …, n}. Permutations π₁, …, πₘ of N represent Kₙ if for every three distinct numbers i, j, k there is a permutation in which k comes after both i and j. The dimension dim(Kₙ) is the smallest such m. We encode a permutation by its position function σ : Equiv.Perm (Fin n), where σ x is the position of x.

Main results:

• dimK_mono : dim(Kₙ) ≤ dim(Kₙ₊₁);
• dimK_three, dimK_four : dim(K₃) = dim(K₄) = 3;
• dimK_twelve_le : the four permutations from the margin represent K₁₂;
• dimK_ge_log_log : dim(Kₙ) ≥ log₂ log₂ n (inequality (2)).

theorem chapter28.KnDimension.erdos_szekeres_finset {n m : ℕ} (f : Fin n → ℝ) (S : Finset (Fin n)) (hcard : m * m < S.card) (hf : Set.InjOn f ↑S) : ∃ T ⊆ S, m < T.card ∧ (StrictMonoOn f ↑T ∨ StrictAntiOn f ↑T)

Erdős-Szekeres on finsets: Given a finset S of size > m² and a function f injective on S, there exists a subset T ⊆ S of size > m on which f is monotone.

theorem chapter28.KnDimension.iterated_erdos_szekeres (p : ℕ) {n : ℕ} (fs : Fin p → Fin n → ℝ) (S : Finset (Fin n)) : (∀ (i : Fin p), Set.InjOn (fs i) ↑S) → 2 ^ 2 ^ p < S.card → ∃ T ⊆ S, 2 < T.card ∧ ∀ (i : Fin p), StrictMonoOn (fs i) ↑T ∨ StrictAntiOn (fs i) ↑T

Iterated Erdős-Szekeres: Given p injective functions on Fin n and a finset S with |S| > 2^(2^p), there exists a subset T ⊆ S with |T| > 2 that is simultaneously monotone (each function is either strictly increasing or strictly decreasing on T).

theorem chapter28.KnDimension.kn_dimension_bound (p n : ℕ) (hn : 2 ^ 2 ^ p < n) (fs : Fin p → Fin n → ℝ) (hfs : ∀ (i : Fin p), Function.Injective (fs i)) : ∃ (T : Finset (Fin n)), 2 < T.card ∧ ∀ (i : Fin p), StrictMonoOn (fs i) ↑T ∨ StrictAntiOn (fs i) ↑T

Simultaneous monotone triple: For n > 2^(2^p) and p injective functions Fin n → ℝ, there exists a subset of size > 2 that is monotone for all of them.

This captures the lower bound dim(Kₙ) ≥ ⌈log₂(⌈log₂ n⌉)⌉: fewer than ⌈log₂(⌈log₂ n⌉)⌉ linear orders cannot separate all triples.

theorem chapter28.KnDimension.kn_dimension_clog_bound (n p : ℕ) (hp : p < Nat.clog 2 (Nat.clog 2 n)) (fs : Fin p → Fin n → ℝ) (hfs : ∀ (i : Fin p), Function.Injective (fs i)) : ∃ (T : Finset (Fin n)), 2 < T.card ∧ ∀ (i : Fin p), StrictMonoOn (fs i) ↑T ∨ StrictAntiOn (fs i) ↑T

Ceiling-log formulation: If p < ⌈log₂(⌈log₂ n⌉)⌉, then p injective functions on Fin n cannot separate all triples. This is the dim(Kₙ) ≥ ⌈log₂(⌈log₂ n⌉)⌉ bound.

def chapter28.RepresentsK (n m : ℕ) (π : Fin m → Equiv.Perm (Fin n)) : Prop

The permutations π 0, …, π (m-1) of Fin n represent Kₙ: for every three distinct i, j, k there is a permutation in which k comes after both i and j. Each permutation is encoded by its position function (π l x is the position of x in the l-th ordering).

Equations

• chapter28.RepresentsK n m π = ∀ (i j k : Fin n), i ≠ j → i ≠ k → j ≠ k → ∃ (l : Fin m), (π l) i < (π l) k ∧ (π l) j < (π l) k

def chapter28.RepresentsKRank (n m : ℕ) (r : Fin m → Fin n → ℕ) : Prop

The same notion for orderings given by arbitrary (injective) rankings into ℕ.

Equations

• chapter28.RepresentsKRank n m r = ∀ (i j k : Fin n), i ≠ j → i ≠ k → j ≠ k → ∃ (l : Fin m), r l i < r l k ∧ r l j < r l k

@[instance_reducible]

instance chapter28.instDecidableRepresentsKRank (n m : ℕ) (r : Fin m → Fin n → ℕ) : Decidable (RepresentsKRank n m r)

Equations

• chapter28.instDecidableRepresentsKRank n m r = id inferInstance

theorem chapter28.exists_perm_of_injective {n : ℕ} (f : Fin n → ℕ) (hf : Function.Injective f) : ∃ (σ : Equiv.Perm (Fin n)), ∀ (x y : Fin n), σ x < σ y ↔ f x < f y

An injective ranking of Fin n is induced by a permutation (its position function).

noncomputable def chapter28.dimK (n : ℕ) : ℕ

The dimension dim(Kₙ): the smallest number of permutations representing Kₙ.

Equations

• chapter28.dimK n = sInf {m : ℕ | ∃ (π : Fin m → Equiv.Perm (Fin n)), chapter28.RepresentsK n m π}

theorem chapter28.representsK_of_rank {n m : ℕ} (r : Fin m → Fin n → ℕ) (hr : ∀ (l : Fin m), Function.Injective (r l)) (h : RepresentsKRank n m r) : ∃ (π : Fin m → Equiv.Perm (Fin n)), RepresentsK n m π

theorem chapter28.dimK_le_of_rank {n m : ℕ} (r : Fin m → Fin n → ℕ) (hr : ∀ (l : Fin m), Function.Injective (r l)) (h : RepresentsKRank n m r) : dimK n ≤ m

theorem chapter28.dimK_le_self (n : ℕ) : dimK n ≤ n

Kₙ is always represented by n permutations (put each k last once).

theorem chapter28.dimK_spec (n : ℕ) : ∃ (π : Fin (dimK n) → Equiv.Perm (Fin n)), RepresentsK n (dimK n) π

theorem chapter28.dimK_mono (n : ℕ) : dimK n ≤ dimK (n + 1)

dim(Kₙ) ≤ dim(Kₙ₊₁): just delete n + 1 in a representation of Kₙ₊₁.

theorem chapter28.dimK_monotone : Monotone dimK

theorem chapter28.three_le_dimK {n : ℕ} (hn : 3 ≤ n) : 3 ≤ dimK n

For n ≥ 3, any representation needs at least three permutations: each of three fixed numbers must come last (among the three) in some permutation, and these permutations are distinct.

def chapter28.listRank {n m : ℕ} (L : Fin m → List (Fin n)) : Fin m → Fin n → ℕ

Rankings given by listing the elements of Fin n in order.

Equations

• chapter28.listRank L l x = List.idxOf x (L l)

theorem chapter28.dimK_three : dimK 3 = 3

dim(K₃) = 3, using π₁ = (1,2,3), π₂ = (2,3,1), π₃ = (3,1,2).

theorem chapter28.dimK_four : dimK 4 = 3

dim(K₄) = 3, using π₁ = (1,2,3,4), π₂ = (2,4,3,1), π₃ = (1,4,3,2).

theorem chapter28.dimK_twelve_le : dimK 12 ≤ 4

The four permutations from the margin represent K₁₂, so dim(K₁₂) ≤ 4.

theorem chapter28.dimK_le_four {n : ℕ} (hn : n ≤ 12) : dimK n ≤ 4

Consequently dim(Kₙ) ≤ 4 for all n ≤ 12.

theorem chapter28.not_representsK_of_lt {p n : ℕ} (hn : 2 ^ 2 ^ p < n) (π : Fin p → Equiv.Perm (Fin n)) : ¬RepresentsK n p π

The key step of (2): p permutations cannot represent Kₙ when n > 2^(2^p), because iterated Erdős–Szekeres yields three numbers a < b < c which are monotone in every permutation, so b never comes after both a and c.

theorem chapter28.le_two_pow_two_pow_dimK (n : ℕ) : n ≤ 2 ^ 2 ^ dimK n

Equivalently: n ≤ 2^(2^dim(Kₙ)).

theorem chapter28.dimK_ge_succ (p : ℕ) : p + 1 ≤ dimK (2 ^ 2 ^ p + 1)

In the form used in the book: dim(Kₙ) ≥ p + 1 for n = 2^(2^p) + 1.

theorem chapter28.dimK_ge_log_log (n : ℕ) : Real.logb 2 (Real.logb 2 ↑n) ≤ ↑(dimK n)

Inequality (2): dim(Kₙ) ≥ log₂ log₂ n.

===================== Part: Divisors =====================

Section 4 of Chapter 28: the average number of divisors

With t(j) the number of divisors of j and t̄(n) = (1/n) ∑_{j ≤ n} t(j), we prove Hₙ − 1 < t̄(n) ≤ Hₙ and log n − 1 < Hₙ − 1 − 1/n < t̄(n) ≤ Hₙ < log n + 1 (for n ≥ 2).

noncomputable def chapter28.avgDivisors (n : ℕ) : ℝ

The average number of divisors t̄(n) = (1/n) ∑_{j=1}^{n} t(j).

Equations

• chapter28.avgDivisors n = 1 / ↑n * ∑ j ∈ Finset.Icc 1 n, ↑j.divisors.card

theorem chapter28.sum_one_div_eq_harmonic (n : ℕ) : ∑ i ∈ Finset.Icc 1 n, 1 / ↑i = harmonic n

theorem chapter28.avgDivisors_bounds {n : ℕ} (hn : 0 < n) : ↑(harmonic n) - 1 < avgDivisors n ∧ avgDivisors n ≤ ↑(harmonic n)

Hₙ − 1 < t̄(n) ≤ Hₙ.

theorem chapter28.log_succ_sub_log_gt {m : ℕ} (hm : 0 < m) : 1 / (↑m + 1) < Real.log (↑m + 1) - Real.log ↑m

log(n+1) − log n > 1/(n+1) for n > 0.

theorem chapter28.log_succ_sub_log_lt {m : ℕ} (hm : 0 < m) : Real.log (↑m + 1) - Real.log ↑m < 1 / ↑m

log(n+1) − log n < 1/n for n > 0.

theorem chapter28.harmonic_lt_log_add_one {n : ℕ} (hn : 2 ≤ n) : ↑(harmonic n) < Real.log ↑n + 1

Hₙ < log n + 1 for n ≥ 2.

theorem chapter28.log_lt_harmonic_sub {n : ℕ} (hn : 2 ≤ n) : Real.log ↑n < ↑(harmonic n) - 1 / ↑n

log n < H_{n-1} = Hₙ − 1/n for n ≥ 2.

theorem chapter28.avgDivisors_log_bounds {n : ℕ} (hn : 2 ≤ n) : Real.log ↑n - 1 < ↑(harmonic n) - 1 - 1 / ↑n ∧ ↑(harmonic n) - 1 - 1 / ↑n < avgDivisors n ∧ avgDivisors n ≤ ↑(harmonic n) ∧ ↑(harmonic n) < Real.log ↑n + 1

The average number of divisors: log n − 1 < Hₙ − 1 − 1/n < t̄(n) ≤ Hₙ < log n + 1 for all n ≥ 2.

theorem chapter28.abs_avgDivisors_sub_log_lt {n : ℕ} (hn : 2 ≤ n) : |avgDivisors n - Real.log ↑n| < 1

Consequently |t̄(n) − log n| < 1 for n ≥ 2.

===================== Part: ReimanGraph =====================

The Reiman graph Gp (Section 5 of Chapter 28, second part)

The Reiman graph Gp: a tight construction for the C₄-free bound

The book constructs a graph Gp for each odd prime p:

• Vertices = points of PG(2,p), i.e., one-dimensional subspaces of (ZMod p)³
• Two vertices [u],[v] are adjacent iff ⟨u,v⟩ = u₁v₁ + u₂v₂ + u₃v₃ = 0
• Gp is C₄-free
• Edge count achieves the bound from c4_free_edge_bound

We use Mathlib's Projectivization and Projectivization.orthogonal.

@[reducible, inline]

abbrev chapter28.PG2 (p : ℕ) [Fact (Nat.Prime p)] : Type

The projective plane over 𝔽ₚ.

Equations

• chapter28.PG2 p = Projectivization (ZMod p) (Fin 3 → ZMod p)

noncomputable def chapter28.reimanGraph (p : ℕ) [Fact (Nat.Prime p)] : SimpleGraph (PG2 p)

The Reiman graph Gp: vertices are points of PG(2,p), adjacency is orthogonality.

Equations

• chapter28.reimanGraph p = SimpleGraph.fromRel fun (v w : chapter28.PG2 p) => Projectivization.orthogonal v w

theorem chapter28.reimanGraph_adj (p : ℕ) [Fact (Nat.Prime p)] {v w : PG2 p} : (reimanGraph p).Adj v w ↔ v ≠ w ∧ Projectivization.orthogonal v w

Adjacency in Gp: distinct orthogonal points.

theorem chapter28.reimanGraph_card_vertices (p : ℕ) [Fact (Nat.Prime p)] : Nat.card (PG2 p) = p ^ 2 + p + 1

The number of vertices of Gp is p² + p + 1. Note: The tex assumes p is an odd prime, but oddness is not needed for the cardinality formula — only that p is a prime (hence ZMod p is a field).

theorem chapter28.orthogonal_both_eq_cross {F : Type u_1} [Field F] [DecidableEq F] {a c : Projectivization F (Fin 3 → F)} (hac : a ≠ c) {x : Projectivization F (Fin 3 → F)} (hxa : x.orthogonal a) (hxc : x.orthogonal c) : x = a.cross c

In PG(2,F), if a point x is orthogonal to two distinct points a and c, then x = cross a c. This is the uniqueness of the intersection of two hyperplanes (each hyperplane is the set of points orthogonal to a given point). Proof: by the BAC-CAB identity, w × (u × v) = (w·v)u − (u·w)v = 0 when w·u = 0 and w·v = 0, so the representatives are proportional.

theorem chapter28.reimanGraph_no_C4 (p : ℕ) [Fact (Nat.Prime p)] (a b c d : PG2 p) : a ≠ c → b ≠ d → ¬((reimanGraph p).Adj a b ∧ (reimanGraph p).Adj b c ∧ (reimanGraph p).Adj c d ∧ (reimanGraph p).Adj d a)

Key lemma for no C₄: if two distinct points v, w are both orthogonal to two distinct points a, b, then v = w. Equivalently, the "orthogonal complement" hyperplanes of distinct points intersect in at most a single projective point.

This is the projective geometry fact that two distinct hyperplanes in PG(2,p) meet in exactly one point.

Note: The tex states this for 4 distinct vertices (6 pairwise ≠ conditions), but the proof only needs a ≠ c and b ≠ d. The other four ≠ conditions follow from Adj being irreflexive (loopless graph).

theorem chapter28.orthogonal_set_card (p : ℕ) [Fact (Nat.Prime p)] [Fintype (PG2 p)] (v : PG2 p) : {w : PG2 p | Projectivization.orthogonal v w}.card = p + 1

The projective hyperplane orthogonal to a point has p+1 elements.

theorem chapter28.reimanGraph_degree_eq (p : ℕ) [Fact (Nat.Prime p)] [Fintype (PG2 p)] [DecidableEq (PG2 p)] [DecidableRel (reimanGraph p).Adj] (v : PG2 p) : (reimanGraph p).degree v = if Projectivization.orthogonal v v then p else p + 1

Each vertex's degree: p if self-orthogonal, p+1 otherwise. The orthogonal hyperplane of [v] in PG(2,p) has p+1 projective points. If v·v = 0, then [v] is among them and the degree is p; otherwise p+1.

===================== Part: ReimanEdges =====================

The number of edges of the Reiman graph Gp

We follow the book: the number of vertices of Gp of degree p is the number of self-orthogonal points (points on the conic x² + y² + z² = 0), which equals trace A for the symmetric 0/1 matrix A with a_{vw} = 1 ↔ ⟨v, w⟩ = 0. Since A² = pI + J and A𝟙 = (p+1)𝟙, every eigenvalue of A is p + 1 or ±√p; since the trace is an integer and √p is irrational, trace A = p + 1.

theorem chapter28.sum_eq_of_roots {ι : Type u_1} [Fintype ι] (μ : ι → ℝ) (p : ℕ) (hp : Irrational √↑p) (hcard : Fintype.card ι = p ^ 2 + p + 1) (hroot : ∀ (i : ι), (μ i - (↑p + 1)) * (μ i ^ 2 - ↑p) = 0) (hsq : ∑ i : ι, μ i ^ 2 = (↑p ^ 2 + ↑p + 1) * (↑p + 1)) (hint : ∃ (t : ℤ), ∑ i : ι, μ i = ↑t) : ∑ i : ι, μ i = ↑p + 1

The purely numerical part of the eigenvalue argument. If the real numbers μ i (i ranging over a set of size N = p² + p + 1) are all roots of (x − (p+1))(x² − p), their squares sum to N (p + 1) and their sum is an integer, then their sum is p + 1.

@[instance_reducible]

noncomputable instance chapter28.instFintypePG2 (p : ℕ) [hp : Fact (Nat.Prime p)] : Fintype (PG2 p)

Equations

• chapter28.instFintypePG2 p = Fintype.ofFinite (chapter28.PG2 p)

@[instance_reducible]

noncomputable instance chapter28.instDecidableEqPG2 (p : ℕ) [hp : Fact (Nat.Prime p)] : DecidableEq (PG2 p)

Equations

• chapter28.instDecidableEqPG2 p = Classical.decEq (chapter28.PG2 p)

noncomputable def chapter28.reimanMatrix (p : ℕ) [hp : Fact (Nat.Prime p)] : Matrix (PG2 p) (PG2 p) ℝ

The matrix A of the book: a_{vw} = 1 if ⟨v, w⟩ = 0 and 0 otherwise (rows and columns are indexed by the points of the projective plane).

Equations

• chapter28.reimanMatrix p v w = if Projectivization.orthogonal v w then 1 else 0

theorem chapter28.reimanMatrix_isHermitian (p : ℕ) [hp : Fact (Nat.Prime p)] : (reimanMatrix p).IsHermitian

theorem chapter28.reimanMatrix_row_sum (p : ℕ) [hp : Fact (Nat.Prime p)] (v : PG2 p) : ∑ w : PG2 p, reimanMatrix p v w = ↑p + 1

Fact 1: every row of A contains exactly p + 1 ones.

theorem chapter28.reimanMatrix_common (p : ℕ) [hp : Fact (Nat.Prime p)] {v w : PG2 p} (hvw : v ≠ w) : ∑ u : PG2 p, reimanMatrix p v u * reimanMatrix p u w = 1

Fact 2: two distinct rows have exactly one common 1.

theorem chapter28.reimanMatrix_sq (p : ℕ) [hp : Fact (Nat.Prime p)] : reimanMatrix p * reimanMatrix p = ↑p • 1 + Matrix.of fun (x x_1 : PG2 p) => 1

A² = p I + J.

theorem chapter28.reimanMatrix_mul_J (p : ℕ) [hp : Fact (Nat.Prime p)] : (reimanMatrix p * Matrix.of fun (x x_1 : PG2 p) => 1) = (↑p + 1) • Matrix.of fun (x x_1 : PG2 p) => 1

A J = (p + 1) J.

theorem chapter28.reimanMatrix_cubic (p : ℕ) [hp : Fact (Nat.Prime p)] : reimanMatrix p * (reimanMatrix p * reimanMatrix p) = (↑p + 1) • (reimanMatrix p * reimanMatrix p) + ↑p • reimanMatrix p - (↑p * (↑p + 1)) • 1

A satisfies (A − (p+1) I)(A² − p I) = 0.

theorem chapter28.reimanMatrix_eigenvalue_root (p : ℕ) [hp : Fact (Nat.Prime p)] (i : PG2 p) : (⋯.eigenvalues i - (↑p + 1)) * (⋯.eigenvalues i ^ 2 - ↑p) = 0

Every eigenvalue of A is p + 1, √p or −√p.

theorem chapter28.trace_mul_self_eq_sum_sq {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.IsHermitian) : (A * A).trace = ∑ i : n, hA.eigenvalues i ^ 2

For a real symmetric matrix, trace (A²) = ∑ λᵢ².

theorem chapter28.card_PG2 (p : ℕ) [hp : Fact (Nat.Prime p)] : Fintype.card (PG2 p) = p ^ 2 + p + 1

The number of vertices of Gp, as a Fintype.card.

theorem chapter28.reimanMatrix_trace (p : ℕ) [hp : Fact (Nat.Prime p)] : (reimanMatrix p).trace = ↑p + 1

The trace argument: trace A = p + 1.

theorem chapter28.card_selfOrthogonal (p : ℕ) [hp : Fact (Nat.Prime p)] : {v : PG2 p | Projectivization.orthogonal v v}.card = p + 1

Claim. Exactly p + 1 points of the projective plane lie on the conic x² + y² + z² = 0 (i.e. are self-orthogonal); these are the vertices of degree p.

theorem chapter28.reimanGraph_two_mul_card_edges (p : ℕ) [hp : Fact (Nat.Prime p)] [DecidableRel (reimanGraph p).Adj] : 2 * (reimanGraph p).edgeFinset.card = p * (p + 1) ^ 2

Edge count of Gp: 2 |E(Gp)| = p (p + 1)².

theorem chapter28.reimanGraph_card_edges (p : ℕ) [hp : Fact (Nat.Prime p)] [DecidableRel (reimanGraph p).Adj] : ↑(reimanGraph p).edgeFinset.card = (↑(Fintype.card (PG2 p)) - 1) / 4 * (1 + √(4 * ↑(Fintype.card (PG2 p)) - 3))

Edge count of Gp, book form: with n = p² + p + 1 vertices, |E(Gp)| = (n − 1)/4 · (1 + √(4n − 3)), which almost agrees with Reiman's bound (6).

theorem chapter28.card_solutions_conic (p : ℕ) [hp : Fact (Nat.Prime p)] : {v : Fin 3 → ZMod p | v ⬝ᵥ v = 0}.card = p ^ 2

The number of solutions of x² + y² + z² = 0 in 𝔽ₚ³ is exactly p².

===================== Part: Sperner =====================

Section 6 of Chapter 28: Sperner's lemma (combinatorial core)

We formalize the double-counting proof of Sperner's lemma for an abstract triangulation. A triangulation is given by a finite family of "small triangles" tri i (i ∈ T), each a set of three vertices. Colors are 0, 1, 2 (the book's 1, 2, 3).

The book's "partial dual graph" argument counts the incidences between small triangles and edges whose endpoints carry the colors 0 and 1 ("doors"). We represent a door by the ordered pair (u, v) with col u = 0 and col v = 1.

• Every edge lies in at most two small triangles (interior edges in two, boundary edges in one), and
• the number of boundary doors is odd,

then the number of tricolored triangles is odd (in particular, nonzero). We also prove the one-dimensional lemma used for the boundary: along a path whose endpoints have different colors there is an odd number of color changes.

def chapter28.Tricolored {V : Type u_2} (col : V → Fin 3) (t : Finset V) : Prop

A small triangle is tricolored if all three colors occur among its vertices.

Equations

• chapter28.Tricolored col t = ∀ (c : Fin 3), ∃ v ∈ t, col v = c

@[instance_reducible]

instance chapter28.instDecidableTricolored {V : Type u_2} (col : V → Fin 3) (t : Finset V) : Decidable (Tricolored col t)

Equations

• chapter28.instDecidableTricolored col t = id inferInstance

def chapter28.pairCount {ι : Type u_1} {V : Type u_2} [DecidableEq V] (T : Finset ι) (tri : ι → Finset V) (u v : V) : ℕ

The number of small triangles containing both u and v.

Equations

• chapter28.pairCount T tri u v = {i ∈ T | u ∈ tri i ∧ v ∈ tri i}.card

def chapter28.doorsIn {V : Type u_2} (col : V → Fin 3) (t : Finset V) : Finset (V × V)

The doors inside a given small triangle: pairs (u, v) of its vertices with col u = 0, col v = 1.

Equations

• chapter28.doorsIn col t = {x ∈ t ×ˢ t | col x.1 = 0 ∧ col x.2 = 1}

def chapter28.doorPairs {ι : Type u_1} {V : Type u_2} [DecidableEq V] (T : Finset ι) (tri : ι → Finset V) (col : V → Fin 3) : Finset (V × V)

All doors of the triangulation.

Equations

• chapter28.doorPairs T tri col = T.biUnion fun (i : ι) => chapter28.doorsIn col (tri i)

theorem chapter28.card_doorsIn_mod_two {V : Type u_2} (col : V → Fin 3) (t : Finset V) (ht : t.card = 3) : (doorsIn col t).card % 2 = if Tricolored col t then 1 else 0

In a single triangle, the number of doors is odd iff the triangle is tricolored.

theorem chapter28.sperner_odd {ι : Type u_1} {V : Type u_2} [DecidableEq V] (T : Finset ι) (tri : ι → Finset V) (col : V → Fin 3) (h3 : ∀ i ∈ T, (tri i).card = 3) (h2 : ∀ (u v : V), u ≠ v → pairCount T tri u v ≤ 2) (hB : Odd {x ∈ doorPairs T tri col | pairCount T tri x.1 x.2 = 1}.card) : Odd {i ∈ T | Tricolored col (tri i)}.card

Sperner's lemma (abstract double-counting form). If every edge lies in at most two small triangles and the number of doors lying in exactly one small triangle (the boundary doors) is odd, then the number of tricolored triangles is odd.

theorem chapter28.odd_card_color_changes (k : ℕ) (s : ℕ → Bool) (h : s 0 ≠ s k) : Odd {i ∈ Finset.range k | s i ≠ s (i + 1)}.card

The one-dimensional Sperner lemma. If a path of vertices 0, 1, …, k is colored with two colors and the endpoints have different colors, then the number of color changes along the path is odd.

===================== Part: SpernerGrid =====================

Sperner's lemma for the standard triangulation of a triangle

The big triangle V₁V₂V₃ is subdivided into k² small triangles. A vertex is a pair (a, b) of natural numbers with a + b ≤ k (barycentric coordinates (a, b, k − a − b) / k); V₁ = (k, 0), V₂ = (0, k), V₃ = (0, 0). The small triangles are the "upward" triangles {(a,b), (a+1,b), (a,b+1)} with a + b + 1 ≤ k and the "downward" triangles {(a+1,b), (a,b+1), (a+1,b+1)} with a + b + 2 ≤ k.

We verify the hypotheses of the abstract Sperner lemma sperner_odd for this triangulation: every edge lies in at most two small triangles, and for a Sperner coloring the boundary doors are exactly the color changes along the side V₁V₂, of which there is an odd number.

def chapter28.upTri (x : ℕ × ℕ) : Finset (ℕ × ℕ)

The upward small triangle with lower-left corner x.

Equations

• chapter28.upTri x = {x, (x.1 + 1, x.2), (x.1, x.2 + 1)}

def chapter28.downTri (x : ℕ × ℕ) : Finset (ℕ × ℕ)

The downward small triangle with "lower-left corner" x.

Equations

• chapter28.downTri x = {(x.1 + 1, x.2), (x.1, x.2 + 1), (x.1 + 1, x.2 + 1)}

def chapter28.gridUp (k : ℕ) : Finset (ℕ × ℕ)

Indices of upward small triangles.

Equations

• chapter28.gridUp k = {x ∈ Finset.range k ×ˢ Finset.range k | x.1 + x.2 + 1 ≤ k}

def chapter28.gridDown (k : ℕ) : Finset (ℕ × ℕ)

Indices of downward small triangles.

Equations

• chapter28.gridDown k = {x ∈ Finset.range k ×ˢ Finset.range k | x.1 + x.2 + 2 ≤ k}

def chapter28.gridT (k : ℕ) : Finset (ℕ × ℕ ⊕ ℕ × ℕ)

Index set of all small triangles of the k-th subdivision.

Equations

• chapter28.gridT k = (chapter28.gridUp k).disjSum (chapter28.gridDown k)

def chapter28.gridTri : ℕ × ℕ ⊕ ℕ × ℕ → Finset (ℕ × ℕ)

The small triangle with a given index.

Equations

• chapter28.gridTri = Sum.elim chapter28.upTri chapter28.downTri

theorem chapter28.mem_gridUp {k : ℕ} {x : ℕ × ℕ} : x ∈ gridUp k ↔ x.1 + x.2 + 1 ≤ k

theorem chapter28.mem_gridDown {k : ℕ} {x : ℕ × ℕ} : x ∈ gridDown k ↔ x.1 + x.2 + 2 ≤ k

theorem chapter28.mem_upTri {x y : ℕ × ℕ} : y ∈ upTri x ↔ y = x ∨ y = (x.1 + 1, x.2) ∨ y = (x.1, x.2 + 1)

theorem chapter28.mem_downTri {x y : ℕ × ℕ} : y ∈ downTri x ↔ y = (x.1 + 1, x.2) ∨ y = (x.1, x.2 + 1) ∨ y = (x.1 + 1, x.2 + 1)

theorem chapter28.card_upTri (x : ℕ × ℕ) : (upTri x).card = 3

theorem chapter28.card_downTri (x : ℕ × ℕ) : (downTri x).card = 3

theorem chapter28.card_gridTri {k : ℕ} (i : ℕ × ℕ ⊕ ℕ × ℕ) : i ∈ gridT k → (gridTri i).card = 3

theorem chapter28.upTri_unique {x u v : ℕ × ℕ} (huv : u ≠ v) (hu : u ∈ upTri x) (hv : v ∈ upTri x) : x = (min u.1 v.1, min u.2 v.2)

An upward triangle is determined by any two of its vertices: its corner is their componentwise minimum.

theorem chapter28.downTri_unique {x u v : ℕ × ℕ} (huv : u ≠ v) (hu : u ∈ downTri x) (hv : v ∈ downTri x) : (x.1 + 1, x.2 + 1) = (max u.1 v.1, max u.2 v.2)

A downward triangle is determined by any two of its vertices: its upper corner is their componentwise maximum.

theorem chapter28.pairCount_grid (k : ℕ) (u v : ℕ × ℕ) : pairCount (gridT k) gridTri u v = {x ∈ gridUp k | u ∈ upTri x ∧ v ∈ upTri x}.card + {x ∈ gridDown k | u ∈ downTri x ∧ v ∈ downTri x}.card

The number of small triangles containing u and v splits into upward and downward ones.

theorem chapter28.upCount_le_one (k : ℕ) {u v : ℕ × ℕ} (huv : u ≠ v) : {x ∈ gridUp k | u ∈ upTri x ∧ v ∈ upTri x}.card ≤ 1

theorem chapter28.downCount_le_one (k : ℕ) {u v : ℕ × ℕ} (huv : u ≠ v) : {x ∈ gridDown k | u ∈ downTri x ∧ v ∈ downTri x}.card ≤ 1

theorem chapter28.pairCount_grid_le_two (k : ℕ) (u v : ℕ × ℕ) (huv : u ≠ v) : pairCount (gridT k) gridTri u v ≤ 2

Every edge lies in at most two small triangles.

theorem chapter28.two_le_pairCount_grid {k : ℕ} {u v x y : ℕ × ℕ} (hx : x ∈ gridUp k) (hux : u ∈ upTri x) (hvx : v ∈ upTri x) (hy : y ∈ gridDown k) (huy : u ∈ downTri y) (hvy : v ∈ downTri y) : 2 ≤ pairCount (gridT k) gridTri u v

An edge lying in an upward and a downward triangle is interior: it lies in two triangles.

def chapter28.sideVertex (k i : ℕ) : ℕ × ℕ

The vertex number i on the side V₂V₁ (from V₂ = (0, k) to V₁ = (k, 0)).

Equations

• chapter28.sideVertex k i = (i, k - i)

def chapter28.sideColor (k : ℕ) (col : ℕ × ℕ → Fin 3) (i : ℕ) : Bool

Whether the i-th side vertex has color 0.

Equations

• chapter28.sideColor k col i = decide (col (chapter28.sideVertex k i) = 0)

def chapter28.sideDoor (k : ℕ) (col : ℕ × ℕ → Fin 3) (i : ℕ) : (ℕ × ℕ) × ℕ × ℕ

The door at position i of the side (if there is a color change there).

Equations

• chapter28.sideDoor k col i = if col (chapter28.sideVertex k i) = 0 then (chapter28.sideVertex k i, chapter28.sideVertex k (i + 1)) else (chapter28.sideVertex k (i + 1), chapter28.sideVertex k i)

structure chapter28.IsSpernerColoring (k : ℕ) (col : ℕ × ℕ → Fin 3) : Prop

A Sperner coloring of the k-th subdivision: vertices on the side opposite to Vᵢ do not get the color of Vᵢ. (Then Vᵢ gets color i, and the side VᵢVⱼ only uses colors i and j.)

• side_a (b : ℕ) : col (0, b) ≠ 0
• side_b (a : ℕ) : col (a, 0) ≠ 1
• side_c (a b : ℕ) : a + b = k → col (a, b) ≠ 2

theorem chapter28.boundary_doors_eq {k : ℕ} {col : ℕ × ℕ → Fin 3} (hcol : IsSpernerColoring k col) : {x ∈ doorPairs (gridT k) gridTri col | pairCount (gridT k) gridTri x.1 x.2 = 1} = Finset.image (sideDoor k col) ({i ∈ Finset.range k | sideColor k col i ≠ sideColor k col (i + 1)})

The boundary doors of a Sperner coloring are exactly the color changes along V₂V₁.

theorem chapter28.grid_sperner (k : ℕ) (col : ℕ × ℕ → Fin 3) (hcol : IsSpernerColoring k col) : Odd {i ∈ gridT k | Tricolored col (gridTri i)}.card

Sperner's lemma for the k-th standard subdivision of a triangle. For every Sperner coloring the number of tricolored small triangles is odd.

theorem chapter28.grid_sperner_exists (k : ℕ) (col : ℕ × ℕ → Fin 3) (hcol : IsSpernerColoring k col) : ∃ i ∈ gridT k, Tricolored col (gridTri i)

In particular, a tricolored small triangle exists.

===================== Part: Brouwer =====================

Brouwer's fixed point theorem in dimension 2, via Sperner's lemma

Following the book, we first prove that every continuous map f : Δ → Δ of the triangle Δ = conv{e₁, e₂, e₃} ⊆ ℝ³ has a fixed point: color a point v by the smallest index i with f(v)ᵢ < vᵢ, apply Sperner's lemma to finer and finer triangulations, and pass to a limit using compactness of Δ. Then we transfer the result to the disk B², which is homeomorphic to Δ.

def chapter28.HasFixedPointProperty {X : Type u_1} [TopologicalSpace X] (S : Set X) : Prop

The fixed point property of a set S: every continuous self-map of S has a fixed point.

Equations

• chapter28.HasFixedPointProperty S = ∀ (f : X → X), ContinuousOn f S → Set.MapsTo f S S → ∃ x ∈ S, f x = x

theorem chapter28.HasFixedPointProperty.transfer {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {S' : Set Y} (φ : X → Y) (ψ : Y → X) (hφ : ContinuousOn φ S) (hψ : ContinuousOn ψ S') (hφS : Set.MapsTo φ S S') (hψS : Set.MapsTo ψ S' S) (hφψ : ∀ y ∈ S', φ (ψ y) = y) (h : HasFixedPointProperty S) : HasFixedPointProperty S'

The fixed point property is inherited along a retraction-type pair of maps (in particular along homeomorphisms).

def chapter28.stdTriangle : Set (Fin 3 → ℝ)

The standard triangle Δ = {x ∈ ℝ³ | xᵢ ≥ 0, x₀ + x₁ + x₂ = 1}.

Equations

• chapter28.stdTriangle = {x : Fin 3 → ℝ | (∀ (i : Fin 3), 0 ≤ x i) ∧ ∑ i : Fin 3, x i = 1}

theorem chapter28.isClosed_stdTriangle : IsClosed stdTriangle

theorem chapter28.isCompact_stdTriangle : IsCompact stdTriangle

theorem chapter28.convex_stdTriangle : Convex ℝ stdTriangle

The coloring λ(v) = min {i : f(v)ᵢ < vᵢ}

noncomputable def chapter28.brouwerColor (f : (Fin 3 → ℝ) → Fin 3 → ℝ) (v : Fin 3 → ℝ) : Fin 3

The book's coloring: the smallest index i such that f(v)ᵢ < vᵢ (with 2 as default).

Equations

• chapter28.brouwerColor f v = if f v 0 < v 0 then 0 else if f v 1 < v 1 then 1 else 2

theorem chapter28.sum_fin_three (x : Fin 3 → ℝ) : ∑ i : Fin 3, x i = x 0 + x 1 + x 2

theorem chapter28.brouwerColor_spec {f : (Fin 3 → ℝ) → Fin 3 → ℝ} {v : Fin 3 → ℝ} (hv : v ∈ stdTriangle) (hfv : f v ∈ stdTriangle) (hne : f v ≠ v) : f v (brouwerColor f v) < v (brouwerColor f v)

If v is not a fixed point, then the i-th coordinate of f(v) − v is negative for the color i of v.

theorem chapter28.brouwerColor_ne_zero {f : (Fin 3 → ℝ) → Fin 3 → ℝ} {v : Fin 3 → ℝ} (hfv : f v ∈ stdTriangle) (h : v 0 = 0) : brouwerColor f v ≠ 0

theorem chapter28.brouwerColor_ne_one {f : (Fin 3 → ℝ) → Fin 3 → ℝ} {v : Fin 3 → ℝ} (hfv : f v ∈ stdTriangle) (h : v 1 = 0) : brouwerColor f v ≠ 1

theorem chapter28.brouwerColor_ne_two {f : (Fin 3 → ℝ) → Fin 3 → ℝ} {v : Fin 3 → ℝ} (hv : v ∈ stdTriangle) (hfv : f v ∈ stdTriangle) (hne : f v ≠ v) (h : v 2 = 0) : brouwerColor f v ≠ 2

Points of the k-th subdivision

noncomputable def chapter28.gridPoint (k : ℕ) (w : ℕ × ℕ) : Fin 3 → ℝ

The vertex (a, b) of the k-th subdivision, as a point (a/k, b/k, (k−a−b)/k) of Δ.

Equations

• chapter28.gridPoint k w = ![↑w.1 / ↑k, ↑w.2 / ↑k, (↑k - ↑w.1 - ↑w.2) / ↑k]

theorem chapter28.gridPoint_mem {k : ℕ} (hk : 0 < k) {w : ℕ × ℕ} (hw : w.1 + w.2 ≤ k) : gridPoint k w ∈ stdTriangle

theorem chapter28.tri_vertex_le {k : ℕ} {i : ℕ × ℕ ⊕ ℕ × ℕ} (hi : i ∈ gridT k) {w : ℕ × ℕ} (hw : w ∈ gridTri i) : w.1 + w.2 ≤ k

theorem chapter28.tri_vertex_close {i : ℕ × ℕ ⊕ ℕ × ℕ} {w w' : ℕ × ℕ} (hw : w ∈ gridTri i) (hw' : w' ∈ gridTri i) : w.1 ≤ w'.1 + 1 ∧ w.2 ≤ w'.2 + 1

theorem chapter28.gridPoint_dist_le {k : ℕ} (hk : 0 < k) {i : ℕ × ℕ ⊕ ℕ × ℕ} {w w' : ℕ × ℕ} (hw : w ∈ gridTri i) (hw' : w' ∈ gridTri i) : ‖gridPoint k w - gridPoint k w'‖ ≤ 2 / ↑k

Vertices of a small triangle of the k-th subdivision are at distance at most 2/k.

Brouwer's theorem for the triangle

theorem chapter28.brouwer_stdTriangle : HasFixedPointProperty stdTriangle

Brouwer's fixed point theorem for the triangle Δ. Every continuous map f : Δ → Δ has a fixed point.

Transfer to the disk B²

noncomputable def chapter28.simplexToPlane (x : Fin 3 → ℝ) : EuclideanSpace ℝ (Fin 2)

The affine map from Δ ⊆ ℝ³ to the plane.

Equations

• chapter28.simplexToPlane x = !₂[x 0 - 1 / 3, x 1 - 1 / 3]

noncomputable def chapter28.planeToSimplex (y : EuclideanSpace ℝ (Fin 2)) : Fin 3 → ℝ

Its inverse (barycentric coordinates).

Equations

• chapter28.planeToSimplex y = ![y.ofLp 0 + 1 / 3, y.ofLp 1 + 1 / 3, 1 / 3 - y.ofLp 0 - y.ofLp 1]

def chapter28.planeTriangle : Set (EuclideanSpace ℝ (Fin 2))

The triangle Δ, placed in the plane with its barycenter at the origin.

Equations

• chapter28.planeTriangle = chapter28.planeToSimplex ⁻¹' chapter28.stdTriangle

theorem chapter28.continuous_simplexToPlane : Continuous simplexToPlane

theorem chapter28.continuous_planeToSimplex : Continuous planeToSimplex

theorem chapter28.simplexToPlane_planeToSimplex (y : EuclideanSpace ℝ (Fin 2)) : simplexToPlane (planeToSimplex y) = y

theorem chapter28.planeToSimplex_simplexToPlane {x : Fin 3 → ℝ} (hx : x ∈ stdTriangle) : planeToSimplex (simplexToPlane x) = x

theorem chapter28.planeTriangle_fpp : HasFixedPointProperty planeTriangle

theorem chapter28.convex_planeTriangle : Convex ℝ planeTriangle

theorem chapter28.isClosed_planeTriangle : IsClosed planeTriangle

theorem chapter28.isBounded_planeTriangle : Bornology.IsBounded planeTriangle

theorem chapter28.interior_planeTriangle_nonempty : (interior planeTriangle).Nonempty

theorem chapter28.closedBall_fpp : HasFixedPointProperty (Metric.closedBall 0 1)

Brouwer's fixed point theorem for the disk, in fixed-point-property form: the closed unit disk B² ⊆ ℝ² has the fixed point property (since it is homeomorphic to Δ).

theorem chapter28.brouwer_fixed_point_2d (f : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)) (hf : Continuous f) (hB : ∀ (x : EuclideanSpace ℝ (Fin 2)), ‖x‖ ≤ 1 → ‖f x‖ ≤ 1) : ∃ (x : EuclideanSpace ℝ (Fin 2)), ‖x‖ ≤ 1 ∧ f x = x

Brouwer's fixed point theorem (n = 2). Every continuous map of the closed unit disk of ℝ² into itself has a fixed point.

theorem chapter28.brouwer_fixed_point_1d (f : ℝ → ℝ) (hf : ContinuousOn f (Set.Icc 0 1)) (hmaps : Set.MapsTo f (Set.Icc 0 1) (Set.Icc 0 1)) : ∃ x ∈ Set.Icc 0 1, f x = x

Brouwer's fixed point theorem (n = 1), from the intermediate value theorem.