English
For Finset s and real-valued f,g with f_i,g_i ≥ 0, ∑ sqrt(f_i) sqrt(g_i) ≤ sqrt(∑ f_i) sqrt(∑ g_i).
Русский
Для конечного множества и неотрицательных f_i,g_i: ∑ sqrt(f_i) sqrt(g_i) ≤ sqrt(∑ f_i) sqrt(∑ g_i).
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 `ℝ`. -/
theorem sum_sqrt_mul_sqrt_le (s : Finset ι) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) :
∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i) := by
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ √(f x)) (fun x ↦ √(g x))
