Coordinatewise Lagrange interpolation on a finite grid. The degree depends on the side length of the grid rather than its number of points.
theorem
CCDN.grid_points_filtered_lower
{K : Type u_1}
{σ : Type u_2}
{ι : Type u_3}
[Field K]
[Fintype σ]
[Fintype ι]
(I : Ideal (MvPolynomial σ K))
(S : Finset K)
(z : ι → σ → K)
(hz : Function.Injective z)
(hzS : ∀ (i : ι) (j : σ), z i j ∈ S)
(hzI : ∀ (i : ι), ∀ f ∈ I, (MvPolynomial.eval (z i)) f = 0)
{N : ℕ}
(hN : Fintype.card σ * (S.card - 1) ≤ N)
:
Distinct points of a fixed coordinate grid give independent filtered coordinate classes at the grid-interpolation degree.