sum_mul_le_sqrt_mul_sqrt — Mathlib

English

For Finset s and real-valued f,g, ∑ f_i g_i ≤ sqrt(∑ f_i^2) sqrt(∑ g_i^2).

Русский

Для конечного множества индексов и действительных f,g: ∑ f_i g_i ≤ sqrt(∑ f_i^2) sqrt(∑ g_i^2).

LaTeX

$$$\\\\sum_{i \\\\in s} f(i) 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 `ℝ`. -/
theorem sum_mul_le_sqrt_mul_sqrt (s : Finset ι) (f g : ι → ℝ) :
    ∑ i ∈ s, f i * g i ≤ √(∑ i ∈ s, f i ^ 2) * √(∑ i ∈ s, g i ^ 2) :=
  (le_sqrt_of_sq_le <| sum_mul_sq_le_sq_mul_sq _ _ _).trans_eq <| sqrt_mul (sum_nonneg fun _ _ ↦ by positivity) _

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