Strict bounds for finite geometric tails

Main results

• geom_sum_Ico_lt_of_lt_one: the strict bound for ∑ i ∈ Ico m n, x ^ i when 0 < x < 1.

References

Adapted selectively from Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

theorem geom_sum_Ico_lt_of_lt_one {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {x : K} (hx : 0 < x) (hx1 : x < 1) (m n : ℕ) : ∑ i ∈ Finset.Ico m n, x ^ i < x ^ m / (1 - x)

For 0 < x < 1, ∑ i ∈ Ico m n, x ^ i < x ^ m / (1 - x). Mathlib's geom_sum_Ico_le_of_lt_one has ≤, for 0 ≤ x.