English
The i-th coordinate projection in EuclideanSpace gives the i-th component; it is a linear map projecting onto the i-th coordinate.
Русский
Проекция i-й координаты в EuclideanSpace возвращает i-ую компоненту; это линейное отображение проекции на i-ю координату.
LaTeX
$$$\mathrm{proj}_\ell(i): \mathrm{EuclideanSpace}\; 𝕜\; ι \to 𝕜$$$
Lean4
@[simp]
theorem isometryL2OfOrthogonalFamily_symm_apply [DecidableEq ι] {V : ι → Submodule 𝕜 E} (hV : DirectSum.IsInternal V)
(hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (w : PiLp 2 fun i => V i) :
(hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i, (w i : E) := by
classical
let e₁ := DirectSum.linearEquivFunOnFintype 𝕜 ι fun i => V i
let e₂ := LinearEquiv.ofBijective (DirectSum.coeLinearMap V) hV
suffices ∀ v : ⨁ i, V i, e₂ v = ∑ i, e₁ v i by exact this (e₁.symm w)
intro v
simp [e₁, e₂, DirectSum.coeLinearMap, DirectSum.toModule, DFinsupp.lsum, DFinsupp.sumAddHom_apply]
