English
Cauchy–Schwarz for finites: sum over i of sqrt(f_i) sqrt(g_i) ≤ sqrt(sum f_i) sqrt(sum g_i) for f_i,g_i ≥ 0.
Русский
Неравенство Коши-Шварца для конечных сумм: сумма sqrt(f_i) sqrt(g_i) ≤ sqrt(sum f_i) sqrt(sum g_i) при f_i,g_i ≥ 0.
LaTeX
$$$\\\\sum_{i \\\\in s} \\sqrt{f(i)} \\sqrt{g(i)} \\\\le \\\\sqrt{\\\\sum_{i \\\\in s} f(i)} \\\\cdot \\\\sqrt{\\\\sum_{i \\\\in s} g(i)}$$$
Lean4
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`. -/
theorem sum_sqrt_mul_sqrt_le (s : Finset ι) (f g : ι → ℝ≥0) :
∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i) := by
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ sqrt (f x)) (fun x ↦ sqrt (g x))
