le_prod_of_submultiplicative_of_nonneg

English

Cauchy–Schwarz for finite multisets/finite index sets: (∑ f_i g_i)^2 ≤ (∑ f_i^2)(∑ g_i^2).

Русский

Коши–Шварц для конечного набора индексов: (∑ 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

theorem le_prod_of_submultiplicative_of_nonneg (f : α → β) (h0 : ∀ a, 0 ≤ f a) (h_one : f 1 ≤ 1)
    (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) : f s.prod ≤ (s.map f).prod :=
  le_prod_of_submultiplicative_on_pred_of_nonneg f (fun _ ↦ True) h0 h_one (fun x y _ _ ↦ h_mul x y) (by simp) s
    (by simp)

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