Prove2Me

Lean-Workbook Plus 16703: Trigonometric inequality

Proved
WorkbookRestored.plus_16703

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

lean-workbookrestored-importssource-checked

For real a,b,c,y,za,b,c,y,z, (asin⁡y+bcos⁡z+c)2≤(a2+b2+c2)(sin⁡2y+cos⁡2z+12)(a\sin y+b\cos z+c)^2\le(a^2+b^2+c^2)(\sin^2y+\cos^2z+1^2).

Source: Lean-Workbook row lean_workbook_plus_16703 (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_16703 {a b c : ℝ} {y z : ℝ} : (a * sin y + b * cos z + c) ^ 2 ≤ (a ^ 2 + b ^ 2 + c ^ 2) * (sin y ^ 2 + cos z ^ 2 + 1 ^ 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_16703; immutable original Prove2Me node 0a0d6d11-938b-46d9-86aa-a51d9e759fff

View graph