Theorems · Theorem · order theory

Finset.sum_sq_le_sq_sum_of_nonneg

∀ {ι : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {f : ι → R}
  {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2

Defined in

Mathlib.Algebra.Order.BigOperators.Ring.Finset

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPartialOrderIsOrderedRing