sum_mul_sq_le_sq_mul_sq — Mathlib

English

A squared form of Cauchy–Schwarz for finite sums: (∑ f_i g_i)^2 ≤ (∑ f_i^2)(∑ g_i^2) under nonnegativity assumptions.

Русский

Квадратная форма неравенства Коши–Шварца для конечных сумм: (∑ f_i g_i)^2 ≤ (∑ f_i^2)(∑ g_i^2) при допустимых условиях неотрицательности.

LaTeX

$$$\left(\sum_{i\in s} f(i) g(i)\right)^2 \le \left(\sum_{i\in s} f(i)^2\right)\left(\sum_{i\in s} g(i)^2\right)$$$

Lean4

/-- **Cauchy-Schwarz inequality** for finsets, squared version. -/
theorem sum_mul_sq_le_sq_mul_sq [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R]
    (s : Finset ι) (f g : ι → R) : (∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2 :=
  sum_sq_le_sum_mul_sum_of_sq_eq_mul s (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ mul_pow ..)

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