lean_workbook_plus_62954
DisprovedWhich is AM-GM:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62954 : ∀ x y z t : ℝ, (x + (y + z + t)) / 2 ≥ Real.sqrt (x * (y + z + t)) := by sorry
Source
Which is AM-GM:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_62954 : ∀ x y z t : ℝ, (x + (y + z + t)) / 2 ≥ Real.sqrt (x * (y + z + t)) := by sorry