feat(data/list): more lemmas on joins and sums (#2501)

A few more lemmas on lists (especially joins) and sums. I also linted the file `lists/basic.lean` and converted some comments to section headers.

Some lemmas got renamed:
`of_fn_prod_take` -> `prod_take_of_fn`
`of_fn_sum_take` -> `sum_take_of_fn`
`of_fn_prod` ->`prod_of_fn`
`of_fn_sum` -> `sum_of_fn`

The arguments of `nth_le_repeat` were changed for better `simp` efficiency

Author: sgouezel

src/algebra/big_operators.lean

@@ -7,6 +7,7 @@ Some big operators for lists and finite sets.
 -/
 import data.finset
 import data.nat.enat
+import tactic.omega
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -359,6 +360,18 @@ lemma prod_range_succ' (f : ℕ → β) :
 | (n + 1) := by rw [prod_range_succ (λ m, f (nat.succ m)), mul_assoc, ← prod_range_succ'];
                  exact prod_range_succ _ _
 
+/-- A telescoping sum along `{0, ..., n-1}` of an `ℕ`-valued function reduces to the difference of
+the last and first terms when the function we are summing is monotone. -/
+lemma sum_range_sub_of_monotone {f : ℕ → ℕ} (h : monotone f) (n : ℕ) :
+  (finset.range n).sum (λ i, f (i+1) - f i) = f n - f 0 :=
+begin
+  induction n with n IH, { simp },
+  rw [finset.sum_range_succ, IH, nat.succ_eq_add_one],
+  have : f n ≤ f (n+1) := h (nat.le_succ _),
+  have : f 0 ≤ f n := h (nat.zero_le _),
+  omega
+end
+
 lemma sum_Ico_add {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (m n k : ℕ) :
   (Ico m n).sum (λ l, f (k + l)) = (Ico (m + k) (n + k)).sum f :=
 Ico.image_add m n k ▸ eq.symm $ sum_image $ λ x hx y hy h, nat.add_left_cancel h

src/analysis/analytic/composition.lean

@@ -373,7 +373,7 @@ def comp_change_of_variables (N : ℕ) (i : Σ n, (fin n) → ℕ) (hi : i ∈ c
 begin
   rcases i with ⟨n, f⟩,
   rw mem_comp_partial_sum_source_iff at hi,
-  exact ⟨finset.univ.sum f, list.of_fn (λ a, ⟨f a, (hi.2 a).1⟩), by simp [list.of_fn_sum]⟩
+  exact ⟨finset.univ.sum f, list.of_fn (λ a, ⟨f a, (hi.2 a).1⟩), by simp [list.sum_of_fn]⟩
 end
 
 @[simp] lemma comp_change_of_variables_length

src/combinatorics/composition.lean

@@ -129,7 +129,7 @@ def blocks_fun : fin c.length → ℕ := λ i, nth_le c.blocks i.1 i.2
 
 lemma sum_blocks_fun : finset.univ.sum c.blocks_fun = n :=
 begin
-  conv_rhs { rw [← c.blocks_sum, ← of_fn_nth_le c.blocks, of_fn_sum] },
+  conv_rhs { rw [← c.blocks_sum, ← of_fn_nth_le c.blocks, sum_of_fn] },
   simp [blocks_fun, length],
   refl
 end

src/data/fintype/basic.lean

@@ -349,6 +349,9 @@ instance {α : Type*} (β : α → Type*)
   [fintype α] [∀ a, fintype (β a)] : fintype (sigma β) :=
 ⟨univ.sigma (λ _, univ), λ ⟨a, b⟩, by simp⟩
 
+@[simp] lemma finset.univ_sigma_univ {α : Type*} {β : α → Type*} [fintype α] [∀ a, fintype (β a)] :
+  (univ : finset α).sigma (λ a, (univ : finset (β a))) = univ := rfl
+
 instance (α β : Type*) [fintype α] [fintype β] : fintype (α × β) :=
 ⟨univ.product univ, λ ⟨a, b⟩, by simp⟩
 

src/data/fintype/card.lean

@@ -149,9 +149,32 @@ lemma fin.sum_pow_mul_eq_add_pow {n : ℕ} {R : Type*} [comm_semiring R] (a b :
   (a + b) ^ n :=
 by simpa using fintype.sum_pow_mul_eq_add_pow (fin n) a b
 
+/-- It is equivalent to sum a function over `fin n` or `finset.range n`. -/
+@[to_additive]
+lemma fin.prod_univ_eq_prod_range [comm_monoid α] (f : ℕ → α) (n : ℕ) :
+  finset.univ.prod (λ (i : fin n), f i.val) = (finset.range n).prod f :=
+begin
+  apply finset.prod_bij (λ (a : fin n) ha, a.val),
+  { assume a ha, simp [a.2] },
+  { assume a ha, refl },
+  { assume a b ha hb H, exact (fin.ext_iff _ _).2 H },
+  { assume b hb, exact ⟨⟨b, list.mem_range.mp hb⟩, finset.mem_univ _, rfl⟩, }
+end
+
+@[to_additive]
+lemma prod_equiv [fintype α] [fintype β] [comm_monoid γ] (e : α ≃ β) (f : β → γ) :
+  finset.univ.prod (f ∘ e) = finset.univ.prod f :=
+begin
+  apply prod_bij (λ i hi, e i) (λ i hi, mem_univ _) _ (λ a b _ _ h, e.injective h),
+  { assume b hb,
+    rcases e.surjective b with ⟨a, ha⟩,
+    exact ⟨a, mem_univ _, ha.symm⟩, },
+  { simp }
+end
+
 namespace list
 
-lemma of_fn_prod_take [comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
+lemma prod_take_of_fn [comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
   ((of_fn f).take i).prod = (finset.univ.filter (λ (j : fin n), j.val < i)).prod f :=
 begin
   have A : ∀ (j : fin n), ¬ (j.val < 0) := λ j, not_lt_bot,
@@ -177,9 +200,9 @@ begin
     simp [← A, B, IH] }
 end
 
--- `to_additive` does not work on `of_fn_prod_take` because of `0 : ℕ` in the proof. Copy-paste the
+-- `to_additive` does not work on `prod_take_of_fn` because of `0 : ℕ` in the proof. Copy-paste the
 -- proof instead...
-lemma of_fn_sum_take [add_comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
+lemma sum_take_of_fn [add_comm_monoid α] {n : ℕ} (f : fin n → α) (i : ℕ) :
   ((of_fn f).take i).sum = (finset.univ.filter (λ (j : fin n), j.val < i)).sum f :=
 begin
   have A : ∀ (j : fin n), ¬ (j.val < 0) := λ j, not_lt_bot,
@@ -205,13 +228,13 @@ begin
     simp [← A, B, IH] }
 end
 
-attribute [to_additive] of_fn_prod_take
+attribute [to_additive] prod_take_of_fn
 
 @[to_additive]
-lemma of_fn_prod [comm_monoid α] {n : ℕ} {f : fin n → α} :
+lemma prod_of_fn [comm_monoid α] {n : ℕ} {f : fin n → α} :
   (of_fn f).prod = finset.univ.prod f :=
 begin
-  convert of_fn_prod_take f n,
+  convert prod_take_of_fn f n,
   { rw [take_all_of_le (le_of_eq (length_of_fn f))] },
   { have : ∀ (j : fin n), j.val < n := λ j, j.2,
     simp [this] }