Commit 2024-06-13 00:50 b3e51ced

View on Github →

feat: Define Pi.orthonormalBasis (#12242) Define an orthonormal basis on a pi space from a family of orthonormal bases.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

added theorem OrthonormalBasis.reindex_toBasis

added theorem Pi.orthonormalBasis.toBasis

added theorem Pi.orthonormalBasis_apply

added theorem Pi.orthonormalBasis_repr

Modified Mathlib/Analysis/NormedSpace/PiLp.lean

added def LinearIsometryEquiv.piLpCurry

added theorem LinearIsometryEquiv.piLpCurry_apply

added theorem LinearIsometryEquiv.piLpCurry_symm_apply