Coefficient transfer from supported monomials

Proved

OAI.PiExponent.LogarithmicJetIdeals.coeff_aeval_eq_coeff_of_monomial_coeff

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

number-theoryopenai-pi-exponent-017

If evaluation preserves the coefficient indexed by e for every unit monomial supported in Q, then it preserves that coefficient for Q. This is the finite polynomial expansion step, using additivity of evaluation and coefficient extraction.

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation

open scoped BigOperators

Formal statement

theorem OAI.PiExponent.LogarithmicJetIdeals.coeff_aeval_eq_coeff_of_monomial_coeff
    {m : Nat}
    (R : Fin (m + 1) -> MvPowerSeries (Fin (m + 1)) Complex)
    (Q : MvPolynomial (Fin (m + 1)) Complex)
    (e : Fin (m + 1) -> Nat)
    (hmono : ∀ a : Finsupp (Fin (m + 1)) Nat, a ∈ Q.support ->
      MvPowerSeries.coeff (Finsupp.equivFunOnFinite.symm e)
        (MvPolynomial.aeval R (MvPolynomial.monomial a (1 : Complex))) =
      MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm e)
        (MvPolynomial.monomial a (1 : Complex))) :
    MvPowerSeries.coeff (Finsupp.equivFunOnFinite.symm e)
      (MvPolynomial.aeval R Q) =
      MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm e) Q := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph