Approximation theory

Approximation and interpolation of functions: Chebyshev equioscillation, best approximation, Lagrange interpolation, Bernstein polynomials and Voronovskaya, Korovkin, Müntz–Szász, Runge, Kolmogorov superposition, universal approximation.

• Bernstein polynomials
• Best approximation in normed spaces
• Chebyshev equioscillation theorem
• Kolmogorov superposition theorem
• Korovkin's theorem
• Lagrange interpolation
• Uniform approximation by partial sums of one power series

TheoremMüntz–Szász theorem for integer exponents#✓fully proved

Let \(\Lambda : \mathbb{N} \to \mathbb{N}\) be strictly increasing with \(\Lambda(0) = 0\). The real linear span of the monomials \(x \mapsto x^{\Lambda(n)}\), \(n \in \mathbb{N}\), restricted to \([0, 1]\), is dense in \(C([0, 1], \mathbb{R})\) with the uniform norm if and only if the series \(\sum_{n \ge 0} 1/\Lambda(n+1)\) diverges, that is, the sequence \((1/\Lambda(n+1))_{n \in \mathbb{N}}\) is not summable.

public theorem muntz_szasz_nat
    (Λ : ℕ → ℕ)
    (hΛ_strict : StrictMono Λ)
    (hΛ_zero : Λ 0 = 0) :
    (Submodule.span ℝ (Set.range (fun n : ℕ =>
        ((Polynomial.X : Polynomial ℝ) ^ Λ n).toContinuousMapOn I))).topologicalClosure = ⊤
    ↔ ¬Summable (fun n : ℕ => ((Λ (n + 1) : ℝ)⁻¹))

Sources

• C. Müntz, Festschrift H. A. Schwarz 1914 303-312 and O. Szász, Math. Ann. 77 (1916) 482-496, Müntz-Szász theorem; Rudin Real & Complex; Lean states integer-exponent ℕ→ℕ StrictMono with 0∈range case as closure = ⊤ iff non-summable reciprocals.

TheoremRunge's theorem#●ready to prove

Let \(K \subseteq \mathbb{C}\) be compact, let \(U \subseteq \mathbb{C}\) be open with \(K \subseteq U\), and let \(f : \mathbb{C} \to \mathbb{C}\) be analytic at every point of \(U\). Then for every real \(\varepsilon > 0\) there are complex polynomials \(p\) and \(q\) such that \(q(z) \ne 0\) for every \(z \in K\) and \(|f(z) - p(z)/q(z)| < \varepsilon\) for every \(z \in K\).

public theorem_wanted runge (K : Set ℂ) (_hK : IsCompact K) (U : Set ℂ) (_hU : IsOpen U)
    (_hKU : K ⊆ U) (f : ℂ → ℂ) (_hf : AnalyticOnNhd ℂ f U)
    (ε : ℝ) (_hε : 0 < ε) :
    ∃ p q : ℂ[X], (∀ z ∈ K, q.eval z ≠ 0) ∧
      (∀ z ∈ K, ‖f z - p.eval z / q.eval z‖ < ε)

Sources

• C. Runge, Zur Theorie der eindeutigen analytischen Funktionen, Acta Math. 6 (1885), 229-244. Listed as §64 (additional statement 3) in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem runge_theorem of the lean-eval benchmark.

TheoremUniversal approximation theorem#✓fully proved

Let \(n\) be a natural number, let \(\mathbb{R}^n\) carry its standard inner product \(\langle \cdot, \cdot \rangle\), let \(K \subseteq \mathbb{R}^n\) be compact, and let \(\sigma : \mathbb{R} \to \mathbb{R}\) be continuous and not a polynomial, that is, there is no real polynomial \(p\) with \(\sigma(x) = p(x)\) for all real \(x\). Then for every function \(f : \mathbb{R}^n \to \mathbb{R}\) that is continuous on \(K\) and every \(\varepsilon > 0\) there exist \(m \in \mathbb{N}\), real numbers \(c_1, \dots, c_m\) and \(b_1, \dots, b_m\), and vectors \(w_1, \dots, w_m \in \mathbb{R}^n\) such that \(\left| f(x) - \sum_{i=1}^{m} c_i \, \sigma(\langle w_i, x \rangle + b_i) \right| < \varepsilon\) for every \(x \in K\).

In words: single-hidden-layer feedforward networks with a continuous, non-polynomial activation approximate every continuous function uniformly on every compact set.

theorem universal_approximation :
    ∀ {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))} (_hK : IsCompact K)
      {σ : ℝ → ℝ} (_hσ : Continuous σ)
      (_hnp : ¬ ∃ p : Polynomial ℝ, ∀ x, σ x = p.eval x)
      {f : EuclideanSpace ℝ (Fin n) → ℝ} (_hf : ContinuousOn f K)
      {ε : ℝ} (_hε : 0 < ε),
      ∃ (m : ℕ) (c : Fin m → ℝ) (W : Fin m → EuclideanSpace ℝ (Fin n))
        (b : Fin m → ℝ),
        ∀ x ∈ K, |f x - ∑ i, c i * σ (@inner ℝ _ _ (W i) x + b i)| < ε

Sources

• universal-approximation-s1 from https://en.wikipedia.org/wiki/Universal_approximation_theorem; the continuous-activation case of M. Leshno, V. Ya. Lin, A. Pinkus and S. Schocken, Multilayer feedforward networks with a nonpolynomial activation function can approximate any function, Neural Networks 6(6) (1993), 861–867, doi:10.1016/S0893-6080(05)80131-5, which allows any locally bounded, piecewise continuous activation that is not almost everywhere equal to a polynomial; for continuous activations this is the same as the pointwise non-polynomial hypothesis.

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.