lean_workbook_plus_19881
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19881 : ∀ a b : ℝ, a ≥ 0 ∧ b ≥ 0 → Real.sqrt ((a + b) / 2) ≥ (Real.sqrt a + Real.sqrt b) / 2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19881 : ∀ a b : ℝ, a ≥ 0 ∧ b ≥ 0 → Real.sqrt ((a + b) / 2) ≥ (Real.sqrt a + Real.sqrt b) / 2 := by sorry