feat(RingTheory/PowerSeries/Basic): coeff of products (#9309)

* Use the class `HasPiAntidiagonal` defined in PR #7904 to compute the coefficients of products of power series (in several or one variable) : `MvPowerSeries.coeff_prod` and `PowerSeries.coeff_prod`
* Update the file `Archive/Partition.lean` accordingly

Co-author : Maria Ines de Frutos Fernandez

Based on work of Bhavik Mehta in `Archive/Partition.lean`



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

Archive/Wiedijk100Theorems/Partition.lean

@@ -10,6 +10,7 @@ import Mathlib.Data.Finset.NatAntidiagonal
 import Mathlib.Data.Fin.Tuple.NatAntidiagonal
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.ApplyFun
+import Mathlib.Data.Finset.PiAntidiagonal
 
 #align_import wiedijk_100_theorems.partition from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"
 
@@ -91,140 +92,10 @@ def partialDistinctGF (m : ℕ) [CommSemiring α] :=
   ∏ i in range m, (1 + (X : PowerSeries α) ^ (i + 1))
 #align theorems_100.partial_distinct_gf Theorems100.partialDistinctGF
 
-/--
-Functions defined only on `s`, which sum to `n`. In other words, a partition of `n` indexed by `s`.
-Every function in here is finitely supported, and the support is a subset of `s`.
-This should be thought of as a generalisation of `Finset.Nat.antidiagonalTuple` where
-`antidiagonalTuple k n` is the same thing as `cut (s : Finset.univ (Fin k)) n`.
--/
-def cut {ι : Type*} (s : Finset ι) (n : ℕ) : Finset (ι → ℕ) :=
-  Finset.filter (fun f => s.sum f = n)
-    ((s.pi fun _ => range (n + 1)).map
-      ⟨fun f i => if h : i ∈ s then f i h else 0, fun f g h => by
-        ext i hi; simpa [dif_pos hi] using congr_fun h i⟩)
-#align theorems_100.cut Theorems100.cut
-
-theorem mem_cut {ι : Type*} (s : Finset ι) (n : ℕ) (f : ι → ℕ) :
-    f ∈ cut s n ↔ s.sum f = n ∧ ∀ i, i ∉ s → f i = 0 := by
-  rw [cut, mem_filter, and_comm, and_congr_right]
-  intro h
-  simp only [mem_map, exists_prop, Function.Embedding.coeFn_mk, mem_pi]
-  constructor
-  · rintro ⟨_, _, rfl⟩ _ H
-    simp [dif_neg H]
-  · intro hf
-    refine' ⟨fun i _ => f i, fun i hi => _, _⟩
-    · rw [mem_range, Nat.lt_succ_iff, ← h]
-      apply single_le_sum _ hi
-      simp
-    · ext x
-      rw [dite_eq_ite, ite_eq_left_iff, eq_comm]
-      exact hf x
-#align theorems_100.mem_cut Theorems100.mem_cut
-
-theorem cut_equiv_antidiag (n : ℕ) :
-    Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (cut univ n) = antidiagonal n := by
-  ext ⟨x₁, x₂⟩
-  simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk, ←
-    Equiv.eq_symm_apply]
-  simp [mem_cut, add_comm]
-#align theorems_100.cut_equiv_antidiag Theorems100.cut_equiv_antidiag
-
-theorem cut_univ_fin_eq_antidiagonalTuple (n : ℕ) (k : ℕ) :
-    cut univ n = Nat.antidiagonalTuple k n := by ext; simp [Nat.mem_antidiagonalTuple, mem_cut]
-#align theorems_100.cut_univ_fin_eq_antidiagonal_tuple Theorems100.cut_univ_fin_eq_antidiagonalTuple
-
-/-- There is only one `cut` of 0. -/
-@[simp]
-theorem cut_zero {ι : Type*} (s : Finset ι) : cut s 0 = {0} := by
-  -- In general it's nice to prove things using `mem_cut` but in this case it's easier to just
-  -- use the definition.
-  rw [cut, range_one, pi_const_singleton, map_singleton, Function.Embedding.coeFn_mk,
-    filter_singleton, if_pos, singleton_inj]
-  · ext; split_ifs <;> rfl
-  rw [sum_eq_zero_iff]
-  intro x hx
-  apply dif_pos hx
-#align theorems_100.cut_zero Theorems100.cut_zero
-
-@[simp]
-theorem cut_empty_succ {ι : Type*} (n : ℕ) : cut (∅ : Finset ι) (n + 1) = ∅ := by
-  apply eq_empty_of_forall_not_mem
-  intro x hx
-  rw [mem_cut, sum_empty] at hx
-  cases hx.1
-#align theorems_100.cut_empty_succ Theorems100.cut_empty_succ
-
-theorem cut_insert {ι : Type*} (n : ℕ) (a : ι) (s : Finset ι) (h : a ∉ s) :
-    cut (insert a s) n =
-      (antidiagonal n).biUnion fun p : ℕ × ℕ =>
-        (cut s p.snd).map
-          ⟨fun f => f + fun t => if t = a then p.fst else 0, add_left_injective _⟩ := by
-  ext f
-  rw [mem_cut, mem_biUnion, sum_insert h]
-  constructor
-  · rintro ⟨rfl, h₁⟩
-    simp only [exists_prop, Function.Embedding.coeFn_mk, mem_map, mem_antidiagonal, Prod.exists]
-    refine' ⟨f a, s.sum f, rfl, fun i => if i = a then 0 else f i, _, _⟩
-    · rw [mem_cut]
-      refine' ⟨_, _⟩
-      · rw [sum_ite]
-        have : filter (fun x => x ≠ a) s = s := by
-          apply filter_true_of_mem
-          rintro i hi rfl
-          apply h hi
-        simp [this]
-      · intro i hi
-        rw [ite_eq_left_iff]
-        intro hne
-        apply h₁
-        simp [not_or, hne, hi]
-    · ext x
-      obtain rfl | h := eq_or_ne x a
-      · simp
-      · simp [if_neg h]
-  · simp only [mem_insert, Function.Embedding.coeFn_mk, mem_map, mem_antidiagonal, Prod.exists,
-      exists_prop, mem_cut, not_or]
-    rintro ⟨p, q, rfl, g, ⟨rfl, hg₂⟩, rfl⟩
-    refine' ⟨_, _⟩
-    · simp [sum_add_distrib, if_neg h, hg₂ _ h, add_comm]
-    · rintro i ⟨h₁, h₂⟩
-      simp [if_neg h₁, hg₂ _ h₂]
-#align theorems_100.cut_insert Theorems100.cut_insert
-
-theorem coeff_prod_range [CommSemiring α] {ι : Type*} (s : Finset ι) (f : ι → PowerSeries α)
-    (n : ℕ) : coeff α n (∏ j in s, f j) = ∑ l in cut s n, ∏ i in s, coeff α (l i) (f i) := by
-  revert n
-  induction s using Finset.induction_on with
-  | empty =>
-    rintro ⟨_ | n⟩
-    · simp
-    simp [cut_empty_succ, if_neg (Nat.succ_ne_zero _)]
-  | @insert a s hi ih =>
-    intro n
-    rw [cut_insert _ _ _ hi, prod_insert hi, coeff_mul, sum_biUnion]
-    · congr with i
-      simp only [sum_map, Pi.add_apply, Function.Embedding.coeFn_mk, prod_insert hi, if_pos rfl, ih,
-        mul_sum]
-      apply sum_congr rfl _
-      intro x hx
-      rw [mem_cut] at hx
-      rw [hx.2 a hi, zero_add]
-      congr 1
-      apply prod_congr rfl
-      intro k hk
-      rw [if_neg, add_zero]
-      exact ne_of_mem_of_not_mem hk hi
-    · simp only [Set.PairwiseDisjoint, Set.Pairwise, Prod.forall, not_and, Ne.def,
-        mem_antidiagonal, disjoint_left, mem_map, exists_prop, Function.Embedding.coeFn_mk,
-        exists_imp, not_exists, Finset.mem_coe, Function.onFun, mem_cut, and_imp]
-      rintro p₁ q₁ rfl p₂ q₂ h t x p hp _ hp3 q hq _ hq3
-      have z := hp3.trans hq3.symm
-      have := sum_congr (Eq.refl s) fun x _ => Function.funext_iff.1 z x
-      obtain rfl : q₁ = q₂ := by simpa [sum_add_distrib, hp, hq, if_neg hi] using this
-      obtain rfl : p₂ = p₁ := by simpa using h
-      exact (t rfl).elim
-#align theorems_100.coeff_prod_range Theorems100.coeff_prod_range
+open Finset.HasAntidiagonal Finset
+
+universe u
+variable {ι : Type u}
 
 /-- A convenience constructor for the power series whose coefficients indicate a subset. -/
 def indicatorSeries (α : Type*) [Semiring α] (s : Set ℕ) : PowerSeries α :=
