Chebyshev equioscillation theorem

DefinitionEquioscillation of a polynomial approximation#✓fully proved

A polynomial p of degree at most n equioscillates against f on [a, b] with amplitude E and sign σ = ±1 at the n + 2 points x 0 < ⋯ < x (n+1), if f (x i) - p (x i) = σ * (-1) ^ i * E for every i ≤ n + 1, and |f y - p.eval y| ≤ E for every y ∈ [a, b].

def Equioscillates (f : ℝ → ℝ) (a b : ℝ) (n : ℕ) (p : ℝ[X]) (E σ : ℝ) (x : ℕ → ℝ) :
    Prop :=
  (σ = 1 ∨ σ = -1) ∧
  p.natDegree ≤ n ∧
  StrictMonoOn x (Set.Icc 0 (n + 1)) ∧
  (∀ i ∈ Set.Icc 0 (n + 1), x i ∈ Set.Icc a b) ∧
  (∀ i ∈ Set.Icc 0 (n + 1), f (x i) - p.eval (x i) = σ * (-1 : ℝ) ^ i * E) ∧
  (∀ y ∈ Set.Icc a b, |f y - p.eval y| ≤ E)

Used by 2

Used byUniqueness of the equioscillating best approximation · Chebyshev equioscillation theorem (sufficiency)

TheoremUniqueness of the equioscillating best approximation#✓fully proved

If p equioscillates against f on [a, b], then p is the unique polynomial of degree at most n whose uniform error on [a, b] is at most E. In particular p is the unique best uniform approximation to f among polynomials of degree at most n.

theorem eq_of_equioscillates {f : ℝ → ℝ} {a b : ℝ} {n : ℕ} {p : ℝ[X]} {E σ : ℝ}
    {x : ℕ → ℝ} (heq : Equioscillates f a b n p E σ x) {q : ℝ[X]}
    (hq : q.natDegree ≤ n) (herr : ∀ y ∈ Set.Icc a b, |f y - q.eval y| ≤ E) : q = p

Uses 1 · Used by 1

Statement usesEquioscillation of a polynomial approximation

Used byChebyshev equioscillation theorem (sufficiency)

TheoremChebyshev equioscillation theorem (sufficiency)#✓fully proved

If p equioscillates against f, then no polynomial of degree at most n has uniform error strictly less than E on [a, b]: p is a best uniform approximation.

theorem not_lt_of_equioscillates {f : ℝ → ℝ} {a b : ℝ} {n : ℕ} {p : ℝ[X]} {E σ : ℝ}
    {x : ℕ → ℝ} (heq : Equioscillates f a b n p E σ x) {q : ℝ[X]}
    (hq : q.natDegree ≤ n) : ¬ ∀ y ∈ Set.Icc a b, |f y - q.eval y| < E

Uses 2

Statement usesEquioscillation of a polynomial approximation

Proof usesUniqueness of the equioscillating best approximation

TheoremDe la Vallée Poussin's theorem#✓fully proved

If the error f - p of a polynomial p of degree at most n alternates with a one-sided lower bound η at n + 2 strictly increasing points of [a, b], η ≤ σ * (-1) ^ i * (f (x i) - p (x i)), then every polynomial of degree at most n has uniform error at least η on [a, b].

theorem de_la_vallee_poussin {f : ℝ → ℝ} {a b : ℝ} {n : ℕ} {p : ℝ[X]} {η σ : ℝ}
    {x : ℕ → ℝ} (hσ : σ = 1 ∨ σ = -1) (hp : p.natDegree ≤ n)
    (hx : StrictMonoOn x (Set.Icc 0 (n + 1)))
    (hxI : ∀ i ∈ Set.Icc 0 (n + 1), x i ∈ Set.Icc a b)
    (halt : ∀ i ∈ Set.Icc 0 (n + 1), η ≤ σ * (-1 : ℝ) ^ i * (f (x i) - p.eval (x i)))
    {q : ℝ[X]} (hq : q.natDegree ≤ n) :
    ¬ ∀ y ∈ Set.Icc a b, |f y - q.eval y| < η

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.