bernsteinApproximation — Mathlib

English

The Bernstein approximation is the finite sum ∑_{k=0}^{n} B_{n,k}(x) f(k/n).

Русский

Аппроксимация Бернштейна задаётся конечной суммой ∑_{k=0}^{n} B_{n,k}(x) f(k/n).

LaTeX

$$$\text{bernsteinApproximation } n\ f\ x = \sum_{k=0}^{n} B_{n,k}(x) f\left( k/n \right)$$$

Lean4

/-- The `n`-th approximation of a continuous function on `[0,1]` by Bernstein polynomials,
given by `∑ k, bernstein n k x • f (k/n)`.
-/
def bernsteinApproximation (n : ℕ) (f : C(I, E)) : C(I, E) :=
  ∑ k : Fin (n + 1), bernstein n k • .const _ (f k/ₙ)

Похожие утверждения