@@ -315,53 +186,74 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
           ((univ : Finset (Nat.Partition n)).filter fun p =>
             (∀ j, p.parts.count j ∈ c j) ∧ ∀ j ∈ p.parts, j ∈ s) :
         α) =
-      (coeff α n) (∏ i : ℕ in s, indicatorSeries α ((· * i) '' c i)) := by
-  simp_rw [coeff_prod_range, coeff_indicator, prod_boole, sum_boole]
-  congr 1
-  refine' Finset.card_congr (fun p _ i => Multiset.count i p.parts • i) _ _ _
-  · simp only [mem_filter, mem_cut, mem_univ, true_and_iff, exists_prop, and_assoc, and_imp,
-      smul_eq_zero, Function.Embedding.coeFn_mk, exists_imp]
-    rintro ⟨p, hp₁, hp₂⟩ hp₃ hp₄
-    dsimp only at *
-    refine' ⟨_, _, _⟩
-    · rw [← hp₂, ←
-        sum_multiset_count_of_subset p s fun x hx => hp₄ _ (Multiset.mem_toFinset.mp hx)]
-    · intro i hi
-      left
-      exact Multiset.count_eq_zero_of_not_mem (mt (hp₄ i) hi)
-    · exact fun i _ => ⟨_, hp₃ i, rfl⟩
+      (coeff α n) (∏ i in s, indicatorSeries α ((· * i) '' c i)) := by
+  simp_rw [coeff_prod, coeff_indicator, prod_boole, sum_boole]
+  apply congr_arg
+  simp only [mem_univ, forall_true_left, not_and, not_forall, exists_prop,
+    Set.mem_image, not_exists]
+  set φ : (a : Nat.Partition n) →
+    a ∈ filter (fun p ↦ (∀ (j : ℕ), Multiset.count j p.parts ∈ c j) ∧ ∀ j ∈ p.parts, j ∈ s) univ →
+    ℕ →₀ ℕ := fun p _ => {
+      toFun := fun i => Multiset.count i p.parts • i
+      support := Finset.filter (fun i => i ≠ 0) p.parts.toFinset
+      mem_support_toFun := fun a => by
+        simp only [smul_eq_mul, ne_eq, mul_eq_zero, Multiset.count_eq_zero]
+        rw [not_or, not_not]
+        simp only [Multiset.mem_toFinset, not_not, mem_filter] }
+  refine' Finset.card_congr φ _ _ _
+  · intro a  ha
+    simp only [not_forall, not_exists, not_and, exists_prop, mem_filter]
+    rw [mem_piAntidiagonal']
+    dsimp only [ne_eq, smul_eq_mul, id_eq, eq_mpr_eq_cast, le_eq_subset, Finsupp.coe_mk]
+    simp only [mem_univ, forall_true_left, not_and, not_forall, exists_prop,
+      mem_filter, true_and] at ha
+    constructor
+    constructor
+    · intro i
+      simp only [ne_eq, Multiset.mem_toFinset, not_not, mem_filter, and_imp]
+      exact fun hi _ => ha.2 i hi
+    · conv_rhs => simp [← a.parts_sum]
+      rw [sum_multiset_count_of_subset _ s]
+      simp only [smul_eq_mul]
+      · intro i
+        simp only [Multiset.mem_toFinset, not_not, mem_filter]
+        apply ha.2
+    · exact fun i _ => ⟨Multiset.count i a.parts, ha.1 i, rfl⟩
   · dsimp only
     intro p₁ p₂ hp₁ hp₂ h
     apply Nat.Partition.ext
     simp only [true_and_iff, mem_univ, mem_filter] at hp₁ hp₂
     ext i
-    rw [Function.funext_iff] at h
-    specialize h i
-    match i with
-    | 0 =>
+    simp only [ne_eq, Multiset.mem_toFinset, not_not, smul_eq_mul, Finsupp.mk.injEq] at h
+    by_cases hi : i = 0
+    · rw [hi]
       rw [Multiset.count_eq_zero_of_not_mem]
       rw [Multiset.count_eq_zero_of_not_mem]
       intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a))
       intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₁.2 0 a))
