Column combinations preserve the weighted support bound

Proved

OAI.PiExponent.AdmissibleFormalInterpolation.columnCombination_weightedSupport

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

number-theoryopenai-pi-exponent-017

Every exponent in the finite column combination satisfies the weighted support bound. Each summand is a monomial at a column exponent that already satisfies the bound; zero coefficients and the empty column set are covered.

Preamble

import Definitions.Def_OAI_PiExponent_ColumnCombination

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

Formal statement

theorem OAI.PiExponent.AdmissibleFormalInterpolation.columnCombination_weightedSupport
    {m : ℕ} (w0 : ℝ) (w : Fin m → ℝ) (H : ℝ)
    (x : InterpolationMatrix.Column w0 w H → ℂ) :
    ∀ a ∈ (columnCombination w0 w H x).support,
      ∑ i, InterpolationMatrix.columnWeights w0 w i * (a i : ℝ) ≤ H := by sorry

Source

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

View graph