mathlib

6d200cb1 - feat(analysis/normed_space/inner_product): Bessel's inequality (#8251)

feat(analysis/normed_space/inner_product): Bessel's inequality (#8251) A proof both of Bessel's inequality and that the infinite sum defined by Bessel's inequality converges.