Results about big operators with values in floor rings

This file proves the classical Hermite identity for the floor function: for every element x of a linearly ordered floor field and every natural number n, $$ \sum_{i=0}^{n-1} \left\lfloor x + \frac{i}{n} \right\rfloor = \lfloor n x \rfloor. $$

Main statements

• Int.sum_floor_add_div: Hermite's identity, ∑ i ∈ Finset.range n, ⌊x + i / n⌋ = ⌊n * x⌋.

theorem Int.sum_range_add_ediv (m : ℤ) {n : ℕ} (hn : 0 < n) : ∑ i ∈ Finset.range n, (m + ↑i) / ↑n = m

The discrete (integer) form of Hermite's identity: the sum of (m + i) / n over a complete block 0 ≤ i < n of consecutive shifts equals m, where / is Euclidean (Int.ediv) division.

theorem Int.sum_floor_add_div {α : Type u_1} [Field α] [LinearOrder α] [IsOrderedRing α] [FloorRing α] (x : α) (n : ℕ) : ∑ i ∈ Finset.range n, ⌊x + ↑i / ↑n⌋ = ⌊↑n * x⌋

Hermite's identity for the floor function: for every x in a linearly ordered floor field and every n : ℕ, ∑ i ∈ Finset.range n, ⌊x + i / n⌋ = ⌊n * x⌋.