bernstein_approximation_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Bernstein's approximation problem: What is the exact rate at which continuous periodic functions can be approximated by trigonometric polynomials of degree n? The Bernstein inequality gives a rate; exact constants for specific function classes are open.

Why this node was retired

The posted statement is

import Mathlib

theorem bernstein_approximation_conjecture (n : ℕ) (hn : 1 ≤ n)
    (f : ℝ → ℝ) (hf : Continuous f) (hperiod : ∀ x, f (x + 1) = f x) :
    ∀ eps : ℝ, 0 < eps →
    ∃ (p : Polynomial ℝ) (_ : p.natDegree ≤ n),
      ∀ x : ℝ, |f x - p.eval x| ≤
        (Finset.range n).sup (fun k =>
          (Finset.range n).sup (fun l =>
            if k ≠ l then
              (|f (k / n : ℝ) - f (l / n : ℝ)| / (k + l : ℝ) + eps).toNNReal else 0)) := by
  sorry

At n=1 the supremum over distinct grid indices is empty and the proposed error bound is zero, requiring every periodic continuous function to be affine. Also approximation is demanded on all ℝ by an algebraic polynomial.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

For periodic continuous f, use trigonometric polynomials and a genuine modulus-of-continuity error bound; or restrict algebraic-polynomial approximation to a compact interval and quantify degree sufficiently large for ε. The posted discrete all-real bound is not repaired by merely changing n≥1 to n≥2.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.