bernstein_apply — Mathlib

English

For n, ν ∈ ℕ, the Bernstein polynomial B_{n,ν} is the continuous function on [0,1] given by B_{n,ν}(x) = C(n,ν) x^{ν} (1−x)^{n−ν}.

Русский

Для целых n, ν ∈ ℕ полином Бернштейна B_{n,ν} на отрезке [0,1] задан как B_{n,ν}(x) = C(n,ν) x^{ν} (1−x)^{n−ν}.

LaTeX

$$$B_{n,\nu}(x) = {n \choose \nu} x^{\nu} (1-x)^{n-\nu}, \quad x \in [0,1]$$$

Lean4

theorem bernstein_apply (n ν : ℕ) (x : I) :
    bernstein n ν x = (n.choose ν : ℝ) * (x : ℝ) ^ ν * (1 - (x : ℝ)) ^ (n - ν) :=
  by
  dsimp [bernstein, Polynomial.toContinuousMapOn, Polynomial.toContinuousMap, bernsteinPolynomial]
  simp

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