Sums over ranges, consecutive blocks and residue classes

Small facts about list sums and lists of natural numbers.

• Sums over ranges. A list sum over List.range n is the Finset sum over range n (List.sum_map_range_eq_sum_range); a list is its entries at 0, …, length - 1 (List.map_getD_range); sums over a flatMap and of a filter's length (List.sum_map_flatMap, List.length_filter_eq_sum), and a Finset sum of list sums is a list sum of Finset sums (Finset.sum_list_sum_comm).
• Consecutive blocks. Numbering blocks of sizes w 0, w 1, … consecutively, block b is List.blockRange w b, starting at List.blockStart w b; the blocks below B are the numbers below List.blockStart w B (List.flatMap_blockRange). The pairs g J + h for g < G, h < J are the numbers below G J (List.flatMap_range_mul).
• Residue classes. List.residueClass J m g is the numbers i below m with i % J = g. Summing over the residue classes modulo J > 0 sums over the list (List.sum_filter_mod), and a residue class below m has at most m / J + 1 numbers (List.length_residueClass_le).

Main definitions

• List.blockStart, List.blockRange: consecutive blocks.
• List.residueClass: a residue class below m.

Main results

• List.sum_map_range_eq_sum_range, List.map_getD_range, List.sum_map_flatMap, List.length_filter_eq_sum, Finset.sum_list_sum_comm: sums.
• List.flatMap_blockRange, List.flatMap_range_mul: consecutive blocks.
• List.sum_filter_mod, List.sum_residueClass, List.sum_length_filter_mod, List.length_residueClass_le: residue classes.

Sums over ranges

theorem List.sum_map_range_eq_sum_range {M : Type u_1} [AddCommMonoid M] (n : ℕ) (f : ℕ → M) : (map f (range n)).sum = ∑ i ∈ Finset.range n, f i

A list sum over List.range n is the Finset sum over range n.

theorem List.map_getD_range {α : Type u_1} (l : List α) (x : α) : map (fun (x_1 : ℕ) => l.getD x_1 x) (range l.length) = l

A list is its entries at 0, …, length - 1.

theorem List.sum_map_flatMap {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddMonoid M] (l : List α) (f : α → List β) (g : β → M) : (map g (flatMap f l)).sum = (map (fun (x : α) => (map g (f x)).sum) l).sum

A sum over a flatMap sums the inner sums.

theorem List.length_filter_eq_sum {α : Type u_1} (l : List α) (q : α → Bool) : (filter q l).length = (map (fun (x : α) => if q x = true then 1 else 0) l).sum

The length of a filtered list counts its elements satisfying the predicate.

theorem Finset.sum_list_sum_comm {ι : Type u_1} {α : Type u_2} (s : Finset ι) (l : List α) (f : ι → α → ℕ) : ∑ h ∈ s, (List.map (f h) l).sum = (List.map (fun (x : α) => ∑ h ∈ s, f h x) l).sum

A Finset sum of list sums is the list sum of the Finset sums.

Consecutive blocks

def List.blockStart (w : ℕ → ℕ) (b : ℕ) : ℕ

The first number of block b when block b' has w b' numbers: Σ_{b' < b} w b'.

def List.blockRange (w : ℕ → ℕ) (b : ℕ) : List ℕ

The numbers of block b: blockStart w b, …, blockStart w b + w b - 1.

theorem List.blockStart_succ (w : ℕ → ℕ) (b : ℕ) : blockStart w (b + 1) = blockStart w b + w b

theorem List.flatMap_blockRange (w : ℕ → ℕ) (B : ℕ) : flatMap (blockRange w) (range B) = range (blockStart w B)

Consecutive blocks: the numbers of the blocks below B, in order, are the numbers below blockStart w B.

theorem List.flatMap_range_mul (G J : ℕ) : flatMap (fun (g : ℕ) => map (fun (x : ℕ) => g * J + x) (range J)) (range G) = range (G * J)

The pairs g J + h for g < G and h < J, in order, are the numbers below G J.

Residue classes

def List.residueClass (J m g : ℕ) : List ℕ

The residue class of g modulo J below m: the numbers i below m with i % J = g, in increasing order. It is empty when 0 < J ≤ g.

theorem List.sum_filter_mod {J : ℕ} (hJ : 0 < J) (l : List ℕ) (f : ℕ → ℕ) : ∑ h ∈ Finset.range J, (map f (filter (fun (x : ℕ) => decide (x % J = h)) l)).sum = (map f l).sum

Summing over the residue classes modulo J > 0 sums over the list.

theorem List.sum_residueClass {J : ℕ} (hJ : 0 < J) (m : ℕ) (f : ℕ → ℕ) : ∑ g ∈ Finset.range J, (map f (residueClass J m g)).sum = (map f (range m)).sum

Summing over the residue classes below m sums over the numbers below m.

theorem List.sum_length_filter_mod {J : ℕ} (hJ : 0 < J) (l : List ℕ) : ∑ h ∈ Finset.range J, (filter (fun (x : ℕ) => decide (x % J = h)) l).length = l.length

Summing the sizes of the residue classes modulo J > 0 gives the length.

theorem List.length_residueClass_le (J m g : ℕ) : (residueClass J m g).length ≤ m / J + 1

A residue class below m has at most m / J + 1 numbers.