Finiteness for periodic affine inversion sets

theorem Bananas.IsKAffine.iterate_nat {k : ℕ} {τ : ℤ → ℤ} (hAffine : IsKAffine k τ) (x : ℤ) (n : ℕ) : τ (x + ↑n * ↑k) = τ x + ↑n * ↑k

Iterating the defining affine-period identity by a natural number.

theorem Bananas.IsKAffine.iterate_int {k : ℕ} {τ : ℤ → ℤ} (hAffine : IsKAffine k τ) (x q : ℤ) : τ (x + q * ↑k) = τ x + q * ↑k

The affine identity extends to arbitrary integral period shifts.

theorem Bananas.int_eq_emod_add_ediv_period {k : ℕ} {b : ℤ} (_hk : 0 < k) : b = b % ↑k + ↑k * (b / ↑k)

Euclidean residue form, stated in the shape used for affine-period calculations.

theorem Bananas.abs_le_residue_sum (k : ℕ) (τ : ℤ → ℤ) (r : ℕ) (hr : r < k) : |τ ↑r| ≤ ∑ i ∈ Finset.range k, |τ ↑i|

Every residue value is bounded by the finite sum of absolute values of the values on one period.

theorem Bananas.kInversions_finite_of_isKAffine {k : ℕ} {τ : ℤ → ℤ} (hk : 0 < k) (hAffine : IsKAffine k τ) : (kInversions k τ).Finite

The inversion representatives of a positive-period affine function form a finite set. The order condition bounds the quotient of the second coordinate, while the inversion condition bounds it from above.