dotProduct_nonneg_of_nonneg — Mathlib

English

If v and w are nonnegative vectors (componentwise) in R^n, then their dot product is nonnegative.

Русский

Если векторы v и w в R^n неотрицательны по каждому компоненту, то их скалярное произведение неотрицательно.

LaTeX

$$0 ≤ ∑_{i} v(i) w(i)$$

Lean4

theorem dotProduct_nonneg_of_nonneg {v w : n → R} (hv : 0 ≤ v) (hw : 0 ≤ w) : 0 ≤ v ⬝ᵥ w :=
  Finset.sum_nonneg (fun i _ => mul_nonneg (hv i) (hw i))

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