English
Let s be a finite index set and f : ι → α. If f is nonnegative on s, then the square of the sum is bounded by the size of s times the sum of squares: (∑ i∈s f(i))^2 ≤ |s| ∑ i∈s f(i)^2.
Русский
Пусть s — конечное множество индексов и f : ι → α. Тогда при f(i) ≥ 0 на s выполняется неравенство: (∑ i∈s f(i))^2 ≤ |s| ∑ i∈s f(i)^2.
LaTeX
$$$\left(\sum_{i \in s} f(i)\right)^2 \le |s| \sum_{i \in s} f(i)^2$$$
Lean4
/-- Special case of **Chebyshev's Sum Inequality** or the **Cauchy-Schwarz Inequality**: The square
of the sum is less than the size of the set times the sum of the squares. -/
theorem sq_sum_le_card_mul_sum_sq : (∑ i ∈ s, f i) ^ 2 ≤ #s * ∑ i ∈ s, f i ^ 2 :=
by
simp_rw [sq]
exact (monovaryOn_self _ _).sum_mul_sum_le_card_mul_sum
