The cell system

Support module for MiscMath.Analysis.KolmogorovArnold, where the theorem is stated and where the reader should start; part of the density argument (Layer 2 of the development). Its declarations are proof: machine-generated, kernel-checked and axiom-audited, and may be read by no one.

Hedberg's red intervals (Lemma 2, p. 269), in general dimension and on the rescaled line u = N t, so that every endpoint is an integer. There are m ranks q : Fin m (m = 2n + 1 in the application). Deleting from the line the open unit intervals (q + m j, q + m j + 1), j ∈ ℕ, leaves for each rank a sequence of closed cells of length m - 1,

cell q j = [q + m j - (m - 1), q + m j],

and the deleted intervals are the gaps of rank q. Two facts carry the whole argument:

• a point u lies in a gap of at most one rank, namely badRank u = ⌊u⌋ mod m, so every point u ≥ 0 lies in a cell of every other rank (badRank_eq_of_inGap, exists_mem_cell_of_not_inGap); Hedberg's "except perhaps for one value of i", Kahane's "sauf au plus une";
• hence a point of the n-dimensional cube lies in a product of cells — a red cube — of at least m - n ranks (le_card_red_add), which for m = 2n + 1 is n + 1: Hedberg's "at least three different ranks" for n = 2.

Also here: the index of a cell meeting [0, N] is at most N, which bounds the finite sums in the staircase construction, and the diameter bound for a cell.

def MiscMath.Analysis.KolmogorovArnold.cellRight {m : ℕ} (q : Fin m) (j : ℕ) : ℝ

The right endpoint q + m j of the cell of rank q and index j.

Equations

• MiscMath.Analysis.KolmogorovArnold.cellRight q j = ↑↑q + ↑m * ↑j

def MiscMath.Analysis.KolmogorovArnold.cellLeft {m : ℕ} (q : Fin m) (j : ℕ) : ℝ

The left endpoint q + m j - (m - 1) of the cell of rank q and index j.

Equations

• MiscMath.Analysis.KolmogorovArnold.cellLeft q j = ↑↑q + ↑m * ↑j - (↑m - 1)

def MiscMath.Analysis.KolmogorovArnold.cell {m : ℕ} (q : Fin m) (j : ℕ) : Set ℝ

The cell of rank q and index j: the closed interval [q + m j - (m - 1), q + m j].

Equations

• MiscMath.Analysis.KolmogorovArnold.cell q j = Set.Icc (MiscMath.Analysis.KolmogorovArnold.cellLeft q j) (MiscMath.Analysis.KolmogorovArnold.cellRight q j)

def MiscMath.Analysis.KolmogorovArnold.InGap {m : ℕ} (q : Fin m) (u : ℝ) : Prop

u lies in a gap of rank q: strictly between the right endpoint of some cell and the left endpoint of the next.

Equations

• MiscMath.Analysis.KolmogorovArnold.InGap q u = ∃ (j : ℕ), MiscMath.Analysis.KolmogorovArnold.cellRight q j < u ∧ u < MiscMath.Analysis.KolmogorovArnold.cellRight q j + 1

theorem MiscMath.Analysis.KolmogorovArnold.mem_cell {m : ℕ} {q : Fin m} {j : ℕ} {u : ℝ} : u ∈ cell q j ↔ cellLeft q j ≤ u ∧ u ≤ cellRight q j

theorem MiscMath.Analysis.KolmogorovArnold.one_le_cast_of_fin {m : ℕ} (q : Fin m) : 1 ≤ ↑m

theorem MiscMath.Analysis.KolmogorovArnold.cellLeft_succ {m : ℕ} (q : Fin m) (j : ℕ) : cellLeft q (j + 1) = cellRight q j + 1

theorem MiscMath.Analysis.KolmogorovArnold.cellLeft_le_cellRight {m : ℕ} (q : Fin m) (j : ℕ) : cellLeft q j ≤ cellRight q j

theorem MiscMath.Analysis.KolmogorovArnold.cellRight_nonneg {m : ℕ} (q : Fin m) (j : ℕ) : 0 ≤ cellRight q j

