Ideal-power membership through polynomial logarithmic jet coefficients
ProvedOAI.PiExponent.LogarithmicJetIdeals.power_membership_iff_polynomialJet_coefficientsnumber-theoryopenai-pi-exponent-017
For positive coordinate exponents and distinct arithmetic-progression centers, membership in a power of the simultaneous jet ideal is equivalent to vanishing of the translated polynomial jet coefficients on the staircase defined by the sum of coordinatewise integer quotients being strictly less than the power index.
Preamble
import Definitions.Def_OAI_PiExponent_PolynomialLogarithmicJets open OAI.PiExponent OAI.PiExponent.LogarithmicJetIdeals open scoped BigOperators
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.power_membership_iff_polynomialJet_coefficients
{m : ℕ} (K : ℕ) (r : Fin m → ℂ) (T : Fin m → ℕ)
(e : Fin (m + 1) → ℕ)
(hr : ∃ i, r i ≠ 0) (he : ∀ i, 0 < e i)
(k : ℕ) (P : MvPolynomial (Fin (m + 1)) ℂ) :
P ∈ (simultaneousJetIdeal K r T e) ^ k ↔
∀ j : Fin K, ∀ u : Fin (m + 1) →₀ ℕ,
(∑ i, u i / e i) < k →
MvPolynomial.coeff u
(polynomialJet (fun i => (j.val : ℂ) * r i) T P) = 0 := by sorrySource