feat(analysis/special_functions/*): a few more simp lemmas (#4550)

Add more lemmas for simplifying inequalities with `exp`, `log`, and
`rpow`. Lemmas that generate more than one inequality are not marked
as `simp`.

src/algebra/ordered_ring.lean

@@ -198,7 +198,7 @@ le_of_not_gt
    h2.not_le h)
 
 lemma pos_and_pos_or_neg_and_neg_of_mul_pos (hab : 0 < a * b) :
-    (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) :=
+  (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) :=
 begin
   rcases lt_trichotomy 0 a with (ha|rfl|ha),
   { refine or.inl ⟨ha, _⟩,

src/analysis/special_functions/exp_log.lean

@@ -272,16 +272,25 @@ by { rw ← log_one, exact log_lt_log_iff h (by norm_num) }
 
 lemma log_neg (h0 : 0 < x) (h1 : x < 1) : log x < 0 := (log_neg_iff h0).2 h1
 
-lemma log_nonneg : 1 ≤ x → 0 ≤ log x :=
-by { intro, rwa [← log_one, log_le_log], norm_num, linarith }
+lemma log_nonneg_iff (hx : 0 < x) : 0 ≤ log x ↔ 1 ≤ x :=
+by rw [← not_lt, log_neg_iff hx, not_lt]
 
-lemma log_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : log x ≤ 0 :=
+lemma log_nonneg (hx : 1 ≤ x) : 0 ≤ log x :=
+(log_nonneg_iff (zero_lt_one.trans_le hx)).2 hx
+
+lemma log_nonpos_iff (hx : 0 < x) : log x ≤ 0 ↔ x ≤ 1 :=
+by rw [← not_lt, log_pos_iff hx, not_lt]
+
+lemma log_nonpos_iff' (hx : 0 ≤ x) : log x ≤ 0 ↔ x ≤ 1 :=
 begin
-  by_cases x_zero : x = 0,
-  { simp [x_zero] },
-  { rwa [← log_one, log_le_log (lt_of_le_of_ne hx (ne.symm x_zero))], norm_num }
+  rcases hx.eq_or_lt with (rfl|hx),
+  { simp [le_refl, zero_le_one] },
+  exact log_nonpos_iff hx
 end
 
+lemma log_nonpos (hx : 0 ≤ x) (h'x : x ≤ 1) : log x ≤ 0 :=
+(log_nonpos_iff' hx).2 h'x
+
 section prove_log_is_continuous
 
 lemma tendsto_log_one_zero : tendsto log (𝓝 1) (𝓝 0) :=

src/analysis/special_functions/pow.lean

@@ -385,14 +385,37 @@ by { rw ← one_rpow z, exact rpow_lt_rpow zero_le_one hx hz }
 lemma one_le_rpow {x z : ℝ} (hx : 1 ≤ x) (hz : 0 ≤ z) : 1 ≤ x^z :=
 by { rw ← one_rpow z, exact rpow_le_rpow zero_le_one hx hz }
 
-lemma one_lt_rpow_of_pos_of_lt_one_of_neg {x z : ℝ} (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
+lemma one_lt_rpow_of_pos_of_lt_one_of_neg (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
   1 < x^z :=
 by { convert rpow_lt_rpow_of_exponent_gt hx1 hx2 hz, exact (rpow_zero x).symm }
 
-lemma one_le_rpow_of_pos_of_le_one_of_nonpos {x z : ℝ} (hx1 : 0 < x) (hx2 : x ≤ 1) (hz : z ≤ 0) :
+lemma one_le_rpow_of_pos_of_le_one_of_nonpos (hx1 : 0 < x) (hx2 : x ≤ 1) (hz : z ≤ 0) :
   1 ≤ x^z :=
 by { convert rpow_le_rpow_of_exponent_ge hx1 hx2 hz, exact (rpow_zero x).symm }
 
+lemma rpow_lt_one_iff_of_pos (hx : 0 < x) : x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y :=
+by rw [rpow_def_of_pos hx, exp_lt_one_iff, mul_neg_iff, log_pos_iff hx, log_neg_iff hx]
+
+lemma rpow_lt_one_iff (hx : 0 ≤ x) : x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y :=
+begin
+  rcases hx.eq_or_lt with (rfl|hx),
+  { rcases em (y = 0) with (rfl|hy); simp [*, lt_irrefl, zero_lt_one] },
+  { simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm] }
+end
+
+lemma one_lt_rpow_iff_of_pos (hx : 0 < x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0 :=
+by rw [rpow_def_of_pos hx, one_lt_exp_iff, mul_pos_iff, log_pos_iff hx, log_neg_iff hx]
+
+lemma one_lt_rpow_iff (hx : 0 ≤ x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0 :=
+begin
+  rcases hx.eq_or_lt with (rfl|hx),
+  { rcases em (y = 0) with (rfl|hy); simp [*, lt_irrefl, (@zero_lt_one ℝ _).not_lt] },
+  { simp [one_lt_rpow_iff_of_pos hx, hx] }
+end
+
+lemma rpow_le_one_iff_of_pos (hx : 0 < x) : x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y :=
+by rw [rpow_def_of_pos hx, exp_le_one_iff, mul_nonpos_iff, log_nonneg_iff hx, log_nonpos_iff hx]
+
 lemma pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : 0 < n) :
   (x ^ n) ^ (n⁻¹ : ℝ) = x :=
 have hn0 : (n : ℝ) ≠ 0, by simpa [nat.pos_iff_ne_zero] using hn,

src/data/complex/exponential.lean

@@ -958,12 +958,18 @@ lemma exp_injective : function.injective exp := exp_strict_mono.injective
 @[simp] lemma exp_eq_one_iff : exp x = 1 ↔ x = 0 :=
 by rw [← exp_zero, exp_injective.eq_iff]
 
-lemma one_lt_exp_iff {x : ℝ} : 1 < exp x ↔ 0 < x :=
+@[simp] lemma one_lt_exp_iff {x : ℝ} : 1 < exp x ↔ 0 < x :=
 by rw [← exp_zero, exp_lt_exp]
 
-lemma exp_lt_one_iff {x : ℝ} : exp x < 1 ↔ x < 0 :=
+@[simp] lemma exp_lt_one_iff {x : ℝ} : exp x < 1 ↔ x < 0 :=
 by rw [← exp_zero, exp_lt_exp]
 
+@[simp] lemma exp_le_one_iff {x : ℝ} : exp x ≤ 1 ↔ x ≤ 0 :=
+exp_zero ▸ exp_le_exp
+
+@[simp] lemma one_le_exp_iff {x : ℝ} : 1 ≤ exp x ↔ 0 ≤ x :=
+exp_zero ▸ exp_le_exp
+
 /-- `real.cosh` is always positive -/
 lemma cosh_pos (x : ℝ) : 0 < real.cosh x :=
 (cosh_eq x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x)))