Sampling and rounding a convex integer path

On each block of N consecutive edges, the endpoint height difference lies between N times the first and last slopes. Common-offset floor division therefore gives a coarse edge slope between those same slopes. Consecutive coarse slopes remain nondecreasing.

def Utilities.ConvexIntegerRounding.slope (v : ℕ → ℤ) (i : ℕ) : ℤ

The forward slope on an integer path.

Equations

• Utilities.ConvexIntegerRounding.slope v i = v (i + 1) - v i

theorem Utilities.ConvexIntegerRounding.slopes_mono_of_adjacent (v : ℕ → ℤ) (L : ℕ) (hStep : ∀ (i : ℕ), i + 1 < L → slope v i ≤ slope v (i + 1)) (a b : ℕ) : a ≤ b → b < L → slope v a ≤ slope v b

Successive slope comparisons give all slope comparisons before L.

theorem Utilities.ConvexIntegerRounding.sum_slopes (v : ℕ → ℤ) (start count : ℕ) : ∑ i ∈ Finset.range count, slope v (start + i) = v (start + count) - v start

Forward slopes telescope along every finite block.

theorem Utilities.ConvexIntegerRounding.block_difference_bounds (v : ℕ → ℤ) (L : ℕ) (hMono : ∀ (a b : ℕ), a ≤ b → b < L → slope v a ≤ slope v b) (start count : ℕ) (hCount : 0 < count) (hEnd : start + count ≤ L) : ↑count * slope v start ≤ v (start + count) - v start ∧ v (start + count) - v start ≤ ↑count * slope v (start + count - 1)

A convex block's height difference lies between its length times the first slope and its length times the last slope.

theorem Utilities.ConvexIntegerRounding.rounded_block_slope_bounds (N : ℕ) (hN : 0 < N) (k : Fin N) (v : ℕ → ℤ) (L : ℕ) (hMono : ∀ (a b : ℕ), a ≤ b → b < L → slope v a ≤ slope v b) (j : ℕ) (hBlock : N * (j + 1) ≤ L) : slope v (N * j) ≤ slope (fun (i : ℕ) => CommonOffsetRounding.round N k (v (N * i))) j ∧ slope (fun (i : ℕ) => CommonOffsetRounding.round N k (v (N * i))) j ≤ slope v (N * (j + 1) - 1)

Rounding the endpoints of a convex length-N block gives a slope between the first and last source slopes.

theorem Utilities.ConvexIntegerRounding.rounded_slopes_nondecreasing (N : ℕ) (hN : 0 < N) (k : Fin N) (v : ℕ → ℤ) (L : ℕ) (hMono : ∀ (a b : ℕ), a ≤ b → b < L → slope v a ≤ slope v b) (j : ℕ) (hTwo : N * (j + 2) ≤ L) : slope (fun (i : ℕ) => CommonOffsetRounding.round N k (v (N * i))) j ≤ slope (fun (i : ℕ) => CommonOffsetRounding.round N k (v (N * i))) (j + 1)

Consecutive coarse slopes remain ordered after common-offset rounding of a convex integer path.