Weighted pole support is covered by coordinate pole supports

Proved

OAI.PiExponent.FormalInterpolation.polynomialCurvePole_support_subset_coordinate_poles

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynumber-theoryopenai-pi-exponent-017

Let $w_i>0$ be coordinate weights. At any normalized place $\nu$ , the weighted pole

\mathrm{Pole}_\nu(x,w)=\sup\bigl\{0\bigr\}\cup\bigl\{-(x_j)_\nu/w_j:j\bigr\}

is strictly positive only if some coordinate satisfies $-(x_j)_\nu>0$ . Consequently the support of $\mathrm{Pole}_\nu(x,w)$ is contained in the union of the individual coordinate pole supports.

Preamble

import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion

open scoped BigOperators
open OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.polynomialCurvePole_support_subset_coordinate_poles
    {d : Nat} {E : Type} [Field E] [Algebra Complex E]
    (x : Fin d → E) (w : Fin d → Rat) (hw : ∀ i, 0 < (w i : Real)) :
    {nu : PolynomialCurvePlace E | polynomialCurvePole nu x w ≠ 0} ⊆
      ⋃ j : Fin d, {nu | max (-(polynomialCurveOrder nu (x j) : Real)) 0 ≠ 0} := by sorry

Source

Elementary consequence of the Option-supremum definition of polynomialCurvePole in Def_OAI_PiExponent_WeightedIdealCurveCriterion; reduction obligation for coordinateWeightedPole_support_finite.

View graph