Bounds on a scaled logarithm as bounds by an exponential

For x > 0 and c > 0, an upper bound R on log x / c or on -log x / c is the same as a bound on x by exp (c * R) or exp (-(c * R)). Logarithmic coordinates -log x / (2π), such as the longitudinal coordinates of the cylindrical ends of the thrice-punctured sphere, turn bounds on the coordinate into bounds on a norm in this way.

Main results

• Real.log_div_le_iff: log x / c ≤ R ↔ x ≤ exp (c * R).
• Real.neg_log_div_le_iff: -log x / c ≤ R ↔ exp (-(c * R)) ≤ x.

theorem Real.log_div_le_iff {x c R : ℝ} (hx : 0 < x) (hc : 0 < c) : log x / c ≤ R ↔ x ≤ exp (c * R)

For x > 0 and c > 0, the bound log x / c ≤ R says x ≤ exp (c * R).

theorem Real.neg_log_div_le_iff {x c R : ℝ} (hx : 0 < x) (hc : 0 < c) : -log x / c ≤ R ↔ exp (-(c * R)) ≤ x

For x > 0 and c > 0, the bound -log x / c ≤ R says exp (-(c * R)) ≤ x.