Finset.sum where term takes finite number of values

Stream: new members

[Sabbir Rahman]

Suppose I have a fisnet.sum where the term I'm summig takes a small number of values. The best example of this is modulo. What theorems can I apply to simplify those expressions. For example how to prove following

import Mathlib

example (n : ℕ) : ∑ i ∈ Finset.range (5 * n), i % 5 = 10 * n := by
  sorry

I searched a bit, but couldn't find anything good. There are things like filter and some relations to List.sum. But honestly, I am kind of lost. And although this particular example is about modulo, but I am searching for something generic that'll work when the term I'm summing takes finitely many values.

[Kyle Miller]

What kind of argument are you expecting here? It might be a finite sum, but the sum's range depends on an unknown parameter n, so it's not like you can expand out the sum and evaluate.

[Edward van de Meent]

maybe induction, then splitting the sum in two pieces?

[Sabbir Rahman]

Kyle Miller said:

What kind of argument are you expecting here? It might be a finite sum, but the sum's range depends on an unknown parameter n, so it's not like you can expand out the sum and evaluate.

something like sum of f(i) over i = sum of x * count(x) over x, where x is a possible value of f(i) and count(x) is number of times x appears as f(i)

[Sabbir Rahman]

induction is indeed a good idea for the mod case, thanks

[Kyle Miller]

I see, you want to sum over the "fibers" of i % 5. That terminology is used sometimes in mathlib; maybe there's something relevant.

[Edward van de Meent]

@loogle Finset.sum, "fiber"

[loogle]

:search: Finset.card_eq_sum_card_fiberwise, Finset.sum_fiberwise, and 27 more

[Edward van de Meent]

docs#Finset.sum_fiberwise_of_maps_to in particular seems useful

[Kyle Miller]

This is getting sort of close:

example (n : ℕ) : ∑ i ∈ Finset.range (5 * n), i % 5 = 10 * n := by
  have := Finset.sum_fiberwise
            (f := fun i : ℕ => i % 5) (g := fun i : ℕ => (i : ZMod 5)) (s := Finset.range (5 * n))
  rw [← this]
  simp only [Finset.sum_filter]
  convert_to ∑ (j : ZMod 5), ∑ i ∈ Finset.range (5 * n), (if (i : ZMod 5) = j then j.1 else 0) = _
    using 4 with _ _ _ _ rfl
  -- ⊢ (∑ j, ∑ i ∈ Finset.range (5 * n), if ↑i = j then ↑j else 0) = 10 * n
  sorry

[Kyle Miller]

Finset.sum_fiberwise_of_maps_to looks more promising

[Kyle Miller]

example (n : ℕ) : ∑ i ∈ Finset.range (5 * n), i % 5 = 10 * n := by
  have := Finset.sum_fiberwise_of_maps_to (t := Finset.range 5)
    (f := fun i : ℕ => i % 5) (g := fun i : ℕ => i % 5) (s := Finset.range (5 * n))
  rw [← this]
  simp only [Finset.sum_range_succ, Finset.range_one, Finset.sum_singleton]
  simp +contextual only [Finset.sum_filter,
    ite_self, Finset.sum_const_zero, Finset.sum_boole, Nat.cast_id, zero_add]
  simp only [Finset.sum_ite,
    Finset.sum_const, smul_eq_mul, Finset.sum_const_zero, add_zero, mul_zero, add_zero]
  /-
  ⊢ {i ∈ Finset.range (5 * n) | i % 5 = 1}.card + {x ∈ Finset.range (5 * n) | x % 5 = 2}.card * 2 +
      {x ∈ Finset.range (5 * n) | x % 5 = 3}.card * 3 +
    {x ∈ Finset.range (5 * n) | x % 5 = 4}.card * 4 =
  10 * n
  -/
  sorry

[Edward van de Meent]

i've got it, but i'm not sure it's mathlib ready... (understatement, feel free to golf)

import Mathlib

lemma Finset.card_filter_mod (n m r: ℕ) (hr : r < m): {i ∈ Finset.range (m * n)| i % m = r}.card = n := by
  induction n with
  | zero => simp
  | succ n hi =>
    rw [mul_add, mul_one, Finset.range_add, Finset.filter_union, Finset.card_union_of_disjoint
      (Finset.disjoint_filter_filter (Finset.disjoint_range_addLeftEmbedding _ _)), hi]
    congr
    rw [Finset.card_eq_one]
    use m * n + r
    ext x
    simp only [Finset.mem_filter, Finset.mem_map, Finset.mem_range, addLeftEmbedding_apply,
      Finset.mem_singleton]
    constructor
    · rintro ⟨⟨a,ha,rfl⟩,rfl⟩
      simp [Nat.mod_eq_of_lt ha]
    · rintro rfl
      simp [hr, Nat.mod_eq_of_lt hr]

example (n : ℕ) : ∑ i ∈ Finset.range (5 * n), i % 5 = 10 * n := by
  have := Finset.sum_fiberwise_of_maps_to (t := Finset.range 5)
    (f := fun i : ℕ => i % 5) (g := fun i : ℕ => i % 5) (s := Finset.range (5 * n)) (by
      simp only [Finset.mem_range]
      intros
      exact Nat.mod_lt _ (by decide))
  rw [← this]
  -- simp only [Finset.sum_range_succ, Finset.range_one, Finset.sum_singleton]
  simp +contextual only [Finset.sum_filter, Finset.sum_ite, Finset.sum_const, smul_eq_mul, mul_zero, add_zero]
  trans ∑ x ∈ Finset.range 5, n * x
  · apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_range] at hx
    simp [Finset.card_filter_mod n 5 x hx]
  rw [← Finset.mul_sum,mul_comm]
  congr

[Sabbir Rahman]

Thanks all for responding, I was not aware of the "fiber" term, I have to look into that. Before that the I can't really understand the proofs :(

[Kyle Miller]

Is there anything in the statement of docs#Finset.sum_fiberwise_of_maps_to that you don't understand? You shouldn't need to know the word "fiber" for that.