hasSum_linearIsometryEquiv_symm — Mathlib

English

For every w ∈ ℓ^2(G), the series ∑_i V_i(w_i) converges in E and sums to h_V.linearIsometryEquiv.symm w.

Русский

Для каждого w ∈ ℓ^2(G) ряд ∑_i V_i(w_i) сходится в E и складывается в h_V.linearIsometryEquiv.symm 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` and `lp G 2`,
a vector `w : lp G 2` is the image of the infinite sum of the associated elements in `E`, and this
sum indeed converges. -/
protected theorem hasSum_linearIsometryEquiv_symm (hV : IsHilbertSum 𝕜 G V) (w : lp G 2) :
    HasSum (fun i => V i (w i)) (hV.linearIsometryEquiv.symm w) := by
  simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.hasSum_linearIsometry]

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