Rounding chips to the ends of a block of unit steps

Fix one block of N ≥ 1 unit steps carrying integer slopes s 0, …, s (N-1). Chips sit at interior offsets 1, …, N-1 of the block, indexed by a finite set chips with offsets off and a rounding side side (true = round the chip to the right end of the block, false = round it to the left end). The only hypothesis on the slopes is that they may drop across an offset, by at most the number of chips sitting there.

Moving a chip from offset off i to an end of the block changes the block total by N - off i (right end) or by -off i (left end); the sum of those changes is the correction δ. The two main results bound the corrected block total between N copies of the first slope (minus the number of chips rounded left) and N copies of the last slope (plus the number of chips rounded right), and the third bounds |δ| by the total distance the chips travel.

All of this is finite-sum integer arithmetic; no graph theory is involved.

Counting the indices of Finset.range N on one side of a threshold

Splitting a chip count off a threshold

Slope bounds inside the block

theorem Utilities.BlockSlopeRounding.slope_ge_first {ι : Type u_1} (N : ℕ) (s : ℕ → ℤ) (chips : Finset ι) (off : ι → ℕ) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) (hslope : ∀ (t : ℕ), 0 < t → t < N → s (t - 1) - ↑{i ∈ chips | off i = t}.card ≤ s t) (t : ℕ) : t < N → s 0 - ↑{i ∈ chips | off i ≤ t}.card ≤ s t

The slope at step t is at least the first slope minus the number of chips at offsets ≤ t.

theorem Utilities.BlockSlopeRounding.slope_le_last {ι : Type u_1} (N : ℕ) (s : ℕ → ℤ) (chips : Finset ι) (off : ι → ℕ) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) (hslope : ∀ (t : ℕ), 0 < t → t < N → s (t - 1) - ↑{i ∈ chips | off i = t}.card ≤ s t) (t : ℕ) : t < N → s t ≤ s (N - 1) + ↑{i ∈ chips | t < off i}.card

The slope at step t is at most the last slope plus the number of chips at offsets > t.

Double counting the chip totals

theorem Utilities.BlockSlopeRounding.sum_card_filter_le_eq {ι : Type u_1} (N : ℕ) (chips : Finset ι) (off : ι → ℕ) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) : ∑ t ∈ Finset.range N, ↑{i ∈ chips | off i ≤ t}.card = ∑ i ∈ chips, (↑N - ↑(off i))

Summing the chip counts below each threshold counts, for each chip, the number of steps strictly to its right.

theorem Utilities.BlockSlopeRounding.sum_card_filter_lt_eq {ι : Type u_1} (N : ℕ) (chips : Finset ι) (off : ι → ℕ) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) : ∑ t ∈ Finset.range N, ↑{i ∈ chips | t < off i}.card = ∑ i ∈ chips, ↑(off i)

Summing the chip counts above each threshold counts, for each chip, the number of steps to its left.

The two main bounds

theorem Utilities.BlockSlopeRounding.block_lower {ι : Type u_1} (N : ℕ) (hN : 0 < N) (s : ℕ → ℤ) (chips : Finset ι) (off : ι → ℕ) (side : ι → Bool) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) (hslope : ∀ (t : ℕ), 0 < t → t < N → s (t - 1) - ↑{i ∈ chips | off i = t}.card ≤ s t) : ↑N * (s 0 - ↑{i ∈ chips | side i = false}.card) ≤ ∑ t ∈ Finset.range N, s t + ∑ i ∈ chips, if side i = true then ↑N - ↑(off i) else -↑(off i)

Rounding every chip to an end of the block cannot push the block total below N copies of the first slope, less one for each chip rounded to the left end.

theorem Utilities.BlockSlopeRounding.block_upper {ι : Type u_1} (N : ℕ) (hN : 0 < N) (s : ℕ → ℤ) (chips : Finset ι) (off : ι → ℕ) (side : ι → Bool) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) (hslope : ∀ (t : ℕ), 0 < t → t < N → s (t - 1) - ↑{i ∈ chips | off i = t}.card ≤ s t) : (∑ t ∈ Finset.range N, s t + ∑ i ∈ chips, if side i = true then ↑N - ↑(off i) else -↑(off i)) ≤ ↑N * (s (N - 1) + ↑{i ∈ chips | side i = true}.card)

Rounding every chip to an end of the block cannot push the block total above N copies of the last slope, plus one for each chip rounded to the right end.

The size of the correction

theorem Utilities.BlockSlopeRounding.abs_delta_le {ι : Type u_1} (N : ℕ) (chips : Finset ι) (off : ι → ℕ) (side : ι → Bool) (hoff : ∀ i ∈ chips, 0 < off i ∧ off i < N) : |∑ i ∈ chips, if side i = true then ↑N - ↑(off i) else -↑(off i)| ≤ ∑ i ∈ chips, ↑(if side i = true then N - off i else off i)

The correction is bounded by the total distance the chips travel.