Elementary logarithm comparisons

Main results

• Real.log_add_one_le_self: Real.log (x + 1) ≤ x for 0 ≤ x.
• Real.natCast_le_of_log_le_log: a positive natural number is bounded by a positive real once their logarithms compare.
• Real.log_one_add_sub_div_four_le: Real.log (1 + x) - x / 4 ≤ Real.log 4 + 1 for 0 ≤ x.
• Real.rpow_half_mul_log_add_le: √B (log B + D) ≤ (1/ε + D) B^(1/2 + ε) for B ≥ 1, an explicit absorption of the logarithm into a power.

theorem Real.log_add_one_le_self {x : ℝ} (hx : 0 ≤ x) : log (x + 1) ≤ x

For nonnegative x, Real.log (x + 1) ≤ x.

theorem Real.natCast_le_of_log_le_log {n : ℕ} {y : ℝ} (hn : 0 < n) (hy : 0 < y) (h : log ↑n ≤ log y) : ↑n ≤ y

A positive natural number is bounded by a positive real once their logarithms compare.

theorem Real.log_one_add_sub_div_four_le {x : ℝ} (hx : 0 ≤ x) : log (1 + x) - x / 4 ≤ log 4 + 1

The logarithm log (1 + x) exceeds x / 4 by at most log 4 + 1 for x ≥ 0.

theorem Real.rpow_half_mul_log_add_le {B ε D : ℝ} (hB : 1 ≤ B) (hε : 0 < ε) (hD : 0 ≤ D) : B ^ (1 / 2) * (log B + D) ≤ (1 / ε + D) * B ^ (1 / 2 + ε)

Absorb the logarithm with a specified positive exponent loss and an explicit constant.