linearIsometryEquiv_symm_apply_dfinsupp_sum_single

English

For a Hilbert sum structure, the infinite sum over i of V_i(w_i) converges to the image under the symm isometry of w.

Русский

Для гильбертовой суммы бесконечная сумма по i образует предел, равный образу w при симметричной изометрии.

LaTeX

$$$ HasSum (\\lambda i, V_i(w_i)) (h_V.linearIsometryEquiv.symm w) $$$

Lean4

/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
`lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
elements of `E`. -/
protected theorem linearIsometryEquiv_symm_apply_dfinsupp_sum_single [DecidableEq ι] [∀ i, DecidableEq (G i)]
    (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ i : ι, G i) :
    hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun i => V i := by
  simp only [map_dfinsuppSum, IsHilbertSum.linearIsometryEquiv_symm_apply_single]

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