Successor jet coefficient decomposition

Proved

OAI.PiExponent.LogarithmicJetIdeals.local_jet_generator_formalJet_decomposition_succ

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

number-theoryopenai-pi-exponent-017

Each coefficient of the formal image of a successor jet generator is the sum of the corresponding successor-variable coefficient and lifted logarithmic-tail coefficient, for arbitrary complex parameters and every natural cutoff.

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation
import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals
open OAI.PiExponent
open OAI.PiExponent.AdmissibleFormalInterpolation
open OAI.PiExponent.LogarithmicJetIdeals
open scoped BigOperators

Formal statement

theorem OAI.PiExponent.LogarithmicJetIdeals.local_jet_generator_formalJet_decomposition_succ
    {m : ℕ} (c : Fin m → ℂ) (T : Fin m → ℕ)
    (b : Fin (m + 1) → ℕ) (i : Fin m) :
    MvPowerSeries.coeff (InterpolationMatrix.exponentVector b)
      (AdmissibleFormalInterpolation.formalJet c
        (jetCoordinate c T i.succ)) =
      MvPowerSeries.coeff (InterpolationMatrix.exponentVector b)
        (MvPowerSeries.X i.succ) +
      MvPowerSeries.coeff (InterpolationMatrix.exponentVector b)
        (AdmissibleFormalInterpolation.liftLogSeries m
          (PowerSeries.log ℂ -
            (InterpolationMatrix.truncatedLog (T i) : PowerSeries ℂ))) := by sorry

Source

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

View graph