Complex.CartanBound.phi_le_log_two_of_le_half

lemma phi_le_log_two_of_le_half {t : ℝ} (ht : t ≤ (1 / 2 : ℝ)) : φ t ≤ Real.log 2 := by  have hnonneg : 0 ≤ (1 - t : ℝ) := by linarith  have hden : (1 / 2 : ℝ) ≤ |1 - t| := by    have : (1 / 2 : ℝ) ≤ (1 - t : ℝ) := by linarith    simpa [abs_of_nonneg hnonneg] using this  have hfrac : (1 / |1 - t| : ℝ) ≤ 2 := by    have hhalfpos : (0 : ℝ) < (1 / 2 : ℝ) := by norm_num    have := one_div_le_one_div_of_le hhalfpos hden    simpa [one_div, div_eq_mul_inv] using this  have hposLog : log⁺ (1 / |1 - t|) ≤ log⁺ (2 : ℝ) :=    Real.posLog_le_posLog (by positivity) hfrac  have habs : (1 : ℝ) ≤ |(2 : ℝ)| := by    simp  have hposLog2 : (log⁺ (2 : ℝ)) = Real.log 2 := by    simpa using (Real.posLog_eq_log habs)  simpa [φ, hposLog2] using hposLog