Corollary 11.7.4 — Absolute-value approximation with zero constant term

Proved

LeblRA.absolute_value_polynomials

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

analysis

Let $a\ge0$ be real. There is a sequence of real polynomials satisfying

\forall n\in\mathbb N,\qquad p_n(0)=0,

and

\forall\varepsilon>0\;\exists N\;\forall n\ge N\;\forall x\in[-a,a], \qquad |p_n(x)-|x||<\varepsilon.

Thus absolute value can be approximated uniformly while requiring every approximant to have zero constant term. This normalization is the content of Lebl’s Corollary 11.7.4.

Formalization Note. The equation at zero holds at every index, including index zero, not merely in the limit. The value $a=0$ is allowed. No positivity, evenness, degree bound, or convergence outside the interval is imposed on the approximating polynomials.

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 absolute_value_polynomials (a : ℝ) (ha : 0 ≤ a) :
    ∃ p : ℕ → ℝ[X], (∀ n, (p n).eval 0 = 0) ∧
      TendstoUniformly (fun n (x : Set.Icc (-a) a) => (p n).eval (x : ℝ))
        (fun x : Set.Icc (-a) a => |(x : ℝ)|) atTop := by sorry
end LeblRA

Source

Jiří Lebl, Basic Analysis II, Section 11.7, Corollary 11.7.4. 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.absolute_value_polynomials

For every real number $a$ satisfying $0\le a$ , there exists a sequence $(p_n)_{n\in\mathbb N}$ of univariate polynomials with real coefficients such that $p_n(0)=0$ for every $n\in\mathbb N$ and such that, for every real $\varepsilon>0$ , there exists $N\in\mathbb N$ for which $|p_n(x)-|x||<\varepsilon$ for every $n\ge N$ and every real $x$ with $-a\le x\le a$ . The sequence is chosen for the given $a$ before the error tolerance is specified, and the same $N$ works for all points of the closed interval $[-a,a]$ , equipped with its inherited real topology. The indexing includes $n=0$ , and the equality at $0$ is required for every term, not merely for sufficiently large indices. The hypothesis allows $a=0$ , in which case the interval is the singleton $\{0\}$ and the approximation error there is exactly zero for every term because of the required equality; negative $a$ is outside the hypothesis. No degree bound, parity, coefficient sign restriction, convergence rate, uniqueness of the sequence, or approximation outside $[-a,a]$ 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