(1 - 1 / k) ^ k ≤ 1 / 2 in ℝ≥0∞

Repeating a trial that succeeds with probability at least 1 / k for k times fails with probability at most (1 - 1 / k) ^ k, which is at most e⁻¹, hence at most 1 / 2. This file proves the bound (1 - 1 / k) ^ k ≤ 1 / 2 in ℝ≥0∞ without real analysis: after clearing denominators it is 2 (k - 1) ^ k ≤ k ^ k (Nat.two_mul_pred_pow_le), an instance of Bernoulli's inequality.

Main results

• ENNReal.one_sub_inv_pow_le_inv_two: (1 - k⁻¹) ^ k ≤ 2⁻¹ for every positive natural k.

theorem ENNReal.one_sub_inv_pow_le_inv_two {k : ℕ} (hk : k ≠ 0) : (1 - (↑k)⁻¹) ^ k ≤ 2⁻¹

(1 - 1 / k) ^ k ≤ 1 / 2 in ℝ≥0∞ for every positive natural number k.