Density of the approximation sets #
Support module for MiscMath.Analysis.KolmogorovArnold, where the theorem is stated and where
the reader should start; Layer 2 of the development, the crux of the Baire-category proof. Its
declarations are proof: machine-generated, kernel-checked and axiom-audited, and may be read by
no one.
For a continuous f on the cube with ‖f‖ ≤ 1, the set approxSet lam δ θ f of tuples of inner
functions admitting a one-step approximation of f — an outer g with ‖g‖ ≤ δ and
‖f - ∑_q g ∘ y_q‖ < θ — is dense in the space of tuples, for δ = 1/(2n+3) and any
θ > (2n+2)/(2n+3). Together with its openness (Layer 1) this is Hedberg's Lemma 2 in general
dimension, and it is the only place where the geometry of the cube enters the proof.
The proof, following Hedberg (pp. 269–271) with Kahane's general-n interval system:
- Given a tuple
ψ₀andε > 0, chooseNso that(2n+1)/Nis below a modulus of continuity offatδand of theψ₀_qatε/4, thenMlarge in terms ofN. The approximant tupleψ(Approximant.lean) is withinεofψ₀and is constant, with a rational level, on every cell of its rank. - On a red cube
a— a product of cells of one rank — every inner sumy_qofψis constant, equal to the cell-map valuecellMap a, and the cell map is injective by the rational independence of theλ_p(Levels.lean; the only use of Layer 0). - Define
gon the finitely many cell-map values asδ · sign(f on the cube)and extend to a bounded continuous function onℝof the same norm by Tietze. - Each point
xof the cube lies in red cubes of at leastn + 1of the2n + 1ranks (Cells.lean), and on those the summandg(y_q(x))isδwhenf(x) > δ,-δwhenf(x) < -δ, because a red cube has diameter below the modulus off; the remaining at mostnsummands are bounded byδ. This gives|f(x) - ∑_q g(y_q(x))| ≤ max(1 - δ, (2n+2)δ) = (2n+2)/(2n+3) < θ.
What this module proves #
Fix n and constants λ : Fin n → ℝ linearly independent over ℚ. For every continuous
f : [0,1]ⁿ → ℝ with ‖f‖ ≤ 1 and every θ > (2n+2)/(2n+3), the set of (2n+1)-tuples of
monotone continuous functions ψ_q : [0,1] → ℝ for which some bounded continuous g : ℝ → ℝ
with ‖g‖ ≤ 1/(2n+3) satisfies sup_{x ∈ [0,1]ⁿ} |f(x) - ∑_{q} g(∑_p λ_p ψ_q(x_p))| < θ is
dense in the space of all such tuples, with respect to uniform convergence in every component
(dense_approxSet).
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 2, pp. 269–271: for
n = 2,‖f‖ = 1,δ = 1/7,θ = 7/8, with red intervals of rankiobtained by deleting[s/N, (s+1)/N]fors ≡ i - 1 (mod 5), approximants constant with rational values on them (properties a)–c)),g = ±1/7on the red rectangles wherefhas a sign, and the count "at least three of the numbersg(t_i(x,y))are equal to1/7". The general-nconstants here,δ = 1/(2n+3)andθ > (2n+2)/(2n+3), reduce to his atn = 2(6/7 < 7/8). His Lemma 1′ (rational independence of theλ_i) is Layer 0. - J.-P. Kahane, Sur le théorème de superposition de Kolmogorov, J. Approx. Theory 13 (1975)
229–234, pp. 231–232: the interval system
I_q(j) = [qδ + (2n+1)jδ, qδ + (2n+1)jδ + 2nδ]for generaln, the observation that every point ofIⁿlies in a cubeP_qfor at leastn + 1values ofq, and the constraintε < 1/(2(n+1)). Kahane setsh = 2ε · (mean of f)on a cube and works in the increasing spaceΦfrom the outset; heregtakes the values±δ, 0as in Hedberg, and the space isInner(monotone, unnormalised).
Sanity checks #
The theorem has hypotheses, so it needs a satisfiability witness: the examples below exhibit
λ from Layer 0 (exists_pos_linearIndependent_rat), a function with ‖f‖ ≤ 1 (the zero
function, and the first coordinate at n = 1), and a θ above the threshold, so that the
hypotheses hold simultaneously; they also check the threshold at n = 2 is Hedberg's 6/7. The
conclusion is a density statement, so it is non-vacuous as soon as the tuple space is non-empty,
which it is (Inner.id).
Relation to Mathlib #
Uses Tietze's theorem in the form
BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding, Metric.dense_iff,
uniform continuity on compact spaces
(CompactSpace.uniformContinuous_of_continuous), and Fintype.linearIndependent_iff through
Levels.lean. Nothing about superpositions is in Mathlib.
Indices of the red cubes with cell indices at most N: a rank and, for each coordinate, a
cell index.
Equations
Instances For
The red cube with index a: the points of the cube each of whose rescaled coordinates
N x_p lies in the cell of rank a.1 and index a.2 p.
Equations
- MiscMath.Analysis.KolmogorovArnold.redCube N a = {y : Fin n → ↑unitInterval | ∀ (p : Fin n), ↑N * ↑(y p) ∈ MiscMath.Analysis.KolmogorovArnold.cell a.1 ↑(a.2 p)}
Instances For
The cell map: the value of the inner sum of rank a.1 of the approximant tuple on the red
cube a, namely ∑_p λ_p · level(a.1, a.2 p).
Equations
- MiscMath.Analysis.KolmogorovArnold.cellMap lam φ N M a = ∑ p : Fin n, lam p * MiscMath.Analysis.KolmogorovArnold.levels φ N M a.1 ↑(a.2 p)
Instances For
The sign of f on the red cube a: 1 if f > 0 throughout, -1 if f < 0 throughout,
and 0 otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The arithmetic of Hedberg's estimate, abstracted: with (2n+3) δ = 1, |a| ≤ 1,
|s| ≤ (2n+1) δ, and s on the side of δ when a is beyond δ, one has
|a - s| ≤ 1 - δ.
The approximation sets are dense (Hedberg, Lemma 2; Kahane, pp. 231–232). For λ
linearly independent over ℚ, ‖f‖ ≤ 1 and θ > (2n+2)/(2n+3), the tuples admitting a
one-step approximation of f with ‖g‖ ≤ 1/(2n+3) and error below θ are dense in
InnerTuple n.