feat(data/finsupp/big_operators): sum of finsupp and their support (#…

…15155)

With some additional API for pairwise on multisets and coerced lists
On the way to computable list-based polynomials





Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>

src/algebra/big_operators/basic.lean

@@ -57,6 +57,9 @@ protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1
   (⟨s, hs⟩ : finset α).prod f = (s.map f).prod :=
 rfl
 
+@[simp, to_additive] lemma prod_val [comm_monoid α] (s : finset α) : s.1.prod = s.prod id :=
+by rw [finset.prod, multiset.map_id]
+
 end finset
 
 /--
@@ -1017,7 +1020,7 @@ open multiset
 @[to_additive] lemma prod_multiset_map_count [decidable_eq α] (s : multiset α)
   {M : Type*} [comm_monoid M] (f : α → M) :
   (s.map f).prod = ∏ m in s.to_finset, (f m) ^ (s.count m) :=
-by { refine quot.induction_on s (λ l, _), simpa [prod_list_map_count l f] }
+by { refine quot.induction_on s (λ l, _), simp [prod_list_map_count l f] }
 
 @[to_additive]
 lemma prod_multiset_count [decidable_eq α] [comm_monoid α] (s : multiset α) :

src/data/finset/basic.lean

@@ -1879,6 +1879,7 @@ variables [decidable_eq α] {l l' : list α} {a : α}
 def to_finset (l : list α) : finset α := multiset.to_finset l
 
 @[simp] theorem to_finset_val (l : list α) : l.to_finset.1 = (l.dedup : multiset α) := rfl
+@[simp] theorem to_finset_coe (l : list α) : (l : multiset α).to_finset = l.to_finset := rfl
 
 lemma to_finset_eq (n : nodup l) : @finset.mk α l n = l.to_finset := multiset.to_finset_eq n
 

src/data/finset/lattice.lean

@@ -164,6 +164,14 @@ by { rw [comp_sup_eq_sup_comp coe]; intros; refl }
   (s.sup f).to_finset = s.sup (λ x, (f x).to_finset) :=
 comp_sup_eq_sup_comp multiset.to_finset to_finset_union rfl
 
+lemma _root_.list.foldr_sup_eq_sup_to_finset [decidable_eq α] (l : list α) :
+  l.foldr (⊔) ⊥ = l.to_finset.sup id :=
+begin
+  rw [←coe_fold_r, ←multiset.fold_dedup_idem, sup_def, ←list.to_finset_coe, to_finset_val,
+      multiset.map_id],
+  refl
+end
+
 theorem subset_range_sup_succ (s : finset ℕ) : s ⊆ range (s.sup id).succ :=
 λ n hn, mem_range.2 $ nat.lt_succ_of_le $ le_sup hn
 
@@ -362,6 +370,14 @@ lemma inf_coe {P : α → Prop}
   (@inf _ _ (subtype.semilattice_inf Pinf) (subtype.order_top Ptop) t f : α) = t.inf (λ x, f x) :=
 @sup_coe αᵒᵈ _ _ _ _ Ptop Pinf t f
 
+lemma _root_.list.foldr_inf_eq_inf_to_finset [decidable_eq α] (l : list α) :
+  l.foldr (⊓) ⊤ = l.to_finset.inf id :=
+begin
+  rw [←coe_fold_r, ←multiset.fold_dedup_idem, inf_def, ←list.to_finset_coe, to_finset_val,
+      multiset.map_id],
+  refl
+end
+
 lemma inf_induction {p : α → Prop} (ht : p ⊤) (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊓ a₂))
   (hs : ∀ b ∈ s, p (f b)) : p (s.inf f) :=
 @sup_induction αᵒᵈ _ _ _ _ _ _ ht hp hs

src/data/finset/pairwise.lean

@@ -8,7 +8,9 @@ import data.finset.lattice
 /-!
 # Relations holding pairwise on finite sets
 
-In this file we prove a few results about the interaction of `set.pairwise_disjoint` and `finset`.
+In this file we prove a few results about the interaction of `set.pairwise_disjoint` and `finset`,
+as well as the interaction of `list.pairwise disjoint` and the condition of
+`disjoint` on `list.to_finset`, in `set` form.
 -/
 
 open finset
