lean_workbook_plus_2833

Proved

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

Let $a_1,a_2,\cdots,a_n \in[0,1]$ $(n\ge 2).$ Prove that

\sum_{i=1}^{n}\left(\prod_{j\neq i}\sqrt{a^n_j }\sqrt{(1-a_i)}\right)\leq 1.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2833 (n : ℕ) (a : Fin n → ℝ) (ha : ∀ i, a i ∈ Set.Icc 0 1) :
  ∑ i, (∏ j, if j ≠ i then Real.sqrt (a j ^ n) * Real.sqrt (1 - a i) else 0) ≤ 1   :=  by sorry

Source

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

View graph