Weighted Cauchy--Schwarz for finite sums

This file records the form of the Cauchy--Schwarz inequality that bounds a weighted first absolute moment by the square root of the corresponding weighted second moment.

Main results

• Finset.weighted_sum_abs_le_sqrt: the weighted first-moment bound when the weights sum to at most one.

theorem Finset.weighted_sum_abs_le_sqrt {ε : ℝ} {ι : Type u_1} (s : Finset ι) (w f : ι → ℝ) (hw0 : ∀ i ∈ s, 0 ≤ w i) (hw1 : ∑ i ∈ s, w i ≤ 1) (hε : ∑ i ∈ s, w i * f i ^ 2 ≤ ε) : ∑ i ∈ s, w i * |f i| ≤ √ε

Weighted Cauchy--Schwarz. If nonnegative weights sum to at most one and the weighted sum of squares of f is at most ε, then the weighted sum of |f| is at most √ε.