sum_sq_le_sq_sum_of_nonneg — Mathlib

English

If f(i) ≥ 0 for all i in s, then the sum of squares is at most the square of the sum: ∑ f(i)^2 ≤ (∑ f(i))^2.

Русский

Если f(i) ≥ 0 для всех i, тогда сумма квадратов не превосходит квадрата суммы: ∑ f(i)^2 ≤ (∑ f(i))^2.

LaTeX

$$$$\\sum_{i \\in s} f(i)^2 \\le \\left(\\sum_{i \\in s} f(i)\\right)^2 \\quad \\text{for } f(i) \\ge 0.$$$$

Lean4

theorem sum_sq_le_sq_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2 :=
  by
  simp only [sq, sum_mul_sum]
  refine sum_le_sum fun i hi ↦ ?_
  rw [← mul_sum]
  gcongr
  · exact hf i hi
  · exact single_le_sum hf hi

Похожие утверждения