English
Let E be a Hilbert space which is the Hilbert sum of a family of Hilbert spaces (G_i) with associated isometries V_i: G_i → E. Then the inverse isometry sends a square-summable family w = (w_i) to the (convergent) sum ∑_i V_i(w_i) in E.
Русский
Пусть E — гильбертово пространство, являющееся гильбертовой суммой семейства гильбертовых пространств (G_i) с соответствующими изометриями V_i: G_i → E. Тогда обратное изометрии отображает квадрат-суммируемую последовательность w = (w_i) в сходящийся в E ряд ∑_i V_i(w_i).
LaTeX
$$$ h_V.linearIsometryEquiv.symm(w) = \\sum_{i} V_i(w_i) \\quad (w \\in \\ell^2(G,2)) $$$
Lean4
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G` and `lp G 2`,
a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`. -/
protected theorem linearIsometryEquiv_symm_apply (hV : IsHilbertSum 𝕜 G V) (w : lp G 2) :
hV.linearIsometryEquiv.symm w = ∑' i, V i (w i) := by
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply]
