wInner_nonneg — Mathlib

English

If w, f, g are coordinatewise nonnegative, then ⟪f,g⟫_{𝕜, w} ≥ 0.

Русский

Если все координаты неотрицательны, то взвешенное скалярное произведение неотрицательно.

LaTeX

$$0 ≤ ⟪f,g⟫_{𝕜,w} (with w ≥ 0, f ≥ 0, g ≥ 0)$$

Lean4

theorem wInner_nonneg (hw : 0 ≤ w) (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[𝕜, w] :=
  sum_nonneg fun _ _ ↦ smul_nonneg (hw _) <| mul_nonneg (hg _) (star_nonneg_iff.2 (hf _))

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