Triangular tail substitutions satisfy the weighted support bound
ProvedOAI.PiExponent.AdmissibleFormalInterpolation.triangular_tail_substitution_supportnumber-theoryopenai-pi-exponent-017
Under the positive-weight, cutoff, and tail-vanishing hypotheses, every exponent appearing in a substituted variable has weighted degree at least the weight of that variable. For the initial variable this follows from its image being X 0; for each other variable it follows from the identity term and the tail cutoff.
Preamble
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation import Mathlib.RingTheory.MvPowerSeries.Substitution open scoped BigOperators open OAI.PiExponent open OAI.PiExponent.AdmissibleFormalInterpolation
Formal statement
theorem OAI.PiExponent.AdmissibleFormalInterpolation.triangular_tail_substitution_support
{m : ℕ} (q : Fin (m + 1) → ℝ) (T : Fin m → ℕ)
(R : Fin m → PowerSeries ℂ)
(hq : ∀ i, 0 < q i)
(hT : ∀ i : Fin m, q i.succ ≤ (T i : ℝ) * q 0)
(hR : ∀ (i : Fin m) (k : ℕ), k < T i → PowerSeries.coeff k (R i) = 0) :
∀ (i : Fin (m + 1)) (a : Fin (m + 1) → ℕ),
MvPowerSeries.coeff (InterpolationMatrix.exponentVector a)
(Fin.cases (MvPowerSeries.X 0)
(fun j : Fin m => MvPowerSeries.X j.succ + liftLogSeries m (R j)) i) ≠ 0 →
q i ≤ ∑ j, q j * (a j : ℝ) := by sorrySource