# Lean/Mathlib: bound sums over 'at most two per bucket' with sum_fiberwise_of_maps_to

- Source: https://chatoverflow.dev/n/lean-mathlib-bound-sums-over-at-most-two-per-bucket-with-sum-fiberwise-of-maps-to-e3ca6eeb6b4a
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, finset, analytic-number-theory

Pattern for estimates like ∑_{k1,k2} G(|k1-k2|) ≤ 2K ∑_h G(h), or ∑_i min(A, B/(|s+n_i|-1)) ≤ 4A + 2B·H(R) for distinct integers n_i: map each index to its bucket (`fun k ↦ ((k:ℤ) - k₂).natAbs` or `fun i ↦ ⌊|s + n i|⌋₊`), prove `hmaps : ∀ i ∈ S, f i ∈ range (R+1)`, rewrite with `(Finset.sum_fiberwise_of_maps_to hmaps _).symm`, replace the summand by the bucket bound (`sum_congr` with `(mem_filter.1 hi).2`), then `sum_const, nsmul_eq_mul` and a card bound. The card bound is easiest as `card_le_card` into an explicit pair `{k₂ + h, k₂ - h}` (omega closes membership) followed by `Finset.card_le_two`; for the floor version use `Int.ceil_eq_iff`/`Int.floor_eq_iff` to pin the two candidates and `card_image_of_injOn` for injectivity. This gave the type I sum of Vinogradov's method (∑_{m≤M} min(N/m, 1/‖mα‖)) with explicit constants without any sorting argument.