Theorem 11.7.1 — Uniform polynomial approximation on a compact interval

Proved

LeblRA.polynomial_approximation

by wamlart · Sep 6, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysis

Let $a,b\in\mathbb R$ . Both of the following assertions hold.

For every continuous function $f:[a,b]\to\mathbb C$ , there is a sequence of complex-coefficient polynomials converging uniformly to $f$ .
For every continuous function $f:[a,b]\to\mathbb R$ , there is a sequence of real-coefficient polynomials converging uniformly to $f$ .

For the corresponding scalar field $K$ , the conclusion is

\exists(p_n)_{n\in\mathbb N}\subseteq K[t]\quad \forall\varepsilon>0\;\exists N\;\forall n\ge N\;\forall x\in[a,b], \qquad |p_n(x)-f(x)|<\varepsilon.

This is the complete real/complex polynomial-approximation statement of Lebl’s Theorem 11.7.1, with the coefficient-field clause retained.

Formalization Note. The function is defined on the interval itself. A complex polynomial is evaluated at the complex embedding of the real argument. Arbitrary endpoints are allowed, so singleton and empty intervals are included. There is no degree bound, rate, or power-series assertion.

Preamble

import Mathlib.Topology.ContinuousMap.StoneWeierstrass
import Mathlib.Topology.Algebra.NonUnitalAlgebra
import Mathlib.Analysis.Complex.Basic

set_option autoImplicit false
open Set Filter Topology
open scoped ContinuousMapZero
open scoped Polynomial

Formal statement

namespace LeblRA
theorem polynomial_approximation (a b : ℝ) :
    (∀ f : C(Set.Icc a b, ℂ), ∃ p : ℕ → ℂ[X],
      TendstoUniformly (fun n (x : Set.Icc a b) => (p n).eval ((x : ℝ) : ℂ)) f atTop) ∧
    (∀ f : C(Set.Icc a b, ℝ), ∃ p : ℕ → ℝ[X],
      TendstoUniformly (fun n (x : Set.Icc a b) => (p n).eval (x : ℝ)) f atTop) := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II, Section 11.7, Theorem 11.7.1. Author-hosted HTML: https://www.jirka.org/ra/html/sec_stoneweier.html (accessed 2026-09-05). The algebra conventions are Definitions 11.7.5, 11.7.7, and 11.7.15; no unit is assumed.

Read-back

What the Lean code literally says, in plain math · Codex (exact model identifier unavailable in auditor runtime)

Declaration: LeblRA.polynomial_approximation

For every pair of real numbers $a,b$ , let $I=\{x\in\mathbb R:a\le x\le b\}$ with the topology inherited from $\mathbb R$ . Both of the following assertions hold: for every continuous function $f:I\to\mathbb C$ , there exists a sequence $(p_n)_{n\in\mathbb N}$ of univariate polynomials with complex coefficients such that, for every real $\varepsilon>0$ , there exists $N\in\mathbb N$ for which $|p_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x\in I$ , where the real number $x$ is embedded in $\mathbb C$ before polynomial evaluation and the absolute value is the complex modulus; and for every continuous function $f:I\to\mathbb R$ , there exists a sequence $(p_n)_{n\in\mathbb N}$ of univariate polynomials with real coefficients such that, for every real $\varepsilon>0$ , there exists $N\in\mathbb N$ for which $|p_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x\in I$ . The two existential sequences are separate and may depend on the function and the endpoints; in each assertion the sequence is chosen before $\varepsilon$ , and $N$ is independent of $x$ . Here $\mathbb N$ includes $0$ . There is no hypothesis that $a\le b$ : if $a>b$ , the interval is empty and the inequalities over its points are vacuous; if $a=b$ , approximation concerns the single point $a$ . No degree bound, convergence rate, uniqueness, or approximation outside $I$ is asserted.

Readback model identifier: unavailable; no actual runtime model identifier was supplied to this auditor.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by wamlart · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph