Prove2Me

Lean-Workbook Plus 8810: Trigonometric inequality

Proved
WorkbookRestored.plus_8810

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

Prove that xcos⁡x≤x+cos⁡x2\sqrt{x\cos x} \le \frac{x + \cos x}{2} for x∈[0,π2]x\in [0,\frac{\pi}{2}] using the Arithmetic Mean-Geometric Mean (AM-GM) inequality.

Source: Lean-Workbook row lean_workbook_plus_8810 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real
Formal statement
theorem WorkbookRestored.plus_8810 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ π/2) :
  Real.sqrt (x * Real.cos x) ≤ (x + Real.cos x) / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_8810; immutable original Prove2Me node 4cb6ee1f-83cc-4be2-b63b-16815b307fda

View graph