The superposition operator and the approximation sets #

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

Given constants λ_1, …, λ_n and a tuple ψ = (ψ_0, …, ψ_{2n}) of inner functions on I = [0, 1], the superposition of an outer function g : ℝ → ℝ is

x ↦ ∑_{q} g (∑_{p} λ_p ψ_q (x_p))

on the cube Iⁿ. The representation theorem says that for a suitable universal ψ every continuous f on the cube is such a superposition. The Baire-category proof (Hedberg 1971, Kahane 1975) gets there by considering, for one fixed f, the set of tuples ψ that admit a one-step approximation of f — an outer function g of norm at most δ with ‖f - ∑_q g ∘ y_q‖ < θ — and showing that this set is open and dense in the complete metric space of tuples. This module defines the operator and that set, and proves the openness. The density is Layer 2, and it is where all the work is.

What this module proves #

Fix n, constants λ : Fin n → ℝ, and a tuple ψ of 2n + 1 monotone continuous functions I → ℝ. Write y_q(x) = ∑_p λ_p ψ_q(x_p) for the inner sums, continuous on the cube.

superpose λ ψ is the linear operator g ↦ ∑_q g ∘ y_q from bounded continuous functions on ℝ to continuous functions on the cube; it has norm at most 2n + 1.
For a continuous f on the cube and reals δ, θ, the approximation set approxSet λ δ θ f consists of the tuples ψ for which some bounded continuous g with ‖g‖ ≤ δ has ‖f - superpose λ ψ g‖ < θ.
Theorem (isOpen_approxSet): approxSet λ δ θ f is open in the sup metric on tuples. Equivalently, if an outer function g works for ψ, it works for every tuple close enough to ψ.

The inner sums and the superposition depend continuously on the tuple ψ (continuous_innerSum, continuous_superpose), which is the whole content of the openness.

Source #

T. Hedberg, The Kolmogorov superposition theorem, Appendix II to H. S. Shapiro, Topics in Approximation Theory, Lecture Notes in Math. 187, Springer, 1971, pp. 267–275. The set U_f of his Lemma 2 (p. 269), for ‖f‖ = 1: the 5-tuples (φ_1, …, φ_5) for which some g ∈ C(ℝ) has |g(t)| ≤ 1/7 and |f(x, y) - ∑_i g(φ_i(x) + λ φ_i(y))| < 7/8. His openness argument is the single sentence "if g works for a particular 5-tuple, it does so for all sufficiently neighboring 5-tuples". Here the constants are parameters δ, θ, the dimension is general, and the inner functions are the factored λ_p ψ_q(x_p) of his Theorem 1.
J.-P. Kahane, Sur le théorème de superposition de Kolmogorov, J. Approx. Theory 13 (1975) 229–234. The set Ω(f) on p. 231, for f ≠ 0: the tuples for which some h ∈ C(I) satisfies his (6), namely ‖h‖ ≤ ‖f‖ and ‖f - ∑_q h(∑_p λ_p φ_q(x_p))‖ < (1 - ε)‖f‖; "visiblement Ω(f) est un ouvert". His bounds are relative to ‖f‖, ours absolute, which is why Layer 2 assumes ‖f‖ ≤ 1.

Sanity checks #

The examples below compute the definitions in the n = 1 case with the identity inner functions and λ = 1 — the inner sums are x ↦ x_0 and the superposition is 3 g(x_0) — and check the approximation sets at their edges: for f = 0 every tuple is in approxSet λ δ θ 0 as soon as 0 ≤ δ and 0 < θ (take g = 0), and approxSet λ δ θ f is empty when θ ≤ 0. The first says the definition is not vacuous; the second that the strict inequality is really there.

Relation to Mathlib #

The operator is a ContinuousLinearMap between Mathlib's Banach spaces ℝ →ᵇ ℝ (BoundedContinuousFunction) and C(Fin n → I, ℝ); the openness rests on ContinuousMap.continuous_postcomp and ContinuousMap.continuous_precomp from Topology/CompactOpen.lean, which apply because the sup-metric topology on C(K, ℝ) for compact K is the compact-open topology. Nothing about superpositions of this shape is in Mathlib.