Coefficients of the evaluated homogeneous sum
ProvedOAI.PiExponent.LogarithmicJetIdeals.finite_homogeneous_sum_coeffnumber-theoryopenai-pi-exponent-017
For a finite set containing exactly the degree- multi-indices, the coefficient at any degree at most of the evaluated weighted sum is the prescribed value in degree and zero below it. The lower-degree and equal-degree cases use hbelow and hsame, respectively.
Preamble
import Mathlib.Data.Complex.Basic import Mathlib.RingTheory.MvPowerSeries.Equiv open scoped BigOperators
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.finite_homogeneous_sum_coeff
{n : Nat}
(phi : Fin n → MvPowerSeries (Fin n) Complex)
(N : Nat)
(hbelow : ∀ d e : Fin n → Nat,
(∑ k, d k) ≤ N → (∑ k, e k) ≤ N →
(∑ k, e k) < (∑ k, d k) →
MvPowerSeries.coeff (Finsupp.equivFunOnFinite.symm e)
(MvPolynomial.aeval phi
(MvPolynomial.monomial (Finsupp.equivFunOnFinite.symm d) (1 : Complex))) = 0)
(hsame : ∀ d e : Fin n → Nat,
(∑ k, d k) ≤ N → (∑ k, e k) ≤ N →
(∑ k, e k) = (∑ k, d k) →
MvPowerSeries.coeff (Finsupp.equivFunOnFinite.symm e)
(MvPolynomial.aeval phi
(MvPolynomial.monomial (Finsupp.equivFunOnFinite.symm d) (1 : Complex))) =
(if d = e then 1 else 0))
(value : (Fin n → Nat) → Complex)
(m : Nat)
(hm : m ≤ N)
(S : Finset (Fin n → Nat))
(hS : ∀ d : Fin n → Nat, d ∈ S ↔ (∑ k, d k) = m)
(e : Fin n → Nat)
(he : (∑ k, e k) ≤ m) :
MvPowerSeries.coeff (Finsupp.equivFunOnFinite.symm e)
(MvPolynomial.aeval phi
(∑ d ∈ S,
MvPolynomial.monomial (Finsupp.equivFunOnFinite.symm d) (value d))) =
(if (∑ k, e k) = m then value e else 0) := by sorrySource