Elementary bounds on -log (1 - x)

This file bounds the quadratic remainder -log (1 - x) - x, then specializes the estimate to x = y ^ (-s). The sharp factor 2 in the denominator comes from reading Mathlib's complex logarithm bound along the reals. It also records the coarser estimate -log (1 - x) ≤ x + 2 x ^ 2 for 0 ≤ x ≤ 1/2.

Main results

• Real.neg_log_one_sub_sub_le: for 0 ≤ x < 1, the remainder is at most x² / (2 (1 - x)).
• Real.neg_log_one_sub_rpow_sub_le_div: for 2 ≤ y and 0 < s, it is at most y ^ (-2s) / (2 (1 - 2 ^ (-s))).
• Real.neg_log_one_sub_rpow_sub_le: for 2 ≤ y and 1 ≤ s, it is at most y⁻².
• Real.neg_log_one_sub_le_add_two_mul_sq: for 0 ≤ x ≤ 1/2, -log (1 - x) is at most x + 2 x ^ 2.
• Complex.norm_neg_log_one_sub_sub_le: for complex z with ‖z‖ ≤ 1/2, the remainder -log (1 - z) - z has norm at most ‖z‖ ^ 2.

References

The shape of Real.neg_log_one_sub_sub_le follows the private declaration neg_log_one_sub_sub_le in CebotarevDensity/Density.lean of CBirkbeck/chebotarev-density (Apache-2.0, C. Birkbeck and R. Brasca), commit 8575c9df1ae0a61120ab5c964c7911414254bec7. The sharper constant here comes from Mathlib's Complex.norm_log_one_sub_inv_sub_self_le.

theorem Real.neg_log_one_sub_sub_nonneg {x : ℝ} (hx1 : x < 1) : 0 ≤ -log (1 - x) - x

The quadratic remainder of -log (1 - x) is nonnegative for x < 1.

theorem Real.neg_log_one_sub_sub_le {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) : -log (1 - x) - x ≤ x ^ 2 / (2 * (1 - x))

The quadratic remainder of -log (1 - x) is at most x² / (2 (1 - x)) for 0 ≤ x < 1. This is Mathlib's complex logarithm bound read along the reals.

theorem Real.neg_log_one_sub_rpow_sub_nonneg {y s : ℝ} (hy : 1 < y) (hs : 0 < s) : 0 ≤ -log (1 - y ^ (-s)) - y ^ (-s)

For 1 < y and 0 < s, the quadratic remainder of -log (1 - y ^ (-s)) is nonnegative.

theorem Real.neg_log_one_sub_rpow_sub_le_div {y s : ℝ} (hy : 2 ≤ y) (hs : 0 < s) : -log (1 - y ^ (-s)) - y ^ (-s) ≤ y ^ (-(2 * s)) / (2 * (1 - 2 ^ (-s)))

For 2 ≤ y and 0 < s, the quadratic remainder of -log (1 - y ^ (-s)) is bounded by y ^ (-2s) / (2 (1 - 2 ^ (-s))).

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

For 2 ≤ y and 1 ≤ s, the quadratic remainder of -log (1 - y ^ (-s)) is at most y⁻².

theorem Real.neg_log_one_sub_le_add_two_mul_sq {x : ℝ} (hx0 : 0 ≤ x) (hx : x ≤ 1 / 2) : -log (1 - x) ≤ x + 2 * x ^ 2

For 0 ≤ x ≤ 1/2, -log (1 - x) ≤ x + 2 x ^ 2.

theorem Complex.norm_neg_log_one_sub_sub_le {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖-log (1 - z) - z‖ ≤ ‖z‖ ^ 2

For complex z with ‖z‖ ≤ 1 / 2, the quadratic remainder -log (1 - z) - z has norm at most ‖z‖ ^ 2.