sum_mul_le_sqrt_mul_sqrt — Mathlib

English

Cauchy–Schwarz inequality for finite sums in ℝ≥0: for s Finset and f,g: s → ℝ≥0, ∑ f i g i ≤ sqrt(∑ f i^2) sqrt(∑ g i^2).

Русский

Неравенство Штюнера (Коши) для конечных сумм в ℝ≥0: ∑ f_i g_i ≤ sqrt(∑ f_i^2) sqrt(∑ g_i^2).

LaTeX

$$$\\\\sum_{i \\\\in s} f(i) \\\\cdot g(i) \\\\le \\\\sqrt{\\\\sum_{i \\\\in s} f(i)^2} \\\\cdot \\\\sqrt{\\\\sum_{i \\\\in s} g(i)^2}$$$

Lean4

/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`. -/
theorem sum_mul_le_sqrt_mul_sqrt (s : Finset ι) (f g : ι → ℝ≥0) :
    ∑ i ∈ s, f i * g i ≤ sqrt (∑ i ∈ s, f i ^ 2) * sqrt (∑ i ∈ s, g i ^ 2) :=
  (le_sqrt_iff_sq_le.2 <| sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq <| sqrt_mul _ _

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