lean_workbook_plus_76550
Provedprove that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76550 (a : ℝ) (ha : a > 0) : Real.sqrt (a^2 + 1/a) ≥ (a + 3) / (2 * Real.sqrt 2) := by sorry
Source
prove that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_76550 (a : ℝ) (ha : a > 0) : Real.sqrt (a^2 + 1/a) ≥ (a + 3) / (2 * Real.sqrt 2) := by sorry