A four-variable product bound at fixed squared norm

Proved

WorkbookSource.base_48397

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

lean-workbooksource-checked

$x^2+y^2+z^2+t^2=4 \implies xyzt \le 1$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_48397 (x y z t : ℝ) (h : x ^ 2 + y ^ 2 + z ^ 2 + t ^ 2 = 4) :
  x * y * z * t ≤ 1  :=  by sorry

Source