Complex.CartanBound.posLog_log_one_div_abs_one_sub_le_sqrt

lemma posLog_log_one_div_abs_one_sub_le_sqrt {t : ℝ} :    Real.posLog (1 / |1 - t|) ≤ Real.sqrt (2 / |1 - t|) := by  by_cases ht : |1 - t| ≤ 1  · by_cases h0 : |1 - t| = 0    · have : t = 1 := by        have : 1 - t = 0 := by simpa [abs_eq_zero] using h0        linarith      subst this      simp    · have hpos : 0 < |1 - t| := lt_of_le_of_ne (abs_nonneg _) (Ne.symm h0)      have hle : -Real.log |1 - t| ≤ Real.sqrt (2 / |1 - t|) :=        neg_log_le_sqrt_two_div (x := |1 - t|) hpos ht      have hlog : Real.log (1 / |1 - t|) = -Real.log |1 - t| := by simp [Real.log_inv]      have hnonneg : 0 ≤ Real.log (1 / |1 - t|) := by        exact Real.log_nonneg ((one_le_div hpos).2 ht)      have hmax : Real.posLog (1 / |1 - t|) = Real.log (1 / |1 - t|) :=        max_eq_right hnonneg      calc        Real.posLog (1 / |1 - t|) = Real.log (1 / |1 - t|) := hmax        _ = -Real.log |1 - t| := hlog        _ ≤ Real.sqrt (2 / |1 - t|) := hle  · have hlt : 1 < |1 - t| := lt_of_not_ge ht    have hle0 : Real.log (1 / |1 - t|) ≤ 0 := by      have hpos : 0 < |1 - t| := lt_trans (by norm_num) hlt      have : (1 / |1 - t| : ℝ) ≤ 1 := (div_le_one hpos).2 (le_of_lt hlt)      exact le_trans (Real.log_le_log (by positivity) this) (by simp)    have hmax : Real.posLog (1 / |1 - t|) = 0 := max_eq_left hle0    have hrhs : 0 ≤ Real.sqrt (2 / |1 - t|) := by      exact Real.sqrt_nonneg _    rw [hmax]    exact hrhs