inner_right_fintype — Mathlib

English

The inner product of sums equals the sum of inner products in an orthogonal family.

Русский

Скалярное произведение сумм равно сумме скалярных произведений для ортогональной семьи.

LaTeX

$$⟪∑ i∈s V_i(l₁ i), ∑ j∈s V_j(l₂ j)⟫ = ∑ i∈s ⟪l₁ i, l₂ i⟫$$

Lean4

theorem inner_right_fintype [Fintype ι] (l : ∀ i, G i) (i : ι) (v : G i) : ⟪V i v, ∑ j : ι, V j (l j)⟫ = ⟪v, l i⟫ := by
  classical
    calc
    ⟪V i v, ∑ j : ι, V j (l j)⟫ = ∑ j : ι, ⟪V i v, V j (l j)⟫ := by rw [inner_sum]
    _ = ∑ j, ite (i = j) ⟪V i v, V j (l j)⟫ 0 :=
      (congr_arg (Finset.sum Finset.univ) <| funext fun j => hV.eq_ite v (l j))
    _ = ⟪v, l i⟫ := by simp only [Finset.sum_ite_eq, Finset.mem_univ, (V i).inner_map_map, if_true]

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