Prove2Me

Substitution fixing the first variable fixes lifted series

Proved
OAI.PiExponent.LogarithmicJetIdeals.subst_liftLogSeries_fixed

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

number-theoryopenai-pi-exponent-017

Every admissible substitution fixing the first formal variable preserves every power series lifted through that variable, with no restriction on its constant coefficient.

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

open OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.subst_liftLogSeries_fixed
    {m : ℕ} (a : Fin (m + 1) → MvPowerSeries (Fin (m + 1)) ℂ)
    (ha : MvPowerSeries.HasSubst a) (ha0 : a 0 = MvPowerSeries.X 0)
    (f : PowerSeries ℂ) :
    MvPowerSeries.subst a
      (OAI.PiExponent.AdmissibleFormalInterpolation.liftLogSeries m f) =
        OAI.PiExponent.AdmissibleFormalInterpolation.liftLogSeries m f := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph