mul_wInner_left — Mathlib

English

When w is the constant function equal to 1, the weighted inner product coincides with the standard inner product on the product space, i.e., ⟪f, g⟫_{𝕜,1} = ∑_i ⟪f_i, g_i⟫.

Русский

При весе w ≡ 1 взвешенное скалярное произведение совпадает с обычным скалярным произведением: ⟪f, g⟫_{𝕜,1} = ∑_i ⟪f_i, g_i⟫.

LaTeX

$$$⟪f, g⟫_{𝕜, w} = \sum_i ⟪f_i, g_i⟫_𝕜 \quad (w = 1)$$$

Lean4

theorem mul_wInner_left (c : 𝕜) (w : ι → ℝ) (f g : ∀ i, E i) : c * ⟪f, g⟫_[𝕜, w] = ⟪star c • f, g⟫_[𝕜, w] := by
  rw [wInner_smul_left, star_star, smul_eq_mul]

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