English
If an orthogonal family is given, the collected basis in the DirectSum IsInternal construction is orthonormal.
Русский
Если дано ортогональное семейство, соответствующая собранная база в конструкции DirectSum IsInternal ортонормирована.
LaTeX
$$Orthonormal 𝕜 (hV_sum.collectedBasis v_family)$$
Lean4
nonrec theorem inner_sum (l₁ l₂ : ∀ i, G i) (s : Finset ι) :
⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
classical
calc
⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
simp only [sum_inner, inner_sum]
_ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 :=
by
congr with i
congr with j
apply hV.eq_ite
_ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map, imp_self, imp_true_iff]
