sum_sq_le_sum_mul_sum_of_sq_eq_mul

English

For finite index set s and functions f,g on ι, the inequality (∑ f_i g_i)^2 ≤ (∑ f_i^2)(∑ g_i^2) holds, provided the usual ordering conditions.

Русский

Для конечного множества индексов s и функций f,g выполняется неравенство (∑ 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.

This is written in terms of sequences `f`, `g`, and `r`, where `r` is a stand-in for
`√(f i * g i)`. See `sum_mul_sq_le_sq_mul_sq` for the more usual form in terms of squared
sequences. -/
theorem sum_sq_le_sum_mul_sum_of_sq_eq_mul [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R]
    (s : Finset ι) {r f g : ι → R} (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) (ht : ∀ i ∈ s, r i ^ 2 = f i * g i) :
    (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i :=
  by
  obtain h | h := (sum_nonneg hg).eq_or_lt'
  · have ht' : ∑ i ∈ s, r i = 0 :=
      sum_eq_zero fun i hi ↦ by simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi
    rw [h, ht']
    simp
  · refine le_of_mul_le_mul_of_pos_left (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h
    calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) :=
        by
        gcongr with i hi
        have ht :
          (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 = (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
          grind
        refine
          le_of_eq_of_le ?_
            (two_mul_le_add_of_sq_eq_mul (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
        repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring

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