Complex.CartanBound.posLog_one_div_norm_one_sub_le_posLog_one_div_abs_one_sub_norm

lemma posLog_one_div_norm_one_sub_le_posLog_one_div_abs_one_sub_norm (w : ℂ) (hw : ‖w‖ ≠ (1 : ℝ)) :    Real.posLog (1 / ‖(1 : ℂ) - w‖) ≤ Real.posLog (1 / |1 - ‖w‖|) := by  have hrev : |(‖(1 : ℂ)‖ : ℝ) - ‖w‖| ≤ ‖(1 : ℂ) - w‖ :=    abs_norm_sub_norm_le (1 : ℂ) w  have hrev' : |1 - ‖w‖| ≤ ‖(1 : ℂ) - w‖ := by    simpa using hrev  have h0 : |1 - ‖w‖| ≠ 0 := by    have : (1 : ℝ) - ‖w‖ ≠ 0 := by      intro h      have : ‖w‖ = (1 : ℝ) := by linarith      exact hw this    simpa [abs_eq_zero] using this  have hpos : 0 < |1 - ‖w‖| := lt_of_le_of_ne (abs_nonneg _) (Ne.symm h0)  have hdiv :      (1 / ‖(1 : ℂ) - w‖ : ℝ) ≤ (1 / |1 - ‖w‖| : ℝ) :=    one_div_le_one_div_of_le hpos hrev'  exact Real.posLog_le_posLog (by positivity) hdiv