Reindex a polynomial support sum by interpolation columns

Proved

OAI.PiExponent.FormalInterpolation.support_sum_eq_column_sum

by Eyal1990 · Oct 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

If every exponent in a polynomial's support is represented by an interpolation column, then summing a function of supported exponents with the polynomial coefficients is equal to summing the same function over all interpolation columns; columns outside the support contribute zero.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.support_sum_eq_column_sum
    {m : Nat} (w0 : Real) (w : Fin m → Real) (H : Real)
    (P : MvPolynomial (Fin (m + 1)) Complex)
    (F : (Fin (m + 1) →₀ Nat) → Complex)
    (hcols : ∀ e ∈ P.support,
      ∃ c : InterpolationMatrix.Column w0 w H,
        InterpolationMatrix.exponentVector c.1 = e) :
      ∑ e ∈ P.support, P.coeff e * F e =
        ∑ c : InterpolationMatrix.Column w0 w H,
          P.coeff (InterpolationMatrix.exponentVector c.1) *
            F (InterpolationMatrix.exponentVector c.1) := by sorry

View graph