Weighted bound for a partial derivative

Proved

OAI.PiExponent.FormalInterpolation.logarithmicDegreeBound_pderiv_support_v2

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

A partial derivative in a positive-weight coordinate preserves the upper bound on weighted support degree. A proof route identifies each supported derivative exponent with an original exponent having positive coordinate i, then uses positivity of w i to bound the reduced degree. Zero derivatives are covered by empty support.

Preamble

import Definitions.Def_OAI_PiExponent_LogarithmicWordContact

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

Formal statement

theorem OAI.PiExponent.FormalInterpolation.logarithmicDegreeBound_pderiv_support_v2
    {d : Nat} (w : Fin d → Rat) (hw : ∀ i, 0 < (w i : Real))
    (N : Real) (F : MvPolynomial (Fin d) Complex)
    (hF : logarithmicDegreeBound w N F) (i : Fin d) :
    logarithmicDegreeBound w N (MvPolynomial.pderiv i F) := by sorry

View graph