A column monomial packet coefficient is its matrix entry

Proved

OAI.PiExponent.FormalInterpolation.truncated_packet_monomial_coeff_eq_entry

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

For a fixed row and column, the coefficient extracted from the substituted column monomial equals its scalar coefficient times the corresponding truncated logarithm matrix entry.

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_monomial_coeff_eq_entry
    {m : Nat} (K : Nat) (w0 v0 theta : Real) (w : Fin m → Real) (H : Real)
    (r : Fin m → Complex) (T : Fin m → Nat)
    (rho : InterpolationMatrix.Row K v0 theta w H)
    (c : InterpolationMatrix.Column w0 w H) (z : Complex) :
    (truncatedPolynomialJet (fun i => (rho.1.val : Complex) * r i) T
      (MvPolynomial.monomial (InterpolationMatrix.exponentVector c.1) z)).coeff
        (InterpolationMatrix.exponentVector rho.2.val) =
      z * InterpolationMatrix.entry r (fun i => InterpolationMatrix.truncatedLog (T i))
        rho.1.val (rho.2.1 0) (fun i => rho.2.1 i.succ)
        (c.1 0) (fun i => c.1 i.succ) := by sorry

View graph