Interpolation bounds the number of points

If a space of functions α → K interpolates every function on a finite set G, restricting to G maps it onto G → K, so its dimension is at least |G|. For the span of finitely many functions v a, a ∈ s, this gives |G| ≤ |s| (Cslib.LinearAlgebra.card_le_of_forall_exists_mem_span_eq). This is the dimension count of the polynomial method: if every function agrees on G with a combination of few functions, G is small.

Main results

• Cslib.LinearAlgebra.card_le_of_forall_exists_mem_span_eq: if every function agrees on G with a combination of the functions v a for a ∈ s, then #G ≤ #s.

theorem Cslib.LinearAlgebra.card_le_of_forall_exists_mem_span_eq {α : Type u_1} {ι : Type u_2} {K : Type u_3} [Field K] (G : Finset α) (s : Finset ι) (v : ι → α → K) (h : ∀ (f : α → K), ∃ g ∈ Submodule.span K (v '' ↑s), ∀ x ∈ G, g x = f x) : G.card ≤ s.card

If every function agrees on G with a combination of the functions v a for a ∈ s, then G has at most #s points: restricting the span to G is onto G → K.