Complex.Gamma.log_one_add_norm_add_one_le

lemma log_one_add_norm_add_one_le {s : ℂ} (hs : 1 ≤ ‖s‖) :    Real.log (1 + ‖s + 1‖) ≤ Real.log 2 + Real.log (1 + ‖s‖) := by  have hpos : 0 < (1 + ‖s + 1‖ : ℝ) := by linarith [norm_nonneg (s + 1)]  have hle : (1 + ‖s + 1‖ : ℝ) ≤ 2 * (1 + ‖s‖) := by    have hn : ‖s + 1‖ ≤ ‖s‖ + 1 := by simpa using norm_add_le s (1 : ℂ)    nlinarith [hn, hs]  have hlog' : Real.log (1 + ‖s + 1‖) ≤ Real.log (2 * (1 + ‖s‖)) :=    Real.log_le_log hpos (by linarith)  have hmul : Real.log (2 * (1 + ‖s‖)) = Real.log 2 + Real.log (1 + ‖s‖) := by    have h2 : (2 : ℝ) ≠ 0 := by norm_num    have h1 : (1 + ‖s‖ : ℝ) ≠ 0 := by linarith [norm_nonneg s]    simpa [mul_assoc] using Real.log_mul h2 h1  simpa [hmul] using hlog'