Nonnegativity of the logarithm of a lower-truncated number

The logarithm of max 1 x is nonnegative for every real x. It absorbs constant terms in estimates of the form C * (1 + log (max 1 |b|)).

Main results

• Real.log_max_one_nonneg: 0 ≤ log (max 1 x).

@[simp]

theorem Real.log_max_one_nonneg (x : ℝ) : 0 ≤ log (max 1 x)

The logarithm of max 1 x is nonnegative for every real x.