Elementary bounds on real powers with a negative exponent

A base at least 2 raised to a negative exponent of size at least 1 is at most 1 / 2. This is the shape in which the local ratio of an Euler factor is bounded away from 1, so that the denominator 1 - y ^ (-s) stays bounded below.

Main results

• Real.rpow_neg_le_half: y ^ (-s) ≤ 1 / 2 for 2 ≤ y and 1 ≤ s.

theorem Real.rpow_neg_le_half {y s : ℝ} (hy : 2 ≤ y) (hs : 1 ≤ s) : y ^ (-s) ≤ 1 / 2

If 2 ≤ y and 1 ≤ s, then y ^ (-s) ≤ 1 / 2.