English
Given a Hilbert sum, the symm inverse maps the finite-difference sum of basis elements to the corresponding elementary images.
Русский
Для гильбертовой суммы симметричное обратное отображение переводит конечную сумму базисных элементов к соответствующим элементарным изображениям.
LaTeX
$$$ h_V.linearIsometryEquiv.symm (W_0.\\sum (lp.single 2)) = W_0.\\sum (\\lambda i, V_i) $$$
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`. -/
@[simp]
protected theorem linearIsometryEquiv_apply_dfinsupp_sum_single [DecidableEq ι] [∀ i, DecidableEq (G i)]
(hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ i : ι, G i) :
((W₀.sum (γ := lp G 2) fun a b ↦ hV.linearIsometryEquiv (V a b)) : ∀ i, G i) = W₀ :=
by
rw [← map_dfinsuppSum]
rw [← hV.linearIsometryEquiv_symm_apply_dfinsupp_sum_single]
rw [LinearIsometryEquiv.apply_symm_apply]
ext i
simp +contextual [DFinsupp.sum, lp.single_apply]
