Korovkin's theorem

DefinitionThe identity test function#✓fully proved

The function \(x \mapsto x\) on \([0, 1]\), as an element of \(C([0, 1], \mathbb{R})\).

def korovkinId : C(I, ℝ) :=
  ⟨fun x => (x : ℝ), continuous_subtype_val⟩

Used by 2

Used byKorovkin's theorem · Expansion of the shifted square

DefinitionThe square test function#✓fully proved

The function \(x \mapsto x^2\) on \([0, 1]\), as an element of \(C([0, 1], \mathbb{R})\).

def korovkinIdSq : C(I, ℝ) :=
  ⟨fun x => (x : ℝ) ^ 2, by fun_prop⟩

Used by 2

Used byKorovkin's theorem · Expansion of the shifted square

DefinitionThe shifted square#✓fully proved

For \(x \in [0, 1]\), the function \(y \mapsto (y - x)^2\) on \([0, 1]\), as an element of \(C([0, 1], \mathbb{R})\).

def korovkinShiftSq (x : I) : C(I, ℝ) :=
  ⟨fun y => ((y : ℝ) - (x : ℝ)) ^ 2, by fun_prop⟩

Used by 2

Used byKorovkin's theorem · Expansion of the shifted square

TheoremExpansion of the shifted square#✓fully proved

Write \(e(y) = y\) and \(q(y) = y^2\) for the identity and square functions and \(1\) for the constant function one, as elements of \(C([0, 1], \mathbb{R})\). For every \(x \in [0, 1]\), the function \(y \mapsto (y - x)^2\) in \(C([0, 1], \mathbb{R})\) equals \(q - 2x \cdot e + x^2 \cdot 1\).

theorem korovkinShiftSq_eq (x : I) :
    korovkinShiftSq x =
      korovkinIdSq - (2 * (x : ℝ)) • korovkinId + (x : ℝ) ^ 2 • (1 : C(I, ℝ))

Uses 3 · Used by 1

Statement usesThe identity test function · The square test function · The shifted square

Used byKorovkin's theorem

TheoremUniform convergence implies pointwise convergence#✓fully proved

If a sequence \((u_n)\) in \(C([0, 1], \mathbb{R})\) converges to \(e\) in the sup norm, then \(u_n(x) \to e(x)\) for every \(x \in [0, 1]\).

theorem tendsto_apply_of_tendsto {u : ℕ → C(I, ℝ)} {e : C(I, ℝ)}
    (h : Tendsto u atTop (𝓝 e)) (x : I) :
    Tendsto (fun n => u n x) atTop (𝓝 (e x))

TheoremPositive linear operators are monotone#✓fully proved

Let \(L\) be a real-linear operator on \(C([0, 1], \mathbb{R})\) that is positive: \((L f)(x) \ge 0\) for all \(x \in [0, 1]\) whenever \(f(x) \ge 0\) for all \(x \in [0, 1]\). If \(g, h \in C([0, 1], \mathbb{R})\) satisfy \(g(x) \le h(x)\) for all \(x \in [0, 1]\), then \((L g)(x) \le (L h)(x)\) for every \(x \in [0, 1]\).

theorem le_apply_of_le {L : C(I, ℝ) →ₗ[ℝ] C(I, ℝ)}
    (hpos : ∀ f : C(I, ℝ), (∀ x, 0 ≤ f x) → ∀ x, 0 ≤ L f x)
    {g h : C(I, ℝ)} (hgh : ∀ x, g x ≤ h x) (x : I) : L g x ≤ L h x

Used by 1

Used byPositive linear operators bound absolute values

TheoremPositive linear operators bound absolute values#✓fully proved

Let \(L\) be a real-linear operator on \(C([0, 1], \mathbb{R})\) that is positive: \((L f)(x) \ge 0\) for all \(x \in [0, 1]\) whenever \(f(x) \ge 0\) for all \(x \in [0, 1]\). If \(g, h \in C([0, 1], \mathbb{R})\) satisfy \(|g(y)| \le h(y)\) for all \(y \in [0, 1]\), then \(|(L g)(x)| \le (L h)(x)\) for every \(x \in [0, 1]\).

theorem abs_apply_le {L : C(I, ℝ) →ₗ[ℝ] C(I, ℝ)}
    (hpos : ∀ f : C(I, ℝ), (∀ x, 0 ≤ f x) → ∀ x, 0 ≤ L f x)
    {g h : C(I, ℝ)} (hg : ∀ y, |g y| ≤ h y) (x : I) : |L g x| ≤ L h x

Uses 1 · Used by 1

Proof usesPositive linear operators are monotone

Used byKorovkin's theorem

TheoremQuadratic bound from a modulus of continuity#✓fully proved

Let \(f \in C([0, 1], \mathbb{R})\) have sup norm \(\|f\|\), let \(x \in [0, 1]\), and let \(\delta > 0\), \(\varepsilon \ge 0\) and \(C \ge 0\) be real numbers with \(2\|f\| \le C \delta^2\). If \(|f(y) - f(x)| < \varepsilon\) for every \(y \in [0, 1]\) with \(|y - x| < \delta\), then \(|f(y) - f(x)| \le \varepsilon + C (y - x)^2\) for every \(y \in [0, 1]\).

Korovkin's theorem applies this with \(C = 2\|f\| / \delta^2\).

theorem abs_sub_le_add_sq {f : C(I, ℝ)} {x : I} {δ ε C : ℝ} (hδ : 0 < δ)
    (hε : 0 ≤ ε) (hC : 2 * ‖f‖ ≤ C * δ ^ 2) (hC0 : 0 ≤ C)
    (huni : ∀ y : I, dist y x < δ → |f y - f x| < ε) (y : I) :
    |f y - f x| ≤ ε + C * ((y : ℝ) - (x : ℝ)) ^ 2

Used by 1

Used byKorovkin's theorem

TheoremKorovkin's theorem#✓fully proved

Write \(e_0\), \(e_1\) and \(e_2\) for the functions \(x \mapsto 1\), \(x \mapsto x\) and \(x \mapsto x^2\) in \(C([0, 1], \mathbb{R})\). Let \((L_n)_{n \in \mathbb{N}}\) be real-linear operators on \(C([0, 1], \mathbb{R})\), each positive: \((L_n f)(x) \ge 0\) for all \(x \in [0, 1]\) whenever \(f(x) \ge 0\) for all \(x \in [0, 1]\). If \(L_n e_i \to e_i\) in the sup norm for \(i = 0, 1, 2\), then \(L_n f \to f\) in the sup norm for every \(f \in C([0, 1], \mathbb{R})\).

theorem korovkin {L : ℕ → C(I, ℝ) →ₗ[ℝ] C(I, ℝ)}
    (hpos : ∀ (n : ℕ) (f : C(I, ℝ)), (∀ x, 0 ≤ f x) → ∀ x, 0 ≤ L n f x)
    (h1 : Tendsto (fun n => L n 1) atTop (𝓝 (1 : C(I, ℝ))))
    (hid : Tendsto (fun n => L n korovkinId) atTop (𝓝 korovkinId))
    (hsq : Tendsto (fun n => L n korovkinIdSq) atTop (𝓝 korovkinIdSq))
    (f : C(I, ℝ)) : Tendsto (fun n => L n f) atTop (𝓝 f)

Uses 6

Statement usesThe identity test function · The square test function

Proof usesPositive linear operators bound absolute values · Quadratic bound from a modulus of continuity · The shifted square · Expansion of the shifted square

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.