refactor(algebra/big_operators/finprod, ring_theory/hahn_series): summable families now use finsum (#7388)

Adds a few `finprod/finsum` lemmas
Uses them to refactor `hahn_series.summable_family` to use `finsum`

Author: awainverse

src/algebra/big_operators/finprod.lean

@@ -667,4 +667,37 @@ begin
   simp [hx]
 end
 
+@[to_additive] lemma finprod_prod_comm (s : finset β) (f : α → β → M)
+  (h : ∀ b ∈ s, (mul_support (λ a, f a b)).finite) :
+  ∏ᶠ a : α, ∏ b in s, f a b = ∏ b in s, ∏ᶠ a : α, f a b :=
+begin
+  have hU : mul_support (λ a, ∏ b in s, f a b) ⊆
+    (s.finite_to_set.bUnion (λ b hb, h b (finset.mem_coe.1 hb))).to_finset,
+  { rw finite.coe_to_finset,
+    intros x hx,
+    simp only [exists_prop, mem_Union, ne.def, mem_mul_support, finset.mem_coe],
+    contrapose! hx,
+    rw [mem_mul_support, not_not, finset.prod_congr rfl hx, finset.prod_const_one] },
+  rw [finprod_eq_prod_of_mul_support_subset _ hU, finset.prod_comm],
+  refine finset.prod_congr rfl (λ b hb, (finprod_eq_prod_of_mul_support_subset _ _).symm),
+  intros a ha,
+  simp only [finite.coe_to_finset, mem_Union],
+  exact ⟨b, hb, ha⟩
+end
+
+@[to_additive] lemma prod_finprod_comm (s : finset α) (f : α → β → M)
+  (h : ∀ a ∈ s, (mul_support (f a)).finite) :
+  ∏ a in s, ∏ᶠ b : β, f a b = ∏ᶠ b : β, ∏ a in s, f a b :=
+(finprod_prod_comm s (λ b a, f a b) h).symm
+
+lemma mul_finsum {R : Type*} [semiring R] (f : α → R) (r : R)
+  (h : (function.support f).finite) :
+  r * ∑ᶠ a : α, f a = ∑ᶠ a : α, r * f a :=
+(add_monoid_hom.mul_left r).map_finsum h
+
+lemma finsum_mul {R : Type*} [semiring R] (f : α → R) (r : R)
+  (h : (function.support f).finite) :
+  (∑ᶠ a : α, f a) * r = ∑ᶠ a : α, f a * r :=
+(add_monoid_hom.mul_right r).map_finsum h
+
 end type

src/ring_theory/hahn_series.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import order.well_founded_set
-import algebra.big_operators
+import algebra.big_operators.finprod
 import ring_theory.valuation.basic
 import algebra.module.pi
 import ring_theory.power_series.basic
@@ -743,8 +743,7 @@ variables (Γ) (R) [partial_order Γ] [add_comm_monoid R]
 structure summable_family (α : Type*) :=
 (to_fun : α → hahn_series Γ R)
 (is_pwo_Union_support' : set.is_pwo (⋃ (a : α), (to_fun a).support))
-(co_support : Γ → finset α)
-(mem_co_support' : ∀ (a : α) (g : Γ), a ∈ co_support g ↔ (to_fun a).coeff g ≠ 0)
+(finite_co_support' : ∀ (g : Γ), ({a | (to_fun a).coeff g ≠ 0}).finite)
 
 end
 
@@ -759,19 +758,15 @@ instance : has_coe_to_fun (summable_family Γ R α) :=
 lemma is_pwo_Union_support (s : summable_family Γ R α) : set.is_pwo (⋃ (a : α), (s a).support) :=
 s.is_pwo_Union_support'
 
-@[simp]
-lemma mem_co_support {s : summable_family Γ R α} {a : α} {g : Γ} :
-  a ∈ s.co_support g ↔ (s a).coeff g ≠ 0 := mem_co_support' _ _ _
+lemma finite_co_support (s : summable_family Γ R α) (g : Γ) :
+  (function.support (λ a, (s a).coeff g)).finite :=
+s.finite_co_support' g
 
 lemma coe_injective : @function.injective (summable_family Γ R α) (α → hahn_series Γ R) coe_fn
-| ⟨f1, hU1, c1, hc1⟩ ⟨f2, hU2, c2, hc2⟩ h :=
+| ⟨f1, hU1, hf1⟩ ⟨f2, hU2, hf2⟩ h :=
 begin
   change f1 = f2 at h,
   subst h,
-  simp only,
-  refine ⟨rfl, _⟩,
-  ext g a,
-  rw [hc1, hc2]
 end
 
 @[ext]
@@ -784,18 +779,16 @@ instance : has_add (summable_family Γ R α) :=
       rw ← set.Union_union_distrib,
       exact set.Union_subset_Union (λ a, support_add_subset)
     end),
-    co_support := λ g, ((x.co_support g) ∪ (y.co_support g)).filter
-      (λ a, (x a).coeff g + (y a).coeff g ≠ 0),
-    mem_co_support' := λ a g, begin
-      simp only [mem_union, mem_filter, mem_co_support, and_iff_right_iff_imp,
-        pi.add_apply, ne.def, add_coeff'],
-      contrapose!,
-      rintro ⟨hx, hy⟩,
-      simp [hx, hy],
+    finite_co_support' := λ g, ((x.finite_co_support g).union (y.finite_co_support g)).subset begin
+      intros a ha,
+      change (x a).coeff g + (y a).coeff g ≠ 0 at ha,
+      rw [set.mem_union, function.mem_support, function.mem_support],
+      contrapose! ha,
+      rw [ha.1, ha.2, add_zero]
     end }⟩
 
 instance : has_zero (summable_family Γ R α) :=
-⟨⟨0, by simp, λ _, ∅, by simp⟩⟩
+⟨⟨0, by simp, by simp⟩⟩
 
 instance : inhabited (summable_family Γ R α) := ⟨0⟩
 
@@ -820,46 +813,34 @@ instance : add_comm_monoid (summable_family Γ R α) :=
 /-- The infinite sum of a `summable_family` of Hahn series. -/
 def hsum (s : summable_family Γ R α) :
   hahn_series Γ R :=
-{ coeff := λ g, ∑ i in s.co_support g, (s i).coeff g,
+{ coeff := λ g, ∑ᶠ i, (s i).coeff g,
   is_pwo_support' := s.is_pwo_Union_support.mono (λ g, begin
     contrapose,
     rw [set.mem_Union, not_exists, function.mem_support, not_not],
     simp_rw [mem_support, not_not],
-    exact λ h, sum_eq_zero (λ a ha, h _),
+    intro h,
+    rw [finsum_congr h, finsum_zero],
   end) }
 
 @[simp]
 lemma hsum_coeff {s : summable_family Γ R α} {g : Γ} :
-  s.hsum.coeff g = ∑ i in s.co_support g, (s i).coeff g := rfl
+  s.hsum.coeff g = ∑ᶠ i, (s i).coeff g := rfl
 
 lemma support_hsum_subset {s : summable_family Γ R α} :
   s.hsum.support ⊆ ⋃ (a : α), (s a).support :=
 λ g hg, begin
-  rw [mem_support, hsum_coeff] at hg,
+  rw [mem_support, hsum_coeff, finsum_eq_sum _ (s.finite_co_support _)] at hg,
   obtain ⟨a, h1, h2⟩ := exists_ne_zero_of_sum_ne_zero hg,
   rw [set.mem_Union],
   exact ⟨a, h2⟩,
 end
 
-lemma co_support_add_subset {s t : summable_family Γ R α} {g : Γ} :
-  (s + t).co_support g ⊆ s.co_support g ∪ t.co_support g :=
-λ a ha, begin
-  rw mem_co_support at ha,
-  rw [mem_union, mem_co_support, mem_co_support],
-  contrapose! ha,
-  obtain ⟨hs, ht⟩ := ha,
-  simp [hs, ht],
-end
-
 @[simp]
 lemma hsum_add {s t : summable_family Γ R α} : (s + t).hsum = s.hsum + t.hsum :=
 begin
   ext g,
-  simp only [add_apply, pi.add_apply, hsum_coeff, ne.def, add_coeff'],
-  rw [sum_subset co_support_add_subset, finset.sum_add_distrib,
-    ← sum_subset (subset_union_left _ _), ← sum_subset (subset_union_right _ _)];
-  { intros x h1 h2,
-    rwa [mem_co_support, not_not] at h2, }
+  simp only [hsum_coeff, add_coeff, add_apply],
+  exact finsum_add_distrib (s.finite_co_support _) (t.finite_co_support _)
 end
 
 end add_comm_monoid
@@ -870,8 +851,8 @@ variables [partial_order Γ] [add_comm_group R] {α : Type*} {s t : summable_fam
 instance : add_comm_group (summable_family Γ R α) :=
 { neg := λ s, { to_fun := λ a, - s a,
     is_pwo_Union_support' := by { simp_rw [support_neg], exact s.is_pwo_Union_support' },
-    co_support := s.co_support,
-    mem_co_support' := by simp },
+    finite_co_support' := λ g, by { simp only [neg_coeff', pi.neg_apply, ne.def, neg_eq_zero],
+      exact s.finite_co_support g } },
   add_left_neg := λ a, by { ext, apply add_left_neg },
   .. summable_family.add_comm_monoid }
 
@@ -899,22 +880,15 @@ instance : has_scalar (hahn_series Γ R) (summable_family Γ R α) :=
       simp only [set.mem_Union, exists_imp_distrib],
       exact λ a ha, (set.add_subset_add (set.subset.refl _) (set.subset_Union _ a)) ha,
     end,
-    co_support := λ g, ((add_antidiagonal x.is_pwo_support s.is_pwo_Union_support g).bUnion
-      (λ ij, s.co_support ij.snd)).filter (λ a, (x * (s a)).coeff g ≠ 0),
-    mem_co_support' := λ a g, begin
-      rw [mem_filter],
-      apply and_iff_right_of_imp,
-      simp only [mem_bUnion, exists_prop, set.mem_Union, mem_add_antidiagonal, mem_co_support,
-        mul_coeff, ne.def, mem_support, is_pwo_support, prod.exists],
-      contrapose!,
-      intro h,
-      rw sum_eq_zero,
-      rintros ⟨i, j⟩ hij,
-      rw [mem_add_antidiagonal, mem_support] at hij,
-      by_cases he : ∃ (b : α), (s b).coeff j ≠ 0,
-      { rw [h i j ⟨hij.1, hij.2.1, he⟩, mul_zero] },
-      simp_rw [not_exists, ne.def, not_not] at he,
-      rw [he a, mul_zero],
+    finite_co_support' := λ g, begin
+      refine ((add_antidiagonal x.is_pwo_support s.is_pwo_Union_support g).finite_to_set.bUnion
+        (λ ij hij, _)).subset (λ a ha, _),
+      { exact λ ij hij, function.support (λ a, (s a).coeff ij.2) },
+      { apply s.finite_co_support },
+      { obtain ⟨i, j, hi, hj, rfl⟩ := support_mul_subset_add_support ha,
+        simp only [exists_prop, set.mem_Union, mem_add_antidiagonal,
+          mul_coeff, ne.def, mem_support, is_pwo_support, prod.exists],
+        refine ⟨i, j, mem_coe.2 (mem_add_antidiagonal.2 ⟨rfl, hi, set.mem_Union.2 ⟨a, hj⟩⟩), hj⟩, }
     end } }
 
 @[simp]