@@ -62,3 +64,42 @@ begin
 end
 
 end set
+
+namespace list
+variables {β : Type*} [decidable_eq α] {r : α → α → Prop} {l : list α}
+
+lemma pairwise_of_coe_to_finset_pairwise (hl : (l.to_finset : set α).pairwise r) (hn : l.nodup) :
+  l.pairwise r :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  simp only [set.pairwise_insert, pairwise_cons, to_finset_cons, finset.coe_insert,
+             finset.mem_coe, mem_to_finset, ne.def, nodup_cons] at hl hn ⊢,
+  refine ⟨λ x hx, (hl.right x hx _).left, IH hl.left hn.right⟩,
+  rintro rfl,
+  exact hn.left hx
+end
+
+lemma pairwise_iff_coe_to_finset_pairwise (hn : l.nodup) (hs : symmetric r) :
+  (l.to_finset : set α).pairwise r ↔ l.pairwise r :=
+begin
+  refine ⟨λ h, pairwise_of_coe_to_finset_pairwise h hn, λ h, _⟩,
+  induction l with hd tl IH,
+  { simp },
+  simp only [set.pairwise_insert, to_finset_cons, finset.coe_insert, finset.mem_coe,
+             mem_to_finset, ne.def, pairwise_cons, nodup_cons] at hn h ⊢,
+  exact ⟨IH hn.right h.right, λ x hx hne, ⟨h.left _ hx, hs (h.left _ hx)⟩⟩
+end
+
+lemma pairwise_disjoint_of_coe_to_finset_pairwise_disjoint {α ι}
+  [semilattice_inf α] [order_bot α] [decidable_eq ι] {l : list ι} {f : ι → α}
+  (hl : (l.to_finset : set ι).pairwise_disjoint f) (hn : l.nodup) :
+  l.pairwise (_root_.disjoint on f) :=
+pairwise_of_coe_to_finset_pairwise hl hn
+
+lemma pairwise_disjoint_iff_coe_to_finset_pairwise_disjoint {α ι}
+  [semilattice_inf α] [order_bot α] [decidable_eq ι] {l : list ι} {f : ι → α} (hn : l.nodup) :
+  (l.to_finset : set ι).pairwise_disjoint f ↔ l.pairwise (_root_.disjoint on f) :=
+pairwise_iff_coe_to_finset_pairwise hn (symmetric_disjoint.comap f)
+
+end list

