degree_interpolate_le — Mathlib

English

The degree of interpolate(s,v,r) is at most card(s) minus 1.

Русский

Степень многочлена интерполяции не выше, чем card(s) − 1.

LaTeX

$$\deg(\text{interpolate}(s,v,r)) \le |s|-1$$

Lean4

theorem degree_interpolate_le (hvs : Set.InjOn v s) : (interpolate s v r).degree ≤ ↑(#s - 1) :=
  by
  refine (degree_sum_le _ _).trans ?_
  rw [Finset.sup_le_iff]
  intro i hi
  rw [degree_mul, degree_basis hvs hi]
  by_cases hr : r i = 0
  · simpa only [hr, map_zero, degree_zero, WithBot.bot_add] using bot_le
  · rw [degree_C hr, zero_add]

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