A coordinate pole is bounded at each place

Proved

OAI.PiExponent.FormalInterpolation.coordinate_pole_le_weighted_at_place

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

At each place, the selected coordinate's nonnegative pole order is bounded by its positive weight times the weighted pole supremum.

Preamble

import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion

open scoped BigOperators
open OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.coordinate_pole_le_weighted_at_place {d : Nat} {E : Type} [Field E] [Algebra Complex E] (x : Fin d → E) (w : Fin d → Rat) (hw : ∀ i, 0 < (w i : Real)) (k : Fin d) : ∀ nu : PolynomialCurvePlace E, 0 ≤ max (-(polynomialCurveOrder nu (x k) : Real)) 0 ∧ max (-(polynomialCurveOrder nu (x k) : Real)) 0 ≤ (w k : Real) * polynomialCurvePole nu x w := by sorry

View graph