src/data/finsupp/big_operators.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2022 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+
+import data.finsupp.basic
+
+/-!
+
+# Sums of collections of finsupp, and their support
+This file provides results about the `finsupp.support` of sums of collections of `finsupp`,
+including sums of `list`, `multiset`, and `finset`.
+
+The support of the sum is a subset of the union of the supports:
+* `list.support_sum_subset`
+* `multiset.support_sum_subset`
+* `finset.support_sum_subset`
+
+The support of the sum of pairwise disjoint finsupps is equal to the union of the supports
+* `list.support_sum_eq`
+* `multiset.support_sum_eq`
+* `finset.support_sum_eq`
+
+Member in the support of the indexed union over a collection iff
+it is a member of the support of a member of the collection:
+* `list.mem_foldr_sup_support_iff`
+* `multiset.mem_sup_map_support_iff`
+* `finset.mem_sup_support_iff`
+
+-/
+
+variables {ι M : Type*} [decidable_eq ι]
+
+lemma list.support_sum_subset [add_monoid M] (l : list (ι →₀ M)) :
+  l.sum.support ⊆ l.foldr ((⊔) ∘ finsupp.support) ∅ :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  { simp only [list.sum_cons, list.foldr_cons, finset.union_comm],
+    refine finsupp.support_add.trans (finset.union_subset_union _ IH),
+    refl }
+end
+
+lemma multiset.support_sum_subset [add_comm_monoid M] (s : multiset (ι →₀ M)) :
+  s.sum.support ⊆ (s.map (finsupp.support)).sup :=
+begin
+  induction s using quot.induction_on,
+  simpa using list.support_sum_subset _
+end
+
+lemma finset.support_sum_subset [add_comm_monoid M] (s : finset (ι →₀ M)) :
+  (s.sum id).support ⊆ finset.sup s finsupp.support :=
+by { classical, convert multiset.support_sum_subset s.1; simp }
+
+lemma list.mem_foldr_sup_support_iff [has_zero M] {l : list (ι →₀ M)} {x : ι} :
+  x ∈ l.foldr ((⊔) ∘ finsupp.support) ∅ ↔ ∃ (f : ι →₀ M) (hf : f ∈ l), x ∈ f.support :=
+begin
+  simp only [finset.sup_eq_union, list.foldr_map, finsupp.mem_support_iff, exists_prop],
+  induction l with hd tl IH,
+  { simp },
+  { simp only [IH, list.foldr_cons, finset.mem_union, finsupp.mem_support_iff, list.mem_cons_iff],
+    split,
+    { rintro (h|h),
+      { exact ⟨hd, or.inl rfl, h⟩ },
+      { exact h.imp (λ f hf, hf.imp_left or.inr) } },
+    { rintro ⟨f, rfl|hf, h⟩,
+      { exact or.inl h },
+      { exact or.inr ⟨f, hf, h⟩ } } }
+end
+
+lemma multiset.mem_sup_map_support_iff [has_zero M] {s : multiset (ι →₀ M)} {x : ι} :
+  x ∈ (s.map (finsupp.support)).sup ↔ ∃ (f : ι →₀ M) (hf : f ∈ s), x ∈ f.support :=
+quot.induction_on s $ λ _, by simpa using list.mem_foldr_sup_support_iff
+
+lemma finset.mem_sup_support_iff [has_zero M] {s : finset (ι →₀ M)} {x : ι} :
+  x ∈ s.sup finsupp.support ↔ ∃ (f : ι →₀ M) (hf : f ∈ s), x ∈ f.support :=
+multiset.mem_sup_map_support_iff
+
+lemma list.support_sum_eq [add_monoid M] (l : list (ι →₀ M))
+  (hl : l.pairwise (disjoint on finsupp.support)) :
+  l.sum.support = l.foldr ((⊔) ∘ finsupp.support) ∅ :=
+begin
+  induction l with hd tl IH,
+  { simp },
+  { simp only [list.pairwise_cons] at hl,
+    simp only [list.sum_cons, list.foldr_cons, function.comp_app],
+    rw [finsupp.support_add_eq, IH hl.right, finset.sup_eq_union],
+    suffices : disjoint hd.support (tl.foldr ((⊔) ∘ finsupp.support) ∅),
+    { exact finset.disjoint_of_subset_right (list.support_sum_subset _) this },
+    { rw [←list.foldr_map, ←finset.bot_eq_empty, list.foldr_sup_eq_sup_to_finset],
+      rw finset.disjoint_sup_right,
+      intros f hf,
+      simp only [list.mem_to_finset, list.mem_map] at hf,
+      obtain ⟨f, hf, rfl⟩ := hf,
+      exact hl.left _ hf } }
+end
+
+lemma multiset.support_sum_eq [add_comm_monoid M] (s : multiset (ι →₀ M))
+  (hs : s.pairwise (disjoint on finsupp.support)) :
+  s.sum.support = (s.map finsupp.support).sup :=
+begin
+  induction s using quot.induction_on,
+  obtain ⟨l, hl, hd⟩ := hs,
+  convert list.support_sum_eq _ _,
+  { simp },
+  { simp },
+  { simp only [multiset.quot_mk_to_coe'', multiset.coe_map, multiset.coe_eq_coe] at hl,
+    exact hl.symm.pairwise hd (λ _ _ h, disjoint.symm h) }
+end
+
+lemma finset.support_sum_eq [add_comm_monoid M] (s : finset (ι →₀ M))
+  (hs : (s : set (ι →₀ M)).pairwise_disjoint finsupp.support) :
+  (s.sum id).support = finset.sup s finsupp.support :=
+begin
+  classical,
+  convert multiset.support_sum_eq s.1 _,
+  { exact (finset.sum_val _).symm },
+  { obtain ⟨l, hl, hn⟩ : ∃ (l : list (ι →₀ M)), l.to_finset = s ∧ l.nodup,
+    { refine ⟨s.to_list, _, finset.nodup_to_list _⟩,
+      simp },
+    subst hl,
+    rwa [list.to_finset_val, list.dedup_eq_self.mpr hn,
+        multiset.pairwise_coe_iff_pairwise,
+        ←list.pairwise_disjoint_iff_coe_to_finset_pairwise_disjoint hn],
+    intros x y hxy,
+    exact symmetric_disjoint hxy }
+end

