Substitution fixing the distinguished variable preserves lifted series

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.subst_liftLogSeries_of_X_zero

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

number-theoryopenai-pi-exponent-017

An admissible substitution fixing $X_0$ leaves unchanged a lifted univariate series, since the lift depends only on $X_0$ .

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation
import Mathlib.RingTheory.MvPowerSeries.Substitution

open OAI.PiExponent
open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.subst_liftLogSeries_of_X_zero
    {m : ℕ} (F : PowerSeries ℂ)
    (a : Fin (m + 1) → MvPowerSeries (Fin (m + 1)) ℂ)
    (ha : MvPowerSeries.HasSubst a) (h0 : a 0 = MvPowerSeries.X 0) :
    MvPowerSeries.subst a (liftLogSeries m F) = liftLogSeries m F := by sorry

Source

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

View graph