Truncated packet equals matrix mulVec for positive-weight weighted polynomials

Proved

OAI.PiExponent.FormalInterpolation.truncated_packet_matrix_of_polynomial_coefficients_of_pos

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

When column weights and the height are strictly positive, a weighted polynomial's truncated packet equals the truncated-log matrix applied to its column coefficients. Positivity places every support exponent in the real weighted simplex, so the support sum of jet coefficients reindexes to the matrix column sum.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets

open OAI.PiExponent OAI.PiExponent.DeterminantContradiction OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.truncated_packet_matrix_of_polynomial_coefficients_of_pos
    {m : Nat} (K : Nat) (w0 v0 theta : Real) (w : Fin m → Real) (H : Real)
    (r : Fin m → Complex) (T : Fin m → Nat)
    (hw0 : 0 < w0) (hw : ∀ i, 0 < w i) (hH : 0 < H)
    (P : WeightedPolynomial w0 w H) :
    truncatedPolynomialPacket K v0 theta w H r T P.val =
      (InterpolationMatrix.truncatedLogMatrix K w0 v0 theta w H r T).mulVecLin
        (fun c : InterpolationMatrix.Column w0 w H =>
          P.val.coeff (InterpolationMatrix.exponentVector c.1)) := by sorry

Source

Reindexing of truncated_polynomial_jet_support_expansion via weighted_coordinates_mem_realWeightedSimplex and truncated_packet_support_sum_eq_column_sum under positive weights.

View graph