src/data/list/perm.lean

@@ -891,6 +891,14 @@ suffices ∀ {l₁ l₂}, l₁ ~ l₂ → pairwise R l₁ → pairwise R l₂, f
     exact h _ (p'.symm.subset m) }
 end
 
+lemma pairwise.perm {R : α → α → Prop} {l l' : list α} (hR : l.pairwise R)
+  (hl : l ~ l') (hsymm : symmetric R) : l'.pairwise R :=
+(hl.pairwise_iff hsymm).mp hR
+
+lemma perm.pairwise {R : α → α → Prop} {l l' : list α}
+  (hl : l ~ l') (hR : l.pairwise R) (hsymm : symmetric R) : l'.pairwise R :=
+hR.perm hl hsymm
+
 theorem perm.nodup_iff {l₁ l₂ : list α} : l₁ ~ l₂ → (nodup l₁ ↔ nodup l₂) :=
 perm.pairwise_iff $ @ne.symm α
 

src/data/multiset/basic.lean

@@ -2218,6 +2218,13 @@ list. -/
 def pairwise (r : α → α → Prop) (m : multiset α) : Prop :=
 ∃l:list α, m = l ∧ l.pairwise r
 
+@[simp] lemma pairwise_nil (r : α → α → Prop) :
+  multiset.pairwise r 0 := ⟨[], rfl, list.pairwise.nil⟩
+
+lemma pairwise_coe_iff {r : α → α → Prop} {l : list α} :
+  multiset.pairwise r l ↔ ∃ l' : list α, l ~ l' ∧ l'.pairwise r :=
+exists_congr $ by simp
+
 lemma pairwise_coe_iff_pairwise {r : α → α → Prop} (hr : symmetric r) {l : list α} :
   multiset.pairwise r l ↔ l.pairwise r :=
 iff.intro

src/data/multiset/lattice.lean

@@ -21,6 +21,8 @@ variables [semilattice_sup α] [order_bot α]
 /-- Supremum of a multiset: `sup {a, b, c} = a ⊔ b ⊔ c` -/
 def sup (s : multiset α) : α := s.fold (⊔) ⊥
 
+@[simp] lemma sup_coe (l : list α) : sup (l : multiset α) = l.foldr (⊔) ⊥ := rfl
+
 @[simp] lemma sup_zero : (0 : multiset α).sup = ⊥ :=
 fold_zero _ _
 
@@ -80,6 +82,8 @@ variables [semilattice_inf α] [order_top α]
 /-- Infimum of a multiset: `inf {a, b, c} = a ⊓ b ⊓ c` -/
 def inf (s : multiset α) : α := s.fold (⊓) ⊤
 
+@[simp] lemma inf_coe (l : list α) : inf (l : multiset α) = l.foldr (⊓) ⊤ := rfl
+
 @[simp] lemma inf_zero : (0 : multiset α).inf = ⊤ :=
 fold_zero _ _
 

src/data/nat/factorization/basic.lean

@@ -74,7 +74,7 @@ by simp [factorization]
 
 /-- The support of `n.factorization` is exactly `n.factors.to_finset` -/
 @[simp] lemma support_factorization {n : ℕ} : n.factorization.support = n.factors.to_finset :=
-by simpa [factorization, multiset.to_finsupp_support]
+by simp [factorization, multiset.to_finsupp_support]
 
 lemma factor_iff_mem_factorization {n p : ℕ} : p ∈ n.factorization.support ↔ p ∈ n.factors :=
 by simp only [support_factorization, list.mem_to_finset]