English
If the constantCoeff of f is nilpotent of index m, then for d with degree constraint, coeff d (f^n) = 0 for n large enough: there is a bound n ≥ m + deg(d) with coeff zero.
Русский
Если константный коэффициент f^m равен нулю, то для данного d существует порог n ≥ m + deg(d), после которого coeff d (f^n) = 0.
LaTeX
$$$\\text{If } (\\operatorname{constantCoeff} f)^m = 0 \\text{ then } \\operatorname{coeff}_d(f^n) = 0 \\text{ for } n \\ge m + \\deg(d).$$$
Lean4
/-- Vanishing of coefficients of powers of multivariate power series
when the constant coefficient is nilpotent
[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, proposition 3][bourbaki1981] -/
theorem coeff_eq_zero_of_constantCoeff_nilpotent {f : MvPowerSeries σ R} {m : ℕ} (hf : constantCoeff f ^ m = 0)
{d : σ →₀ ℕ} {n : ℕ} (hn : m + degree d ≤ n) : coeff d (f ^ n) = 0 := by
classical
rw [coeff_pow]
apply sum_eq_zero
intro k hk
rw [mem_finsuppAntidiag] at hk
set s := {i ∈ range n | k i = 0} with hs_def
have hs : s ⊆ range n := filter_subset _ _
have hs' (i : ℕ) (hi : i ∈ s) : coeff (k i) f = constantCoeff f :=
by
simp only [hs_def, mem_filter] at hi
rw [hi.2, coeff_zero_eq_constantCoeff]
have hs'' (i : ℕ) (hi : i ∈ s) : k i = 0 :=
by
simp only [hs_def, mem_filter] at hi
rw [hi.2]
rw [← prod_sdiff (s₁ := s) (filter_subset _ _)]
apply mul_eq_zero_of_right
rw [prod_congr rfl hs', prod_const]
suffices m ≤ #s by
obtain ⟨m', hm'⟩ := Nat.exists_eq_add_of_le this
rw [hm', pow_add, hf, zero_mul]
rw [← Nat.add_le_add_iff_right, add_comm #s, Finset.card_sdiff_add_card_eq_card (filter_subset _ _), card_range]
apply le_trans _ hn
simp only [add_comm m, Nat.add_le_add_iff_right, ← hk.1, ← sum_sdiff (hs), sum_eq_zero (s := s) hs'', add_zero]
rw [← hs_def]
convert Finset.card_nsmul_le_sum (range n \ s) (fun x ↦ degree (k x)) 1 _
· simp only [Algebra.id.smul_eq_mul, mul_one]
· simp only [degree_eq_weight_one, map_sum]
· simp only [hs_def, mem_filter, mem_sdiff, mem_range, not_and, and_imp]
intro i hi hi'
rw [← not_lt, Nat.lt_one_iff, degree_eq_zero_iff]
exact hi' hi
