Rational levels for the staircases

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 approximating inner functions (Lemma 2, properties a) and b), p. 269) are constant on each cell with a rational value, the values on distinct cells of one rank are distinct, and a value taken on a cell of rank i differs from every value taken on a cell of rank j ≠ i. Together with the rational independence of the λ_p (his Lemma 1′) this makes the cell map (q, j) ↦ ∑_p λ_p · (value on cell (q, j_p)) injective, which is what lets the outer function be prescribed cell by cell without conflict.

Here the levels are given by a closed formula rather than an inductive choice. With b̂_{q,j} the right endpoint of the cell (q, j) in t-coordinates, clamped into I, and integers N, M ≥ 1,

level φ N M q j = (m · (⌈(M · φ_q(b̂_{q,j}) - q) / m⌉ + j) + q) / M.

The numerator is ≡ q (mod m), so levels of different ranks differ; the + j makes the levels of one rank strictly increasing even where φ_q is flat; and the ceiling places the level in [φ_q(b̂_{q,j}), φ_q(b̂_{q,j}) + m (j + 1) / M), so that for M large the staircase with these levels is uniformly close to φ_q. Those are le_level, level_lt, level_strictMono, level_injective; the cell map's injectivity from LinearIndependent ℚ lam is cellMap_injective, the only place Layer 0 is used.

noncomputable def MiscMath.Analysis.KolmogorovArnold.cellEnd {m : ℕ} (N : ℕ) (q : Fin m) (j : ℕ) : ↑unitInterval

The right endpoint of the cell (q, j) in t-coordinates, (q + m j) / N, clamped into I.

Equations

• MiscMath.Analysis.KolmogorovArnold.cellEnd N q j = Set.projIcc 0 1 MiscMath.Analysis.KolmogorovArnold.cellEnd._proof_1 (MiscMath.Analysis.KolmogorovArnold.cellRight q j / ↑N)

theorem MiscMath.Analysis.KolmogorovArnold.coe_cellEnd {m : ℕ} (N : ℕ) (q : Fin m) (j : ℕ) : ↑(cellEnd N q j) = min 1 (cellRight q j / ↑N)

theorem MiscMath.Analysis.KolmogorovArnold.cellEnd_mono {m : ℕ} (N : ℕ) (q : Fin m) : Monotone (cellEnd N q)

noncomputable def MiscMath.Analysis.KolmogorovArnold.endValue {m : ℕ} (φ : Fin m → Inner) (N : ℕ) (q : Fin m) (j : ℕ) : ℝ

The value of the q-th inner function at the clamped right endpoint of the cell (q, j).

Equations

• MiscMath.Analysis.KolmogorovArnold.endValue φ N q j = ↑(φ q) (MiscMath.Analysis.KolmogorovArnold.cellEnd N q j)

theorem MiscMath.Analysis.KolmogorovArnold.endValue_mono {m : ℕ} (φ : Fin m → Inner) (N : ℕ) (q : Fin m) : Monotone (endValue φ N q)

noncomputable def MiscMath.Analysis.KolmogorovArnold.levelNum {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) (j : ℕ) : ℤ

The integer numerator of a level: m (⌈(M φ_q(b̂) - q) / m⌉ + j) + q.

Equations

• MiscMath.Analysis.KolmogorovArnold.levelNum φ N M q j = ↑m * (⌈(↑M * MiscMath.Analysis.KolmogorovArnold.endValue φ N q j - ↑↑q) / ↑m⌉ + ↑j) + ↑↑q

noncomputable def MiscMath.Analysis.KolmogorovArnold.level {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) (j : ℕ) : ℚ

The level of the staircase of rank q on its cell of index j, a rational.

Equations

• MiscMath.Analysis.KolmogorovArnold.level φ N M q j = ↑(MiscMath.Analysis.KolmogorovArnold.levelNum φ N M q j) / ↑M

theorem MiscMath.Analysis.KolmogorovArnold.level_cast {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) (j : ℕ) : ↑(level φ N M q j) = ↑(levelNum φ N M q j) / ↑M

theorem MiscMath.Analysis.KolmogorovArnold.levelNum_cast {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) (j : ℕ) : ↑(levelNum φ N M q j) = ↑m * (↑⌈(↑M * endValue φ N q j - ↑↑q) / ↑m⌉ + ↑j) + ↑↑q

theorem MiscMath.Analysis.KolmogorovArnold.le_level {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) (j : ℕ) : endValue φ N q j ≤ ↑(level φ N M q j)

The level lies at or above the value of φ_q at the clamped right endpoint of its cell.

theorem MiscMath.Analysis.KolmogorovArnold.level_lt {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) (j : ℕ) : ↑(level φ N M q j) < endValue φ N q j + ↑m * (↑j + 1) / ↑M

The level lies below φ_q(b̂) + m (j + 1) / M.

theorem MiscMath.Analysis.KolmogorovArnold.levelNum_lt_succ {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) (j : ℕ) : levelNum φ N M q j < levelNum φ N M q (j + 1)

Within one rank the numerators strictly increase with the cell index.

theorem MiscMath.Analysis.KolmogorovArnold.levelNum_strictMono {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) : StrictMono (levelNum φ N M q)

theorem MiscMath.Analysis.KolmogorovArnold.level_strictMono {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) : StrictMono (level φ N M q)

theorem MiscMath.Analysis.KolmogorovArnold.level_monotone {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) : Monotone (level φ N M q)

theorem MiscMath.Analysis.KolmogorovArnold.level_cast_monotone {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) : Monotone fun (j : ℕ) => ↑(level φ N M q j)

The real levels of one rank are monotone in the cell index.

theorem MiscMath.Analysis.KolmogorovArnold.levelNum_emod {m : ℕ} (φ : Fin m → Inner) (N M : ℕ) (q : Fin m) (j : ℕ) : levelNum φ N M q j % ↑m = ↑↑q

The numerator of a level of rank q is ≡ q (mod m).

theorem MiscMath.Analysis.KolmogorovArnold.level_injective {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) : Function.Injective fun (qj : Fin m × ℕ) => level φ N M qj.1 qj.2

Equal levels come from the same rank and the same cell index.

theorem MiscMath.Analysis.KolmogorovArnold.cellMap_injective {n : ℕ} {lam : Fin n → ℝ} (hlam : LinearIndependent ℚ lam) (φ : Fin (2 * n + 1) → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) : Function.Injective fun (qj : Fin (2 * n + 1) × (Fin n → ℕ)) => ∑ p : Fin n, lam p * ↑(level φ N M qj.1 (qj.2 p))

The cell map is injective (Hedberg, Lemma 1′ with properties a) and b)): for rationally independent λ, the value ∑_p λ_p · level(q, j_p) determines the rank q and the cell indices j. Stated for m = 2n + 1 ranks; the case n = 0 is covered because then there is a single rank.