feat(analysis/special_functions/log): Relating log-inequalities and…

… `exp`-inequalities (#10191)

This proves `log x ≤ y ↔ x ≤ exp y` and `x ≤ log y ↔ exp x ≤ y`.

src/analysis/special_functions/log.lean

@@ -101,6 +101,14 @@ by { intro h, rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)] }
 lemma log_lt_log_iff (hx : 0 < x) (hy : 0 < y) : log x < log y ↔ x < y :=
 by { rw [← exp_lt_exp, exp_log hx, exp_log hy] }
 
+lemma log_le_iff_le_exp (hx : 0 < x) : log x ≤ y ↔ x ≤ exp y := by rw [←exp_le_exp, exp_log hx]
+
+lemma log_lt_iff_lt_exp (hx : 0 < x) : log x < y ↔ x < exp y := by rw [←exp_lt_exp, exp_log hx]
+
+lemma le_log_iff_exp_le (hy : 0 < y) : x ≤ log y ↔ exp x ≤ y := by rw [←exp_le_exp, exp_log hy]
+
+lemma lt_log_iff_exp_lt (hy : 0 < y) : x < log y ↔ exp x < y := by rw [←exp_lt_exp, exp_log hy]
+
 lemma log_pos_iff (hx : 0 < x) : 0 < log x ↔ 1 < x :=
 by { rw ← log_one, exact log_lt_log_iff zero_lt_one hx }
 
@@ -228,4 +236,3 @@ lemma continuous_on.log (hf : continuous_on f s) (h₀ : ∀ x ∈ s, f x ≠ 0)
 λ x hx, (hf x hx).log (h₀ x hx)
 
 end continuity
-