Weight triangularity truncates the shear coefficient expansion

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.weighted_finsum_cutoff

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

number-theoryopenai-pi-exponent-017

Positive weights and weight triangularity force every monomial contribution from outside the strict weighted simplex to vanish at b. Prove that weight below H implies membership by the coordinate bounds a i ≤ floor(H / w i), then restrict the finsum to this finite set. Equality at weight H is excluded, and still gives strictly larger weight than b. The zero-constant hypothesis is retained for compatibility, although this cutoff argument does not use it.

Preamble

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

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

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.weighted_finsum_cutoff
    {m : ℕ} (v0 : ℝ) (u : Fin m → ℝ) (H : ℝ)
    (D : Fin m → PowerSeries ℂ)
    (hv0 : 0 < v0) (hu : ∀ i, 0 < u i) (hH : 0 < H)
    (hD0 : ∀ i, PowerSeries.coeff 0 (D i) = 0)
    (htri : ∀ (a b : Fin (m + 1) → ℕ),
      (∑ i, Fin.cases v0 u i * (b i : ℝ)) <
        (∑ i, Fin.cases v0 u i * (a i : ℝ)) →
      MvPowerSeries.coeff (InterpolationMatrix.exponentVector b)
        (seriesShear D
          (MvPolynomial.monomial (InterpolationMatrix.exponentVector a) 1)) = 0)
    (G : MvPowerSeries (Fin (m + 1)) ℂ)
    (b : ↥(strictWeightedSimplex (Fin.cases v0 u) H)) :
    (∑ᶠ a : Fin (m + 1) → ℕ,
      MvPowerSeries.coeff (InterpolationMatrix.exponentVector a) G *
        MvPowerSeries.coeff (InterpolationMatrix.exponentVector b.val)
          (seriesShear D
            (MvPolynomial.monomial (InterpolationMatrix.exponentVector a) 1))) =
      (∑ a : ↥(strictWeightedSimplex (Fin.cases v0 u) H),
        MvPowerSeries.coeff (InterpolationMatrix.exponentVector a.val) G *
          MvPowerSeries.coeff (InterpolationMatrix.exponentVector b.val)
            (seriesShear D
              (MvPolynomial.monomial (InterpolationMatrix.exponentVector a.val) 1))) := by sorry

Source

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

View graph