evalBernstein

Mathlib.Analysis.SpecialFunctions.Bernstein

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Positivity.evalBernstein

Lean4

/-- Extension of the `positivity` tactic for Bernstein polynomials: they are always non-negative. -/
@[positivity DFunLike.coe (bernstein _ _) _]
def evalBernstein : PositivityExt where
  eval {_ _} _zα _pα
    e := do
    let .app (.app _coe (.app (.app _ n) ν)) x ← whnfR e |
      throwError"not bernstein polynomial"
    let p ← mkAppOptM ``bernstein_nonneg #[n, ν, x]
    pure (.nonnegative p)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru