lean_workbook_plus_15818

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

By triangle inequality we have \n

| \sin {x} +\ cos{x} | +| \sin{x} -\cos{x}| \ge | \sin {x}+\cos{x} +\sin{x}-\cos{x}|=2|\sin{x} |\ge 2\sin ^2 {x}

equality holds if and only if $x=\dfrac {\pi} {2}$ or $x=\dfrac {3\pi} {2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15818 :
  ∀ x : ℝ,
    abs (sin x + cos x) + abs (sin x - cos x) ≥ 2 * (sin x)^2   :=  by sorry

Source