English
In the canonical isometric isomorphism, a finitely-supported vector maps to the finite sum of images.
Русский
В каноническом изометрическом изоморфизме вектор с конечной поддержкой отображается в конечную сумму образов.
LaTeX
$$$ h_V.linearIsometryEquiv.symm (W_0.\\sum (lp.single 2)) = W_0.\\sum (V_i) $$$
Lean4
/-- Given a total orthonormal family `v : ι → E`, `E` is a Hilbert sum of `fun i : ι => 𝕜`
relative to the family of linear isometries `fun i k => k • v i`. -/
theorem isHilbertSum {v : ι → E} (hv : Orthonormal 𝕜 v) (hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure) :
IsHilbertSum 𝕜 (fun _ : ι => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (hv.1 i) :=
IsHilbertSum.mk hv.orthogonalFamily
(by
convert hsp
simp [← LinearMap.span_singleton_eq_range, ← Submodule.span_iUnion])
