feat(Analysis/SpecialFunctions/Complex/LogBounds): Add some log bounds (#15376)

Add some basic bounds on complex logs that are useful for bounding infinite sums/products. 



Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Author: CBirkbeck

Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

@@ -178,6 +178,31 @@ lemma norm_log_one_add_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) :
   · simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]
   · norm_num
 
+lemma norm_log_one_add_le {z : ℂ} (hz : ‖z‖ < 1) :
+    ‖log (1 + z)‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖ := by
+  rw [Eq.symm (sub_add_cancel (log (1 + z)) z)]
+  apply le_trans (norm_add_le _ _)
+  exact add_le_add_right (Complex.norm_log_one_add_sub_self_le hz) ‖z‖
+
+/--For `‖z‖ ≤ 1/2`, the complex logarithm is bounded by `(3/2) * ‖z‖`. -/
+lemma norm_log_one_add_half_le_self {z : ℂ} (hz : ‖z‖ ≤ 1/2) : ‖(log (1 + z))‖ ≤ (3/2) * ‖z‖ := by
+  apply le_trans (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one))
+  have hz3 : (1 - ‖z‖)⁻¹ ≤ 2 := by
+    rw [inv_eq_one_div, div_le_iff]
+    · linarith
+    · linarith
+  have hz4 : ‖z‖^2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖/2 * 2 / 2 := by
+    gcongr
+    · rw [inv_nonneg]
+      linarith
+    · rw [sq, div_eq_mul_one_div]
+      apply mul_le_mul (by simp only [norm_eq_abs, mul_one, le_refl])
+        (by simpa only [norm_eq_abs, one_div] using hz) (norm_nonneg z)
+        (by simp only [norm_eq_abs, mul_one, apply_nonneg])
+  simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+    IsUnit.div_mul_cancel] at hz4
+  linarith
+
 /-- The difference of `log (1-z)⁻¹` and its `(n+1)`st Taylor polynomial can be bounded in
 terms of `‖z‖`. -/
 lemma norm_log_one_sub_inv_add_logTaylor_neg_le (n : ℕ) {z : ℂ} (hz : ‖z‖ < 1) :