lean_workbook_plus_39123
ProvedProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39123 {a b : ℝ} (ha : a > 0) (hb : b > 0) : (1 / a + 1 / b) / 2 ≥ 2 / (a + b) := by sorrySource
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_39123 {a b : ℝ} (ha : a > 0) (hb : b > 0) : (1 / a + 1 / b) / 2 ≥ 2 / (a + b) := by sorry