The packet of the column monomial sum is the matrix image

Proved

OAI.PiExponent.FormalInterpolation.truncated_packet_column_monomial_sum

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

The truncated packet of the explicit finite sum over columns equals the truncated logarithm matrix applied to the coefficient vector.

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_monomial_sum
    {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) :
    truncatedPolynomialPacket K v0 theta w H r T
        (∑ c : InterpolationMatrix.Column w0 w H,
          MvPolynomial.monomial (InterpolationMatrix.exponentVector c.1) (x c)) =
      (InterpolationMatrix.truncatedLogMatrix K w0 v0 theta w H r T).mulVecLin x := by sorry

View graph