bernstein_approximation_conjecture
Disprovedanalysisgraph-theory
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.
Preamble
import Mathlib
Formal statement
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
sorrySource