English
Equivalent formulations comparing coefficient-wise equality of interpolations.
Русский
Эквивалентные формулировки, сравнивающие по коэффициентам, равенство интерволнований.
LaTeX
$$interpolate_eq_iff_values_eq_on (hvs) : interpolate s v r = interpolate s v r' ↔ ∀ i∈s, r i = r' i$$
Lean4
/-- This is the characteristic property of the interpolation: the interpolation is the
unique polynomial of `degree < Fintype.card ι` which takes the value of the `r i` on the `v i`.
-/
theorem eq_interpolate_iff {f : F[X]} (hvs : Set.InjOn v s) :
(f.degree < #s ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = interpolate s v r :=
by
constructor <;> intro h
· exact eq_interpolate_of_eval_eq _ hvs h.1 h.2
· rw [h]
exact ⟨degree_interpolate_lt _ hvs, fun _ hi => eval_interpolate_at_node _ hvs hi⟩