theorem MiscMath.Analysis.KolmogorovArnold.cellRight_mono {m : ℕ} (q : Fin m) : Monotone (cellRight q)

theorem MiscMath.Analysis.KolmogorovArnold.cellRight_add_one_le_cellLeft {m : ℕ} {q : Fin m} {j j' : ℕ} (h : j' < j) : cellRight q j' + 1 ≤ cellLeft q j

Cells of the same rank are separated by gaps of length one.

theorem MiscMath.Analysis.KolmogorovArnold.cellRight_mem_cell {m : ℕ} (q : Fin m) (j : ℕ) : cellRight q j ∈ cell q j

theorem MiscMath.Analysis.KolmogorovArnold.cellRight_add_one_mem_cell {m : ℕ} (q : Fin m) (j : ℕ) : cellRight q j + 1 ∈ cell q (j + 1)

theorem MiscMath.Analysis.KolmogorovArnold.abs_sub_le_of_mem_cell {m : ℕ} {q : Fin m} {j : ℕ} {u v : ℝ} (hu : u ∈ cell q j) (hv : v ∈ cell q j) : |u - v| ≤ ↑m - 1

Two points of one cell are at distance at most m - 1.

theorem MiscMath.Analysis.KolmogorovArnold.le_of_cellLeft_le {m : ℕ} {q : Fin m} {j N : ℕ} {u : ℝ} (h1 : cellLeft q j ≤ u) (h2 : u ≤ ↑N) : j ≤ N

A cell of index j that meets [0, N] has j ≤ N.

noncomputable def MiscMath.Analysis.KolmogorovArnold.badRank (m : ℕ) [NeZero m] (u : ℝ) : Fin m

The rank a point can be missed by: ⌊u⌋ mod m.

Equations

• MiscMath.Analysis.KolmogorovArnold.badRank m u = ⟨⌊u⌋₊ % m, ⋯⟩

theorem MiscMath.Analysis.KolmogorovArnold.badRank_eq_of_inGap {m : ℕ} [NeZero m] {q : Fin m} {u : ℝ} (h : InGap q u) : badRank m u = q

A gap of rank q forces ⌊u⌋ = q + m j, so the rank is ⌊u⌋ mod m: a point lies in a gap of at most one rank.

theorem MiscMath.Analysis.KolmogorovArnold.exists_mem_cell_of_not_inGap {m : ℕ} {q : Fin m} {u : ℝ} (hu : 0 ≤ u) (h : ¬InGap q u) : ∃ (j : ℕ), u ∈ cell q j

A point u ≥ 0 not in a gap of rank q lies in a cell of rank q.

Red cubes

def MiscMath.Analysis.KolmogorovArnold.IsRed {m n : ℕ} (q : Fin m) (u : Fin n → ℝ) : Prop

A point u of the rescaled cube is red for rank q if each coordinate lies in a cell of rank q, i.e. u lies in a product of cells of rank q.

Equations

• MiscMath.Analysis.KolmogorovArnold.IsRed q u = ∃ (jv : Fin n → ℕ), ∀ (p : Fin n), u p ∈ MiscMath.Analysis.KolmogorovArnold.cell q (jv p)

theorem MiscMath.Analysis.KolmogorovArnold.exists_badRank_eq_of_not_isRed {m n : ℕ} [NeZero m] {q : Fin m} {u : Fin n → ℝ} (hu : ∀ (p : Fin n), 0 ≤ u p) (h : ¬IsRed q u) : ∃ (p : Fin n), badRank m (u p) = q

A rank for which u is not red misses some coordinate, and so is that coordinate's bad rank.

theorem MiscMath.Analysis.KolmogorovArnold.exists_red_finset {m n : ℕ} [NeZero m] {u : Fin n → ℝ} (hu : ∀ (p : Fin n), 0 ≤ u p) : ∃ (S : Finset (Fin m)), (∀ q ∈ S, IsRed q u) ∧ m ≤ S.card + n

Covering multiplicity. A point of the n-cube with non-negative coordinates is red for at least m - n ranks: there is a set S of ranks, all red for u, with m ≤ #S + n. For m = 2n + 1 this is n + 1 ranks.

Sanity checks