lean_workbook_plus_46069

Proved

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

The following problem is true already: Prove that for all real $x_i$ ( $\forall i=\overline{1;n}$ ) there exist $\epsilon_i\in\{-1,1\}$ so that the following inequality is true: $(\sum_{i=1}^n\epsilon_i x_i)^2\leq \sum_{i=1}^n x_i^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46069 (n : ℕ) (x : Fin n → ℝ) :
    ∃ ε : Fin n → ℝ, ∀ i, ε i = 1 ∨ ε i = -1 ∧
    (∑ i, ε i * x i) ^ 2 ≤ ∑ i, (x i) ^ 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph