Prove2Me

Admissible formal shear composes with polynomial series jets

Proved
OAI.PiExponent.AdmissibleFormalInterpolation.seriesShear_subst_seriesJet

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

number-theoryopenai-pi-exponent-017

When every D_i has zero constant coefficient, formal shear substitution sends the polynomial series jet formed using F to the jet formed using F+D. The background family F may have arbitrary constant terms.

Preamble
import Definitions.Def_OAI_PiExponent_WeightedJetShear
import Mathlib.RingTheory.MvPowerSeries.Substitution

open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.seriesShear_subst_seriesJet
    {m : ℕ} (D F : Fin m → PowerSeries ℂ) (c : Fin m → ℂ)
    (hD0 : ∀ i, PowerSeries.coeff 0 (D i) = 0)
    (P : MvPolynomial (Fin (m + 1)) ℂ) :
    MvPowerSeries.subst
        (Fin.cases (MvPowerSeries.X 0)
          (fun i => MvPowerSeries.X i.succ + liftLogSeries m (D i)))
        (seriesJet c F P) =
      seriesJet c (fun i => F i + D i) P := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph