Commit 2022-01-13 17:57 05044255
View on Github →feat(analysis/inner_product_space/basic): criterion for summability (#11224)
In a complete inner product space E, a family f of mutually-orthogonal elements of E is summable, if and only if
(λ i, ∥f i∥ ^ 2) is summable.