Commit 2023-06-02 03:45 3eaf72e1

View on Github →

feat: port Analysis.InnerProductSpace.l2Space (#4555)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/l2Space.lean

added theorem HilbertBasis.coe_toOrthonormalBasis

added theorem HilbertBasis.finite_spans_dense

added structure HilbertBasis

added theorem IsHilbertSum.mk

added theorem IsHilbertSum.mkInternal

added structure IsHilbertSum

added theorem Orthonormal.exists_hilbertBasis_extension

added theorem Orthonormal.isHilbertSum

added theorem Orthonormal.linearIsometryEquiv_symm_apply_single_one

added theorem OrthonormalBasis.coe_toHilbertBasis

added theorem Submodule.isHilbertSumOrthogonal

added theorem exists_hilbertBasis

added theorem lp.hasSum_inner

added theorem lp.inner_eq_tsum

added theorem lp.inner_single_left

added theorem lp.inner_single_right

added theorem lp.summable_inner