English
Let f1, f2, g be vectors in the product of inner product spaces, and let w be a finite index weight. The weighted inner product is additive in the first argument: ⟪f1 − f2, g⟫_{𝕜, w} = ⟪f1, g⟫_{𝕜, w} − ⟪f2, g⟫_{𝕜, w}.
Русский
Пусть f1, f2, g — векторы в произведении евклидовых пространств, а w — вес. Взвешенное скалярное произведение линейно по первому аргументу: ⟪f1 − f2, g⟫_{𝕜, w} = ⟪f1, g⟫_{𝕜, w} − ⟪f2, g⟫_{𝕜, w}.
LaTeX
$$$\ll f_1 - f_2, g \gg_{\mathbb{K}, w} = \ll f_1, g \gg_{\mathbb{K}, w} - \ll f_2, g \gg_{\mathbb{K}, w}$$$
Lean4
theorem wInner_sub_left (w : ι → ℝ) (f₁ f₂ g : ∀ i, E i) : ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w] := by
simp_rw [sub_eq_add_neg, wInner_add_left, wInner_neg_left]
