Commit 2023-05-29 05:29 cfaaf51b

View on Github →

feat: port Analysis.InnerProductSpace.PiL2 (#4420) Some theorems in Analysis.InnerProductSpace.Basic, such as Orthonormal.inner_right_finsupp, accidentally gained a new DecidableEq hypothesis during the port. This removes the hypothesis by using classical! instead of classical in their proofs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Created Mathlib/Analysis/InnerProductSpace/PiL2.lean

added theorem Basis.coe_toOrthonormalBasis

added theorem Basis.coe_toOrthonormalBasis_repr

added theorem Basis.coe_toOrthonormalBasis_repr_symm

added theorem Basis.toBasis_toOrthonormalBasis

added def Basis.toOrthonormalBasis

added theorem Complex.coe_orthonormalBasisOneI

added def Complex.isometryOfOrthonormal

added theorem Complex.isometryOfOrthonormal_apply

added theorem Complex.isometryOfOrthonormal_symm_apply

added theorem Complex.map_isometryOfOrthonormal

added def Complex.orthonormalBasisOneI

added theorem Complex.orthonormalBasisOneI_repr_apply

added theorem Complex.orthonormalBasisOneI_repr_symm_apply

added theorem Complex.toBasis_orthonormalBasisOneI

added theorem DirectSum.IsInternal.collectedOrthonormalBasis_mem

added def DirectSum.IsInternal.isometryL2OfOrthogonalFamily

added theorem DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply

added theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate

added theorem EuclideanSpace.dist_eq

added theorem EuclideanSpace.dist_single_same

added theorem EuclideanSpace.edist_eq

added theorem EuclideanSpace.edist_single_same

added def EuclideanSpace.equiv

added theorem EuclideanSpace.inner_eq_star_dotProduct

added theorem EuclideanSpace.inner_piLp_equiv_symm

added theorem EuclideanSpace.inner_single_left

added theorem EuclideanSpace.inner_single_right

added theorem EuclideanSpace.nndist_eq

added theorem EuclideanSpace.nndist_single_same

added theorem EuclideanSpace.nnnorm_eq

added theorem EuclideanSpace.nnnorm_single

added theorem EuclideanSpace.norm_eq

added theorem EuclideanSpace.norm_single

added theorem EuclideanSpace.orthonormal_single

added theorem EuclideanSpace.piLpCongrLeft_single

added def EuclideanSpace.proj

added def EuclideanSpace.projₗ

added def EuclideanSpace.single

added theorem EuclideanSpace.single_apply

added def EuclideanSpace

added theorem LinearIsometry.extend_apply

added theorem Matrix.piLp_equiv_toEuclideanLin

added def Matrix.toEuclideanLin

added theorem Matrix.toEuclideanLin_eq_toLin

added theorem Matrix.toEuclideanLin_piLp_equiv_symm

added theorem Orthonormal.exists_orthonormalBasis_extension

added theorem Orthonormal.exists_orthonormalBasis_extension_of_card_eq

added theorem OrthonormalBasis.coe_ofRepr

added theorem OrthonormalBasis.det_to_matrix_orthonormalBasis

added theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_real

added def OrthonormalBasis.fromOrthogonalSpanSingleton

added def OrthonormalBasis.reindex

added theorem OrthonormalBasis.repr_injective

added theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal

added theorem OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary

added structure OrthonormalBasis

added theorem PiLp.equiv_single

added theorem PiLp.equiv_symm_single

added theorem PiLp.inner_apply

added theorem exists_orthonormalBasis

added theorem finrank_euclideanSpace

added theorem finrank_euclideanSpace_fin

added theorem inner_matrix_col_col

added theorem inner_matrix_row_row

added theorem orthonormalBasis_one_dim

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean