English
Let F be a field, ι a type, and s ⊆ ι a finite set with cardinality n. Let v: ι → F be a function whose values on s are pairwise distinct. Then the space of polynomials over F of degree less than n is linearly isomorphic to the space of all functions from s to F, via evaluation at the nodes v|s, with the inverse given by Lagrange interpolation.
Русский
Пусть F — поле, ι — множество, s ⊆ ι — конечное множество с кардиналом n. Пусть v : ι → F такова, что значения на s различны. Тогда пространство полиномов над F степени меньше n изоморфно пространству всех функций s → F при помощи оценки в узлах v на s, а обратное отображение задаётся интерполяцией Лагранжа.
LaTeX
$$$ \\deg_{<|s|}(F) \\cong_F s \\to F $$$
Lean4
/-- Lagrange interpolation induces isomorphism between functions from `s`
and polynomials of degree less than `Fintype.card ι`. -/
def funEquivDegreeLT (hvs : Set.InjOn v s) : degreeLT F #s ≃ₗ[F] s → F
where
toFun f i := f.1.eval (v i)
map_add' _ _ := funext fun _ => eval_add
map_smul' c f := funext <| by simp
invFun
r := ⟨interpolate s v fun x => if hx : x ∈ s then r ⟨x, hx⟩ else 0, mem_degreeLT.2 <| degree_interpolate_lt _ hvs⟩
left_inv := by
rintro ⟨f, hf⟩
simp only [Subtype.mk_eq_mk, dite_eq_ite]
rw [mem_degreeLT] at hf
conv => rhs; rw [eq_interpolate hvs hf]
exact interpolate_eq_of_values_eq_on _ _ fun _ hi => if_pos hi
right_inv := by
intro f
ext ⟨i, hi⟩
simp only [eval_interpolate_at_node _ hvs hi]
exact dif_pos hi