-    | .succ i =>
-      rwa [Nat.nsmul_eq_mul, Nat.nsmul_eq_mul, mul_left_inj' i.succ_ne_zero] at h
-  · simp only [mem_filter, mem_cut, mem_univ, exists_prop, true_and_iff, and_assoc]
-    rintro f ⟨hf₁, hf₂, hf₃⟩
+    · rw [← mul_left_inj' hi]
+      rw [Function.funext_iff] at h
+      exact h.2 i
+  · simp only [mem_filter, mem_piAntidiagonal, mem_univ, exists_prop, true_and_iff, and_assoc]
+    rintro f ⟨hf, hf₃, hf₄⟩
+    suffices hf' : f ∈ piAntidiagonal s n
+    simp only [mem_piAntidiagonal'] at hf'
     refine' ⟨⟨∑ i in s, Multiset.replicate (f i / i) i, _, _⟩, _, _, _⟩
     · intro i hi
       simp only [exists_prop, mem_sum, mem_map, Function.Embedding.coeFn_mk] at hi
       rcases hi with ⟨t, ht, z⟩
       apply hs
       rwa [Multiset.eq_of_mem_replicate z]
-    · simp_rw [Multiset.sum_sum, Multiset.sum_replicate, Nat.nsmul_eq_mul, ← hf₁]
+    · simp_rw [Multiset.sum_sum, Multiset.sum_replicate, Nat.nsmul_eq_mul]
+      rw [← hf'.2]
       refine' sum_congr rfl fun i hi => Nat.div_mul_cancel _
-      rcases hf₃ i hi with ⟨w, _, hw₂⟩
+      rcases hf₄ i hi with ⟨w, _, hw₂⟩
       rw [← hw₂]
       exact dvd_mul_left _ _
     · intro i
       simp_rw [Multiset.count_sum', Multiset.count_replicate, sum_ite_eq]
       split_ifs with h
-      · rcases hf₃ i h with ⟨w, hw₁, hw₂⟩
+      · rcases hf₄ i h with ⟨w, hw₁, hw₂⟩
         rwa [← hw₂, Nat.mul_div_cancel _ (hs i h)]
       · exact hc _ h
     · intro i hi
@@ -370,11 +262,16 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ)
       rwa [Multiset.eq_of_mem_replicate hj₂]
     · ext i
       simp_rw [Multiset.count_sum', Multiset.count_replicate, sum_ite_eq]
+      simp only [ne_eq, Multiset.mem_toFinset, not_not, smul_eq_mul, ite_mul,
+        zero_mul, Finsupp.coe_mk]
       split_ifs with h
       · apply Nat.div_mul_cancel
-        rcases hf₃ i h with ⟨w, _, hw₂⟩
+        rcases hf₄ i h with ⟨w, _, hw₂⟩
         apply Dvd.intro_left _ hw₂
-      · rw [zero_smul, hf₂ i h]
+      · apply symm
+        rw [← Finsupp.not_mem_support_iff]
+        exact not_mem_mono hf h
+    · exact mem_piAntidiagonal.mpr ⟨hf, hf₃⟩
 #align theorems_100.partial_gf_prop Theorems100.partialGF_prop
 
 theorem partialOddGF_prop [Field α] (n m : ℕ) :

Mathlib/Data/Finsupp/Defs.lean

@@ -1062,6 +1062,11 @@ noncomputable def _root_.AddEquiv.finsuppUnique {ι : Type*} [Unique ι] :
   __ := Equiv.finsuppUnique
   map_add' _ _ := rfl
 
+  lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
+      AddEquiv.finsuppUnique.symm d = single () d := by
+  rw [Finsupp.unique_single (AddEquiv.finsuppUnique.symm d), Finsupp.unique_single_eq_iff]
+  rfl
+
 instance instIsRightCancelAdd [IsRightCancelAdd M] : IsRightCancelAdd (α →₀ M) where
   add_right_cancel _ _ _ h := ext fun x => add_right_cancel <| DFunLike.congr_fun h x
 

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -11,6 +11,7 @@ import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.RingTheory.Ideal.LocalRing
 import Mathlib.RingTheory.Multiplicity
 import Mathlib.Tactic.Linarith
+import Mathlib.Data.Finset.PiAntidiagonal
 
 #align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60"
 
@@ -812,6 +813,50 @@ set_option linter.uppercaseLean3 false in
 
 end Semiring
 
+section CommSemiring
+
+open Finset.HasAntidiagonal Finset
+
+variable {R : Type*} [CommSemiring R] {ι : Type*} [DecidableEq ι]
+
+/-- Coefficients of a product of power series -/
+theorem coeff_prod [DecidableEq σ]
+    (f : ι → MvPowerSeries σ R) (d : σ →₀ ℕ) (s : Finset ι) :
+    coeff R d (∏ j in s, f j) =
+      ∑ l in piAntidiagonal s d,
+        ∏ i in s, coeff R (l i) (f i) := by
+  induction s using Finset.induction_on generalizing d with
+  | empty =>
+    simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, piAntidiagonal_empty]
+    split_ifs
+    · simp only [card_singleton, Nat.cast_one]
+    · simp only [card_empty, Nat.cast_zero]
+  | @insert a s ha ih =>
+    rw [piAntidiagonal_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
+    · apply Finset.sum_congr rfl
+      · simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
+        rintro u v rfl
+        rw [ih, Finset.mul_sum, ← Finset.sum_attach]
+        apply Finset.sum_congr rfl
+        simp only [mem_attach, Finset.prod_insert ha, Function.update_same, forall_true_left,
+          Subtype.forall]
+        rintro x -
+        rw [Finset.prod_congr rfl]
+        intro i hi
+        rw [Function.update_noteq]
+        exact ne_of_mem_of_not_mem hi ha
+    · simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
+        disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
+        exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
+        Prod.forall, Prod.mk.injEq]
+      rintro u v rfl u' v' huv h k - l - hkl
+      obtain rfl : u' = u := by
+        simpa only [Finsupp.coe_update, Function.update_same] using DFunLike.congr_fun hkl a
+      simp only [add_right_inj] at huv
+      exact h rfl huv.symm
+
+end CommSemiring
+
 section Ring
 
 variable [Ring R]
@@ -2014,6 +2059,28 @@ set_option linter.uppercaseLean3 false in
 
 end Ring
 
+section CommSemiring
+
+open Finset.HasAntidiagonal Finset
+
+variable {R : Type*} [CommSemiring R] {ι : Type*} [DecidableEq ι]
+
+/-- Coefficients of a product of power series -/
+theorem coeff_prod (f : ι → PowerSeries R) (d : ℕ) (s : Finset ι) :
+    coeff R d (∏ j in s, f j) = ∑ l in piAntidiagonal s d, ∏ i in s, coeff R (l i) (f i) := by
+  simp only [coeff]
+  convert MvPowerSeries.coeff_prod _ _ _
+  rw [← AddEquiv.finsuppUnique_symm d, ← mapRange_piAntidiagonal_eq, sum_map, sum_congr rfl]
+  intro x _
+  apply prod_congr rfl
+  intro i _
+  congr 2
+  simp only [AddEquiv.toEquiv_eq_coe, Finsupp.mapRange.addEquiv_toEquiv, AddEquiv.toEquiv_symm,
+    Equiv.coe_toEmbedding, Finsupp.mapRange.equiv_apply, AddEquiv.coe_toEquiv_symm,
+    Finsupp.mapRange_apply, AddEquiv.finsuppUnique_symm]
+
+end CommSemiring
+
 section CommRing
 
 variable {A : Type*} [CommRing A]