chore(algebra/big_operators/intervals): Move and golf sum_range_sub_sum_range (#13359)

Move sum_range_sub_sum_range to a better file. Also implemented the golf demonstrated in this paper https://arxiv.org/pdf/2202.01344.pdf from @spolu.

Author: BoltonBailey

src/algebra/big_operators/intervals.lean

@@ -81,9 +81,22 @@ lemma prod_Ico_eq_mul_inv {δ : Type*} [comm_group δ] (f : ℕ → δ) {m n : 
   (∏ k in Ico m n, f k) = (∏ k in range n, f k) * (∏ k in range m, f k)⁻¹ :=
 eq_mul_inv_iff_mul_eq.2 $ by rw [mul_comm]; exact prod_range_mul_prod_Ico f h
 
-lemma sum_Ico_eq_sub {δ : Type*} [add_comm_group δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
-  (∑ k in Ico m n, f k) = (∑ k in range n, f k) - (∑ k in range m, f k) :=
-by simpa only [sub_eq_add_neg] using sum_Ico_eq_add_neg f h
+@[to_additive]
+lemma prod_Ico_eq_div {δ : Type*} [comm_group δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
+  (∏ k in Ico m n, f k) = (∏ k in range n, f k) / (∏ k in range m, f k) :=
+by simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h
+
+@[to_additive]
+lemma prod_range_sub_prod_range {α : Type*} [comm_group α] {f : ℕ → α}
+  {n m : ℕ} (hnm : n ≤ m) : (∏ k in range m, f k) / (∏ k in range n, f k) =
+  ∏ k in (range m).filter (λ k, n ≤ k), f k :=
+begin
+  rw [← prod_Ico_eq_div f hnm],
+  congr,
+  apply finset.ext,
+  simp only [mem_Ico, mem_filter, mem_range, *],
+  tauto,
+end
 
 /-- The two ways of summing over `(i,j)` in the range `a<=i<=j<b` are equal. -/
 lemma sum_Ico_Ico_comm {M : Type*} [add_comm_monoid M]

src/data/complex/exponential.lean

@@ -197,20 +197,6 @@ by rw [sum_sigma', sum_sigma']; exact sum_bij
     mem_range.2 (nat.lt_succ_of_le (nat.le_add_left _ _))⟩,
   sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (add_tsub_cancel_right _ _).symm⟩⟩⟩)
 
--- TODO move to src/algebra/big_operators/basic.lean, rewrite with comm_group, and make to_additive
-lemma sum_range_sub_sum_range {α : Type*} [add_comm_group α] {f : ℕ → α}
-  {n m : ℕ} (hnm : n ≤ m) : ∑ k in range m, f k - ∑ k in range n, f k =
-  ∑ k in (range m).filter (λ k, n ≤ k), f k :=
-begin
-  rw [← sum_sdiff (@filter_subset _ (λ k, n ≤ k) _ (range m)),
-    sub_eq_iff_eq_add, ← eq_sub_iff_add_eq, add_sub_cancel'],
-  refine finset.sum_congr
-    (finset.ext $ λ a, ⟨λ h, by simp at *; tauto,
-    λ h, have ham : a < m := lt_of_lt_of_le (mem_range.1 h) hnm,
-      by simp * at *⟩)
-    (λ _ _, rfl),
-end
-
 end
 
 section no_archimedean