Prove2Me

Formula for the composed sheared substitution

Proved
OAI.PiExponent.LogarithmicJetIdeals.formalJet_sheared_substitution_formula

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

number-theoryopenai-pi-exponent-017

After the specified polynomial substitution and application of formalJet, the resulting series is polynomial evaluation at X 0 for the first variable and X i.succ + liftLogSeries m (PowerSeries.log ℂ) - X 0 for each later variable.

Preamble
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation

open scoped BigOperators
open OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.formalJet_sheared_substitution_formula
    {m : Nat}
    (center : Fin m -> Complex)
    (Q : MvPolynomial (Fin (m + 1)) Complex) :
    formalJet center (MvPolynomial.aeval
      (Fin.cases (MvPolynomial.X 0 - MvPolynomial.C 1)
        (fun i => MvPolynomial.X i.succ - MvPolynomial.C (center i) -
          (MvPolynomial.X 0 - MvPolynomial.C 1))) Q) =
      MvPolynomial.aeval
        (Fin.cases (MvPowerSeries.X 0)
          (fun i => MvPowerSeries.X i.succ +
            liftLogSeries m (PowerSeries.log ℂ) - MvPowerSeries.X 0)) Q := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph