Finite multivariate Taylor interpolation at distinct center–exponent pairs

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.ordinaryTaylor_interpolatingPolynomial

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

number-theoryopenai-pi-exponent-017

For any selected pair in a finite family of distinct center–exponent pairs, there is a multivariate polynomial whose ordinary Taylor coefficient at that pair is one and whose coefficients at all other pairs in the family are zero.

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation

open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.ordinaryTaylor_interpolatingPolynomial
    {m : ℕ} {ι : Type} [Fintype ι] [DecidableEq ι]
    (center : ι → Fin (m + 1) → ℂ)
    (exponent : ι → (Fin (m + 1) →₀ ℕ))
    (hindex : Function.Injective (fun x => (center x, exponent x)))
    (x : ι) :
    ∃ p : MvPolynomial (Fin (m + 1)) ℂ,
      ∀ y : ι,
        (((MvPowerSeries.coeff (exponent y)).comp
          (MvPolynomial.aeval (fun i =>
            MvPowerSeries.C (center y i) + MvPowerSeries.X i)).toLinearMap) p) =
          if y = x then 1 else 0 := by sorry

Source

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

View graph