Padded packet vanishing detects simultaneous jet ideal powers
ProvedOAI.PiExponent.LogarithmicJetIdeals.padded_packet_kernel_in_simultaneous_powernumber-theoryopenai-pi-exponent-017
With positive row weights and exponents, distinct centers, truncation tails of sufficiently large weight, and generator weights bounded above by S, vanishing of the raw packet below (n+m)S implies membership in the nth power of the simultaneous logarithmic jet ideal.
Preamble
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals open OAI.PiExponent open OAI.PiExponent.AdmissibleFormalInterpolation open OAI.PiExponent.LogarithmicJetIdeals
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.padded_packet_kernel_in_simultaneous_power
{m : ℕ} (K : ℕ) (v0 theta : ℝ) (w : Fin m → ℝ) (S : ℝ)
(r : Fin m → ℂ) (T : Fin m → ℕ) (e : Fin (m + 1) → ℕ)
(hS : 0 < S)
(hv : ∀ i, 0 < InterpolationMatrix.rowWeights v0 theta w i)
(he : ∀ i, 0 < e i)
(hscale : ∀ i, (e i : ℝ) * InterpolationMatrix.rowWeights v0 theta w i ≤ S)
(hT : ∀ i : Fin m,
InterpolationMatrix.rowWeights v0 theta w i.succ ≤ (T i : ℝ) * v0)
(hc : Function.Injective (fun j : Fin K => fun i : Fin m => (j.val : ℂ) * r i))
(n : ℕ) (P : MvPolynomial (Fin (m + 1)) ℂ)
(hpacket : rawPacketMap K v0 theta w (((n + m : ℕ) : ℝ) * S) r P = 0) :
P ∈ (simultaneousJetIdeal K r T e) ^ n := by sorrySource