Kolmogorov superposition theorem
TheoremKolmogorov superposition theorem#✓fully proved
Let \(n \ge 2\). There are continuous functions \(\psi_{q,p} : [0,1] \to \mathbb{R}\) for \(0 \le q \le 2n\) and \(0 \le p < n\), depending only on \(n\), such that for every continuous function \(f : [0,1]^n \to \mathbb{R}\) there are continuous functions \(\varphi_q : \mathbb{R} \to \mathbb{R}\) for \(0 \le q \le 2n\) with \(f(x) = \sum_{q=0}^{2n} \varphi_q\left(\sum_{p=0}^{n-1} \psi_{q,p}(x_p)\right)\) for every \(x = (x_0, \dots, x_{n-1}) \in [0,1]^n\).
theorem kolmogorov_superposition
{n : ℕ} (hn : 2 ≤ n) :
∃ (ψ : Fin (2 * n + 1) → Fin n → C(Set.Icc (0 : ℝ) 1, ℝ)),
∀ (f : C(Fin n → Set.Icc (0 : ℝ) 1, ℝ)),
∃ (φ : Fin (2 * n + 1) → C(ℝ, ℝ)),
∀ (x : Fin n → Set.Icc (0 : ℝ) 1),
f x = ∑ q : Fin (2 * n + 1), φ q (∑ p : Fin n, ψ q p (x p))
Sources
- Kolmogorov superposition theorem, A. N. Kolmogorov, Dokl. Akad. Nauk SSSR 114 (1957) 953–956, refined Arnold 1957; see Braun–Griebel, Acta Numer. 2009 review; Lean is n ≥ 2 exact cardinal Fin (2n+1) with inner ψ in C(Icc 0 1, ℝ) independent of f and outer φ in C(ℝ, ℝ), compact-source specialization [0, 1]^n as Fin n → Icc.
TheoremKolmogorov–Arnold superposition with a single outer function#●ready to prove
Let \(n \ge 1\) and let \(f : \mathbb{R}^n \to \mathbb{R}\) be continuous on the unit cube \([0, 1]^n\). Then there exist a continuous function \(g : \mathbb{R} \to \mathbb{R}\) and continuous functions \(\varphi_{k,l} : \mathbb{R} \to \mathbb{R}\) for \(0 \le k \le 2n\) and \(0 \le l < n\) such that for every \(x = (x_0, \dots, x_{n-1}) \in [0, 1]^n\),
Both \(g\) and the \(\varphi_{k,l}\) may depend on \(f\), so this is weaker than the form in which the inner functions are universal.
public theorem_wanted kolmogorov_arnold (n : ℕ) (_hn : 1 ≤ n)
(f : (Fin n → ℝ) → ℝ) (_hf : ContinuousOn f (Set.Icc 0 1)) :
∃ (g : ℝ → ℝ) (φ : Fin (2 * n + 1) → Fin n → ℝ → ℝ),
Continuous g ∧ (∀ k l, Continuous (φ k l)) ∧
∀ x ∈ Set.Icc (0 : Fin n → ℝ) 1,
f x = ∑ k, g (∑ l, φ k l (x l))
Sources
- A. N. Kolmogorov, On the representation of continuous functions of several variables by superposition of continuous functions of one variable and addition, Doklady Akad. Nauk SSSR 114 (1957), 953-956. V. I. Arnold, On functions of three variables, Doklady Akad. Nauk SSSR 114 (1957), 679-681. G. G. Lorentz, Metric entropy, widths, and superpositions of functions, Amer. Math. Monthly 69 (1962), 469-485 (single-outer-function refinement). Listed as §80 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem
kolmogorov_arnold_superpositionof the lean-eval benchmark.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.