Plain jet evaluates shifted coordinate products

Proved

OAI.PiExponent.LogarithmicJetIdeals.plainJet_shifted_product_eq_Xprod

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

number-theoryopenai-pi-exponent-017

Applying plainJet to a scalar times a product of powers of coordinates shifted by the jet center gives the same scalar times the product of the corresponding formal variables to those powers. The statement includes zero exponents and the empty product.

Preamble

import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals_PlainJet
import Mathlib.Data.Fintype.Pi

open scoped BigOperators
open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.LogarithmicJetIdeals.plainJet_shifted_product_eq_Xprod
    {m : Nat} (c : Fin m -> Complex) (a : Complex)
    (d : Fin (m + 1) -> Nat) :
    OAI.PiExponent.LogarithmicJetIdeals.plainJet c
        (MvPolynomial.C a *
          Finset.prod Finset.univ (fun k : Fin (m + 1) =>
            (MvPolynomial.X k -
              MvPolynomial.C ((Fin.cases (1 : Complex) c : Fin (m + 1) -> Complex) k)) ^ d k)) =
      MvPowerSeries.C a *
        Finset.prod Finset.univ (fun k : Fin (m + 1) =>
          (MvPowerSeries.X k) ^ d k) := by sorry

Source

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

View graph