Iteration to an exact representation #
Support module for MiscMath.Analysis.KolmogorovArnold, where the theorem is stated and where
the reader should start; Layer 4 of the development. Its declarations are proof:
machine-generated, kernel-checked and axiom-audited, and may be read by no one.
Layer 3 produced a tuple ψ of strictly increasing inner functions with a one-step
approximation for every f: an outer g with ‖g‖ ≤ c ‖f‖ and residual
‖f - ∑_q g ∘ y_q‖ ≤ θ ‖f‖, θ < 1. Iterating on the residual gives outer functions g_j
with ‖g_j‖ ≤ c θ^j ‖f‖, whose sum converges in the Banach space of bounded continuous
functions on the line; the superposition operator is a bounded linear map, so it passes
through the sum, and the images telescope to f. Hence every continuous f on the cube
is a superposition ∑_q g ∘ y_q — exactly, not approximately — for the same universal ψ.
What this module proves #
Fix n and constants λ : Fin n → ℝ linearly independent over ℚ. There is a tuple
ψ = (ψ_0, …, ψ_{2n}) of continuous strictly increasing functions [0,1] → ℝ such that for
every continuous f : [0,1]ⁿ → ℝ there is a bounded continuous g : ℝ → ℝ with
f(x) = ∑_{q=0}^{2n} g(∑_{p} λ_p ψ_q(x_p)) for all x ∈ [0,1]ⁿ (exists_universal_tuple).
The inner functions are chosen before f and serve every f; only g depends on f.
The iteration itself is stated separately (exists_eq_superpose_of_step): any tuple with a
one-step approximation property with constants c ≥ 0, 0 ≤ θ < 1 represents every f
exactly.
Source #
T. Hedberg, The Kolmogorov superposition theorem, Appendix II to H. S. Shapiro, Topics in
Approximation Theory, Lecture Notes in Math. 187, Springer, 1971, proof of Theorem 1, pp.
271–272: f_0 = f, f_{j+1} = f_j - ∑_i g_j ∘ t_i with g_j from Lemma 3, so
‖f_j‖ ≤ (8/9)^j ‖f‖ and ‖g_j‖ ≤ (1/7)(8/9)^j ‖f‖; "the series ∑ g_j converges in norm to an
element g ∈ C(ℝ), and we have f = ∑ (f_j - f_{j+1}) = ∑_i g ∘ t_i". Kahane, J. Approx.
Theory 13 (1975), p. 231, runs the same induction with h_j = γ(f_j). Both are for the
n = 2 notation or general n verbatim; nothing changes here.
Sanity checks #
exists_universal_tuple has one hypothesis, satisfied by Layer 0's λ, so the example
below instantiates it at every n. The n = 0 case is recorded as well: the cube is a point,
the single inner sum is empty, and the theorem says that a constant is g(0) for some bounded
continuous g, which is true and content-free — the content starts at n = 1, and the theorem
is stated for all n so that no hypothesis needs to be checked for vacuity.
Relation to Mathlib #
Uses Summable.of_norm_bounded with the geometric series, ContinuousLinearMap.map_tsum,
Summable.hasSum_iff_tendsto_nat and the telescoping sum Finset.sum_range_sub'. Nothing
about superpositions is in Mathlib.
Iteration (Hedberg, proof of Theorem 1). A tuple with a one-step approximation for every
f, with ‖g‖ ≤ c ‖f‖ and residual at most θ ‖f‖ for a fixed θ < 1, represents every f
exactly: f = ∑_q g ∘ y_q for some bounded continuous g.
A universal tuple of inner functions, on the cube (Kolmogorov–Arnold, Lorentz–Sprecher
form, with inner functions on I and a bounded outer function). For λ linearly independent
over ℚ there is a tuple ψ of continuous strictly increasing ψ_q : I → ℝ such that every
continuous f on the cube is ∑_q g (∑_p λ_p ψ_q (x_p)) for some bounded continuous
g : ℝ → ℝ.
The pointwise form of exists_universal_tuple: the representation as an identity of
functions on the cube.