Definition. Polynomial constraints and evaluation filtrations [cn-0019]

Let \(W\) be a finite-dimensional real vector space, the ambient space of polynomial values, and let \(U_1,\ldots ,U_m\subseteq W\) be subspaces. Choose distinct real interpolation nodes [cn-0063] \(t_1,\ldots ,t_m\), at which we impose conditions on those vector values. For a subspace \(Z\subseteq W\), write \(Z[\xi ]\) for the univariate polynomial maps [cn-0064] with coefficients in \(Z\): \(P(\xi )=\sum _{r=0}^{h}z_r\xi ^r\) with each \(z_r\in Z\).

The constrained polynomial space, for \(h\geq 0\), is

\[\mathcal P_h(Z)=\{P\in Z[\xi ]:\deg P\leq h,\ P(t_i)\in U_i\text { for every }i\},\qquad \mathcal P_{-1}(Z)=0.\]

Each constraint means \(\sum _{r=0}^{h}t_i^r z_r\in U_i\). This sum already belongs to \(Z\), so the permitted value lies in \(U_i\cap Z\). The coefficients form a tuple in \(Z^{h+1}\), and these are linear conditions on that tuple.

Its evaluation space and dimension increment are

\[E_h(Z;t)=\{P(t):P\in \mathcal P_h(Z)\},\qquad k_h(Z)=\dim \mathcal P_h(Z)-\dim \mathcal P_{h-1}(Z),\quad k_{-1}(Z)=0.\]

For a fixed \(t_*\notin \{t_1,\ldots ,t_m\}\), called a non-node [cn-0063], the spaces \(E_h(W;t_*)\) are nested. After identifying their dimensions [cn-0020], write \(\ell _h=k_h(W)-k_{h-1}(W)\) for the evaluation-filtration increment. Nonnegativity of these increments is a consequence of nesting.

Lean uses a strict degree bound: its space indexed by \(h+1\) corresponds to the paper's \(\mathcal P_h\). The Lean guide [cn-0038] records this shift.

Proof dependencies
Univariate polynomial maps [cn-0064]; Interpolation nodes [cn-0063]
Provenance
OpenAI, 23 September 2026 [cn-0042], proof of Lemma 2.1; reconstructed as a reading account on 9 October 2026. Lean source: PolynomialFiltration.