feat(analysis/special_functions/log): log of natural power (#11685)

The rpow versions are already present, but the natural/integer versions can also be very helpful (eg for squares).

src/analysis/special_functions/log.lean

@@ -172,6 +172,23 @@ begin
   { rintro (rfl|rfl|rfl); simp only [log_one, log_zero, log_neg_eq_log], }
 end
 
+@[simp] lemma log_pow (x : ℝ) (n : ℕ) : log (x ^ n) = n * log x :=
+begin
+  induction n with n ih,
+  { simp },
+  rcases eq_or_ne x 0 with rfl | hx,
+  { simp },
+  rw [pow_succ', log_mul (pow_ne_zero _ hx) hx, ih, nat.cast_succ, add_mul, one_mul],
+end
+
+@[simp] lemma log_zpow (x : ℝ) (n : ℤ) : log (x ^ n) = n * log x :=
+begin
+  induction n,
+  { rw [int.of_nat_eq_coe, zpow_coe_nat, log_pow, int.cast_coe_nat] },
+  rw [zpow_neg_succ_of_nat, log_inv, log_pow, int.cast_neg_succ_of_nat, nat.cast_add_one,
+    neg_mul_eq_neg_mul],
+end
+
 lemma log_le_sub_one_of_pos {x : ℝ} (hx : 0 < x) : log x ≤ x - 1 :=
 begin
   rw le_sub_iff_add_le,