Prove2Me

Lean-Workbook Plus 15818: Trigonometric inequality

Proved
WorkbookRestored.plus_15818

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

lean-workbookrestored-importssource-checked

For every real xx, ∣sin⁡x+cos⁡x∣+∣sin⁡x−cos⁡x∣≥2sin⁡2x|\sin x+\cos x|+|\sin x-\cos x|\ge2\sin^2 x. This formalizes the inequality in the source; it makes no assertion about equality cases.

Source: Lean-Workbook row lean_workbook_plus_15818 (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_15818 :
  ∀ x : ℝ,
    abs (sin x + cos x) + abs (sin x - cos x) ≥ 2 * (sin x)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_15818; immutable original Prove2Me node 5c569a1b-c3ed-4672-8f6c-f5712ea987c0

View graph