Prove2Me

Formal product coefficients match polynomial interpolation coefficients

Proved
OAI.PiExponent.AdmissibleFormalInterpolation.explicitProduct_coeff_eq_polynomialCoeff

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

number-theoryopenai-pi-exponent-017

The coefficient of the explicit multivariate formal-series product, at distinguished degree s and remaining degrees b, equals the coefficient of degree s in the polynomial coefficient at b of the interpolation monomial image.

Preamble
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.explicitProduct_coeff_eq_polynomialCoeff
    {m : ℕ} (j s : ℕ) (r : Fin m → ℂ) (G : Fin m → Polynomial ℂ)
    (h : ℕ) (a b : Fin m → ℕ) :
  MvPowerSeries.coeff (InterpolationMatrix.exponentVector (Fin.cases s b))
      ((1 + MvPowerSeries.X 0) ^ h *
        ∏ i, (MvPowerSeries.C ((j : ℂ) * r i) + MvPowerSeries.X i.succ +
          liftLogSeries m (G i : PowerSeries ℂ)) ^ a i) =
    ((InterpolationMatrix.monomialImage r G j h a).coeff
      (InterpolationMatrix.exponentVector b)).coeff s := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph