The approximating tuple of inner functions

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.

Given a tuple φ of inner functions and integers N, M ≥ 1, the approximant of rank q is the staircase of rank q on the u = N t line whose levels are the rational level φ N M q j of Levels.lean. This is the tuple (φ_1, …, φ_{2n+1}) of Hedberg's Lemma 2 (p. 269): constant with a rational value on every cell of its rank, distinct values across cells and ranks, and — the content of this module — uniformly within ε of φ_q once N exceeds the modulus of continuity of the φ_q and M is large in terms of N (abs_approximant_sub_lt, dist_approximant_lt). The value taken on a cell is approximant_apply_of_mem_cell.

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

The real levels of rank q: j ↦ level φ N M q j, cast to ℝ.

Equations

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

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

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

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

noncomputable def MiscMath.Analysis.KolmogorovArnold.approximant {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) : Inner

The approximant of rank q: the staircase of rank q with the levels of φ, rescaled to I, with N + 1 ramps (enough for every cell meeting [0, N]).

Equations

• MiscMath.Analysis.KolmogorovArnold.approximant φ N hM q = MiscMath.Analysis.KolmogorovArnold.stairInner N q ⋯ (N + 1)

theorem MiscMath.Analysis.KolmogorovArnold.approximant_apply {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) (t : ↑unitInterval) : ↑(approximant φ N hM q) t = stair q (levels φ N M q) (N + 1) (↑N * ↑t)

theorem MiscMath.Analysis.KolmogorovArnold.approximant_apply_of_mem_cell {m : ℕ} (φ : Fin m → Inner) (N : ℕ) {M : ℕ} (hM : 0 < M) (q : Fin m) {j : ℕ} (hj : j ≤ N + 1) {t : ↑unitInterval} (ht : ↑N * ↑t ∈ cell q j) : ↑(approximant φ N hM q) t = levels φ N M q j

On a cell of rank q and index j ≤ N + 1, the approximant takes the level of that cell.

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

theorem MiscMath.Analysis.KolmogorovArnold.abs_approximant_sub_lt {m : ℕ} (φ : Fin m → Inner) {N M : ℕ} (hN : 0 < N) (hM : 0 < M) {ε η : ℝ} (hη : ∀ (q : Fin m) (s t : ↑unitInterval), |↑s - ↑t| < η → |↑(φ q) s - ↑(φ q) t| < ε / 4) (hNη : ↑m / ↑N < η) (hMε : ↑m * (↑N + 2) / ↑M ≤ ε / 4) (q : Fin m) (t : ↑unitInterval) : |↑(approximant φ N hM q) t - ↑(φ q) t| < ε / 2

The approximant is uniformly close to φ_q. If η is a modulus of continuity of every φ_q at ε / 4, m / N < η and m (N + 2) / M ≤ ε / 4, then the approximant of rank q is within ε / 2 of φ_q at every point of I.

theorem MiscMath.Analysis.KolmogorovArnold.dist_approximant_lt {n : ℕ} (φ : InnerTuple n) {N M : ℕ} (hN : 0 < N) (hM : 0 < M) {ε η : ℝ} (hε : 0 < ε) (hη : ∀ (q : Fin (2 * n + 1)) (s t : ↑unitInterval), |↑s - ↑t| < η → |↑(φ q) s - ↑(φ q) t| < ε / 4) (hNη : ↑(2 * n + 1) / ↑N < η) (hMε : ↑(2 * n + 1) * (↑N + 2) / ↑M ≤ ε / 4) : dist (fun (q : Fin (2 * n + 1)) => approximant φ N hM q) φ < ε

The approximant tuple is within ε of φ in the sup metric on tuples, under the same hypotheses. Stated for m = 2n + 1 ranks, where the tuple type is InnerTuple n.