Weighted bound is closed under addition

Proved

OAI.PiExponent.FormalInterpolation.logarithmicDegreeBound_add_support_v2

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

Addition preserves a common weighted support-degree bound because the support of a sum is contained in the union of the supports. A proof route uses support membership for addition; cancellation only removes terms.

Preamble

import Definitions.Def_OAI_PiExponent_LogarithmicWordContact

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.logarithmicDegreeBound_add_support_v2
    {d : Nat} (w : Fin d → Rat) (N : Real)
    (F G : MvPolynomial (Fin d) Complex)
    (hF : logarithmicDegreeBound w N F)
    (hG : logarithmicDegreeBound w N G) :
    logarithmicDegreeBound w N (F + G) := by sorry

View graph