Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-11 19:28 6d200cb1

View on Github →

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.

Estimated changes