Linearity of the truncated packet on a column monomial sum

Proved

OAI.PiExponent.FormalInterpolation.truncated_packet_column_sum_linear

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

At each row, the truncated packet of the finite sum of column monomials equals the sum of the packets of those monomials.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets

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

Formal statement

theorem OAI.PiExponent.FormalInterpolation.truncated_packet_column_sum_linear
    {m : Nat} (K : Nat) (w0 v0 theta : Real) (w : Fin m → Real) (H : Real)
    (r : Fin m → Complex) (T : Fin m → Nat)
    (x : InterpolationMatrix.Column w0 w H → Complex)
    (rho : InterpolationMatrix.Row K v0 theta w H) :
    truncatedPolynomialPacket K v0 theta w H r T
        (∑ c : InterpolationMatrix.Column w0 w H,
          MvPolynomial.monomial (InterpolationMatrix.exponentVector c.1) (x c)) rho =
      ∑ c : InterpolationMatrix.Column w0 w H,
        truncatedPolynomialPacket K v0 theta w H r T
          (MvPolynomial.monomial (InterpolationMatrix.exponentVector c.1) (x c)) rho := by sorry

View graph