Explicit smallness for the finite geometric sums in the transported H_m estimate.

theorem AVenhance.Infra.Section4.hm_pow_sum_range_le_two {x : ℝ} (hx0 : 0 ≤ x) (hxhalf : x ≤ 1 / 2) (N : ℕ) : ∑ n ∈ Finset.range N, x ^ n ≤ 2

A finite geometric sum with ratio at most one half is at most two.