@@ -935,47 +909,31 @@ lemma hsum_smul {x : hahn_series Γ R} {s : summable_family Γ R α} :
   (x • s).hsum = x * s.hsum :=
 begin
   ext g,
-  rw [mul_coeff, sum_subset (add_antidiagonal_mono_right support_hsum_subset)],
-  { rw hsum_coeff,
-    have h : (x • s).co_support g ⊆ (add_antidiagonal x.is_pwo_support s.is_pwo_Union_support
-      g).bUnion (λ ij, s.co_support ij.snd),
-    { intros a ha,
-      rw [mem_co_support, smul_apply, mul_coeff] at ha,
-      obtain ⟨ij, h1, h2⟩ := exists_ne_zero_of_sum_ne_zero ha,
-      rw mem_bUnion,
-      exact ⟨ij, add_antidiagonal_mono_right (set.subset_Union _ a) h1,
-        mem_co_support.2 (right_ne_zero_of_mul h2)⟩ },
-    refine eq.trans (sum_subset h _) _,
-    { apply is_pwo_Union_support },
-    { intros a h1 h2,
-      contrapose! h2,
-      rw [mem_co_support],
-      exact h2 },
-    have h' : ∀ a, ((x • s) a).coeff g =
-      ∑ (ij : Γ × Γ) in add_antidiagonal x.is_pwo_support s.is_pwo_Union_support g,
-      x.coeff ij.fst * (s a).coeff ij.snd,
-    { intro a,
-      rw [smul_apply, mul_coeff],
-      apply sum_subset (add_antidiagonal_mono_right
-        (set.subset_Union (support ∘ s) a)),
-      intros ij h1 h2,
-      rw [mem_add_antidiagonal] at *,
-      have h : ¬ ij.snd ∈ (s a).support := λ c, h2 ⟨h1.1, h1.2.1, c⟩,
-      rw [mem_support, not_not] at h,
-      rw [h, mul_zero] },
-    rw [sum_congr rfl (λ a ha, h' a), sum_comm],
-    refine sum_congr rfl (λ ij hij, _),
-    rw [hsum_coeff, ← mul_sum],
-    apply congr rfl (sum_subset (subset_bUnion_of_mem _ hij) _).symm,
-    intros a h1 h2,
-    contrapose! h2,
-    rw [mem_co_support],
-    exact h2 },
-  { intros ij h1 h2,
+  simp only [mul_coeff, hsum_coeff, smul_apply],
+  have h : ∀ i, (s i).support ⊆ ⋃ j, (s j).support := set.subset_Union _,
+  refine (eq.trans (finsum_congr (λ a, _))
+    (finsum_sum_comm (add_antidiagonal x.is_pwo_support s.is_pwo_Union_support g)
+    (λ i ij, x.coeff (prod.fst ij) * (s i).coeff ij.snd) _)).trans _,
+  { refine sum_subset (add_antidiagonal_mono_right (set.subset_Union _ a)) _,
+    rintro ⟨i, j⟩ hU ha,
     rw mem_add_antidiagonal at *,
-    have h : ¬ ij.snd ∈ s.hsum.support := λ con, h2 ⟨h1.1, h1.2.1, con⟩,
-    rw [mem_support, not_not] at h,
-    simp [h] },
+    rw [not_not.1 (λ con, ha ⟨hU.1, hU.2.1, con⟩), mul_zero] },
+  { rintro ⟨i, j⟩ hij,
+    refine (s.finite_co_support j).subset _,
+    simp_rw [function.support_subset_iff', function.mem_support, not_not],
+    intros a ha,
+    rw [ha, mul_zero] },
+  { refine (sum_congr rfl _).trans (sum_subset (add_antidiagonal_mono_right _) _).symm,
+    { rintro ⟨i, j⟩ hij,
+      rw mul_finsum,
+      apply s.finite_co_support, },
+    { intros x hx,
+      simp only [set.mem_Union, ne.def, mem_support],
+      contrapose! hx,
+      simp [hx] },
+    { rintro ⟨i, j⟩ hU ha,
+      rw mem_add_antidiagonal at *,
+      rw [← hsum_coeff, not_not.1 (λ con, ha ⟨hU.1, hU.2.1, con⟩), mul_zero] } }
 end
 
 /-- The summation of a `summable_family` as a `linear_map`. -/
@@ -1003,31 +961,29 @@ def of_finsupp (f : α →₀ (hahn_series Γ R)) :
       have h : (λ i, (f i).support) a ≤ _ := le_sup haf,
       exact h ha,
     end,
-  co_support := λ g, f.support.filter (λ a, (f a).coeff g ≠ 0),
-  mem_co_support' := λ a g, begin
-    simp only [mem_filter, and_iff_right_iff_imp, finsupp.mem_support_iff, ne.def],
-    contrapose!,
-    intro h,
-    simp [h]
+  finite_co_support' := λ g, begin
+    refine f.support.finite_to_set.subset (λ a ha, _),
+    simp only [coeff.add_monoid_hom_apply, mem_coe, finsupp.mem_support_iff,
+    ne.def, function.mem_support],
+    contrapose! ha,
+    simp [ha]
   end }
 
 @[simp]
 lemma coe_of_finsupp {f : α →₀ (hahn_series Γ R)} : ⇑(summable_family.of_finsupp f) = f := rfl
 
-@[simp]
-lemma co_support_of_finsupp {f : α →₀ (hahn_series Γ R)} {g : Γ} :
-  (summable_family.of_finsupp f).co_support g = f.support.filter (λ a, (f a).coeff g ≠ 0) := rfl
-
 @[simp]
 lemma hsum_of_finsupp {f : α →₀ (hahn_series Γ R)} :
   (of_finsupp f).hsum = f.sum (λ a, id) :=
 begin
   ext g,
-  simp only [filter_congr_decidable, hsum_coeff, coe_of_finsupp, ne.def, co_support_of_finsupp],
-  rw [sum_filter_ne_zero],
-  simp_rw [← coeff.add_monoid_hom_apply],
-  rw ← add_monoid_hom.map_sum,
-  refl
+  simp only [hsum_coeff, coe_of_finsupp, finsupp.sum, ne.def],
+  simp_rw [← coeff.add_monoid_hom_apply, id.def],
+  rw [add_monoid_hom.map_sum, finsum_eq_sum_of_support_subset],
+  intros x h,
+  simp only [coeff.add_monoid_hom_apply, mem_coe, finsupp.mem_support_iff, ne.def],
+  contrapose! h,
+  simp [h]
 end
 
 end of_finsupp