Prove2Me

A two-row linear-map bound under norm constraints

Proved
WorkbookSource.plus_81471

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that (ax+by)2+(cx+dy)2≤116(ax+by)^2+(cx+dy)^2\leq\frac{1}{16}, where a2+b2+c2+d2≤116a^2+b^2+c^2+d^2\leq\frac{1}{16} and x2+y2=1x^2+y^2=1.

Source: InternLM Lean-Workbook, record lean_workbook_plus_81471 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.plus_81471 (a b c d x y : ℝ) (h1 : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 ≤ 1 / 16) (h2 : x ^ 2 + y ^ 2 = 1) : (a * x + b * y) ^ 2 + (c * x + d * y) ^ 2 ≤ 1 / 16   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_81471; Apache-2.0

View graph