The Baire step: a generic tuple approximates every function in one step #
Support module for MiscMath.Analysis.KolmogorovArnold, where the theorem is stated and where
the reader should start; Layer 3 of the development. Its declarations are proof:
machine-generated, kernel-checked and axiom-audited, and may be read by no one.
Layer 1 made the approximation sets U_f open and Layer 2 made them dense, for every f in
the closed unit ball of C(Iⁿ, ℝ). That ball is separable, so the intersection of the U_h
over a countable dense set of h is a dense Gδ in the complete metric space of tuples
(Baire); so is the set of tuples with strictly increasing components (Layer 1), and two dense
Gδs meet. A tuple ψ in the intersection approximates every continuous f in one step,
with ‖g‖ and the error both proportional to ‖f‖: this is Hedberg's Lemma 3, and it is the
input to the iteration of Layer 4.
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] → ℝ, and
constants c ≥ 0 and 0 ≤ θ < 1, such that for every continuous f : [0,1]ⁿ → ℝ there is a
bounded continuous g : ℝ → ℝ with ‖g‖ ≤ c ‖f‖ and
sup_{x ∈ [0,1]ⁿ} |f(x) - ∑_q g(∑_p λ_p ψ_q(x_p))| ≤ θ ‖f‖ (exists_generic_tuple). The proof
gives c = 1/(2n+3) and θ = (8n+11)/(8n+12); at n = 2 these are Hedberg's 1/7 and
θ = 27/28, a weaker contraction than his 8/9: the one-step constant is taken as
(4n+5)/(4n+6) (13/14 at n = 2, against his 7/8), and half the remaining slack is spent
approximating f from the countable dense family, where he spends 1/72. Any θ < 1 drives
the iteration of Layer 4.
The tuple does not depend on f — that is the point — and it comes from a residual set, so
"quasi-every" tuple of monotone inner functions would do.
Source #
T. Hedberg, The Kolmogorov superposition theorem, Appendix II to H. S. Shapiro, Topics in
Approximation Theory, Lecture Notes in Math. 187, Springer, 1971, Lemma 3, p. 271: "there exist
φ_1, …, φ_5 ∈ C(I) such that, given f ∈ C(I²), there exists g ∈ C(ℝ) satisfying
|g(t)| ≤ (1/7)‖f‖ and ‖f - ∑_i g ∘ t_i‖ ≤ (8/9)‖f‖", proved by intersecting the U_{h_j}
over a sequence (h_j) dense in the unit sphere of C(I²) and appealing to Baire's theorem.
The strict monotonicity of the components is Kahane's remark (J. Approx. Theory 13 (1975),
p. 231), imported from StrictlyIncreasing.lean through Dense.inter_of_Gδ; Hedberg's Remark 2
(p. 272) obtains non-decreasing components by running the same argument in the closed subspace
H, which is where Inner lives from the outset.
Sanity checks #
The theorem has one hypothesis, the rational independence of λ, and Layer 0 supplies a
witness (exists_pos_linearIndependent_rat), so the example below instantiates the theorem
at every n. A second example records the countable dense subset of the closed unit ball
that the proof intersects over, since separability of C(Iⁿ, ℝ) is what makes the Baire
family countable.
Relation to Mathlib #
Uses BaireSpace for the complete metric space of tuples (through dense_biInter_of_isOpen),
Dense.inter_of_Gδ, and ContinuousMap.instSecondCountableTopology for separability of
C(Iⁿ, ℝ). Nothing about superpositions is in Mathlib.
The closed unit ball of C(Iⁿ, ℝ) has a countable subset dense in it.
A generic tuple approximates every f in one step (Hedberg, Lemma 3). For λ linearly
independent over ℚ there are a tuple ψ of continuous strictly increasing inner functions
and constants c ≥ 0, 0 ≤ θ < 1, such that every continuous f on the cube has an outer
g with ‖g‖ ≤ c ‖f‖ and ‖f - ∑_q g ∘ y_q‖ ≤ θ ‖f‖.