English
Let f, g1, g2 be vectors in the product of inner product spaces with weight w. The weighted inner product is additive in the second argument: ⟪f, g1 − g2⟫_{𝕜, w} = ⟪f, g1⟫_{𝕜, w} − ⟪f, g2⟫_{𝕜, w}.
Русский
Пусть f, g1, g2 — векторы в произведении евклидовых пространств с весом w. Взвешенное скалярное произведение линейно по второму аргументу: ⟪f, g1 − g2⟫_{𝕜, w} = ⟪f, g1⟫_{𝕜, w} − ⟪f, g2⟫_{𝕜, w}.
LaTeX
$$$\ll f, g_1 - g_2 \gg_{\mathbb{K}, w} = \ll f, g_1 \gg_{\mathbb{K}, w} - \ll f, g_2 \gg_{\mathbb{K}, w}$$$
Lean4
theorem wInner_sub_right (w : ι → ℝ) (f g₁ g₂ : ∀ i, E i) : ⟪f, g₁ - g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] - ⟪f, g₂⟫_[𝕜, w] := by
simp_rw [sub_eq_add_neg, wInner_add_right, wInner_neg_right]
