feat(big_operators/intervals): lemma on dependent double sum (#6361)

src/algebra/big_operators/intervals.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 
 import algebra.big_operators.basic
 import data.finset.intervals
+import tactic.linarith
 
 
 /-!
@@ -70,6 +71,21 @@ lemma sum_Ico_eq_sub {δ : Type*} [add_comm_group δ] (f : ℕ → δ) {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
 
+/-- 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]
+  (a b : ℕ) (f : ℕ → ℕ → M) :
+  ∑ i in finset.Ico a b, ∑ j in finset.Ico i b, f i j =
+  ∑ j in finset.Ico a b, ∑ i in finset.Ico a (j+1), f i j :=
+begin
+  rw [finset.sum_sigma', finset.sum_sigma'],
+  refine finset.sum_bij'
+    (λ (x : Σ (i : ℕ), ℕ) _, (⟨x.2, x.1⟩ : Σ (i : ℕ), ℕ)) _ (λ _ _, rfl)
+    (λ (x : Σ (i : ℕ), ℕ) _, (⟨x.2, x.1⟩ : Σ (i : ℕ), ℕ)) _
+    (by rintro ⟨⟩ _; refl) (by rintro ⟨⟩ _; refl);
+  simp only [finset.Ico.mem, sigma.forall, finset.mem_sigma];
+  rintros a b ⟨⟨h₁,h₂⟩, ⟨h₃, h₄⟩⟩; refine ⟨⟨_, _⟩, ⟨_, _⟩⟩; linarith
+end
+
 @[to_additive]
 lemma prod_Ico_eq_prod_range (f : ℕ → β) (m n : ℕ) :
   (∏ k in Ico m n, f k) = (∏ k in range (n - m), f (m + k)) :=