Filtered substitution cannot lower monomial weight

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.mvPowerSeries_substitution_monomial_coeff_eq_zero_of_weight_lt

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

number-theoryopenai-pi-exponent-017

For any real coordinate weights, replacing each variable Xᵢ₊₁ by Xᵢ₊₁+Lᵢ cannot create a monomial coefficient at strictly lower weight if every coefficient of Lᵢ has weight at least uᵢ. This applies also when some weights are nonpositive; the assertion follows by expanding the finite monomial substitution and checking the weight of each contribution.

Preamble

import Definitions.Def_OAI_PiExponent_WeightedJetShear

open OAI.PiExponent OAI.PiExponent.AdmissibleFormalInterpolation
open scoped BigOperators

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.mvPowerSeries_substitution_monomial_coeff_eq_zero_of_weight_lt
    {m : ℕ} (v0 : ℝ) (u : Fin m → ℝ)
    (L : Fin m → MvPowerSeries (Fin (m + 1)) ℂ)
    (hL : ∀ i α,
      (∑ j, Fin.cases v0 u j * (α j : ℝ)) < u i →
        MvPowerSeries.coeff α (L i) = 0)
    (a b : Fin (m + 1) → ℕ)
    (hab : (∑ i, Fin.cases v0 u i * (b i : ℝ)) <
      (∑ i, Fin.cases v0 u i * (a i : ℝ))) :
    MvPowerSeries.coeff (InterpolationMatrix.exponentVector b)
      (MvPolynomial.aeval (Fin.cases (MvPowerSeries.X 0)
        (fun i => MvPowerSeries.X i.succ + L i))
        (MvPolynomial.monomial (InterpolationMatrix.exponentVector a) 1)) = 0 := by sorry

Source

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

View graph