mathlib

05044255 - feat(analysis/inner_product_space/basic): criterion for summability (#11224)

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.