| Name | Category | Theorems |
|---|
addEquiv π | CompOp | 7 mathmath: addEquiv_apply, toAddEquiv_linearEquiv, linearEquiv_apply, coe_addEquiv, addEquiv_symm_apply, linearEquiv_symm_apply, coe_symm_addEquiv
|
delabToLp π | CompOp | β |
equiv π | CompOp | 8 mathmath: toEquiv_uniformEquivProd, PiLp.toEquiv_uniformEquiv, equiv_symm_apply, equiv_apply, PiLp.toEquiv_homeomorph, toEquiv_homeomorphProd, EuclideanSpace.measurableEquiv_toEquiv, equiv_symm_apply_ofLp
|
instAddAction π | CompOp | β |
instAddCommGroup π | CompOp | 166 mathmath: Matrix.l2_opNorm_toEuclideanCLM, Pi.comul_eq_adjoint, PiLp.continuousLinearEquiv_symm_apply, ofLp_listSum, PiLp.basisFun_equivFun, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, EuclideanSpace.closedBall_zero_eq, Submodule.toLinearEquiv_orthogonalDecomposition_symm, Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, addEquiv_apply, Matrix.l2_opNorm_mulVec, coe_linearEquiv, ofLp_neg, ofLp_sub, Submodule.toLinearEquiv_orthogonalDecomposition, ofLp_multisetSum, instModuleFinite, prod_norm_eq_idemFst_of_L1, LinearEquiv.coe_withLpCongr, Matrix.spectrum_toLpLin, sndL_apply, Behrend.sphere_subset_preimage_metric_sphere, prodContinuousLinearEquiv_symm_apply, neg_snd, Matrix.toLpLin_mul_same, sub_fst, PiLp.coe_continuousLinearEquiv, Matrix.toEuclideanLin_apply, LinearMap.withLpMap_id, idemSnd_compl, Submodule.coe_orthogonalDecomposition_symm, MeasureTheory.charFunDual_pi', Pi.counit_eq_adjoint, differentiable_euclidean, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.coe_toOrthonormalBasis_repr, toLp_multisetSum, zero_fst, PiLp.sub_apply, Matrix.toLpLin_symm_pow, toLp_zero, coe_addEquiv_lpPiLp_symm, Matrix.toEuclideanCLM_toLp, PiLp.hasFDerivAt_toLp, Matrix.toLpLin_one, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.withLpMap_comp, toAddEquiv_linearEquiv, Matrix.l2_opNNNorm_mulVec, add_snd, PiLp.basisFun_repr, Matrix.toLpLin_pow, prod_norm_eq_idemFst_sup_idemSnd, Matrix.ofLp_toLpLin, Module.Basis.coe_toOrthonormalBasis_repr_symm, prod_norm_eq_add_idemFst, Submodule.coe_orthogonalDecomposition, LinearIsometryEquiv.piLpCurry_apply, LinearEquiv.withLpCongr_refl, EuclideanSpace.sphere_zero_eq, hasStrictFDerivAt_piLp, toLp_listSum, prodContinuousLinearEquiv_symm_apply_ofLp, PiLp.basisFun_apply, idemFst_compl, Matrix.toLpLin_toLp, hasFDerivWithinAt_piLp, differentiableOn_piLp, Matrix.ofLp_toEuclideanCLM, ofLp_eq_zero, coe_fstL, Matrix.toLpLin_symm_id, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, ProbabilityTheory.indepFun_iff_charFunDual_prod', differentiableAt_piLp, toLp_sum, IccLeftChart_extend_bot, Matrix.l2_opNNNorm_def, Submodule.sndL_comp_coe_orthogonalDecomposition, modelWithCornersEuclideanHalfSpace_zero, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, Pi.orthonormalBasis.toBasis, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, PiLp.projβ_apply, LinearIsometryEquiv.piLpCurry_symm_apply, hasFDerivWithinAt_euclidean, sndβ_apply, PiLp.hasStrictFDerivAt_apply, Matrix.toEuclideanLin_eq_toLin, Matrix.isHermitian_iff_isSymmetric, PiLp.add_apply, PiLp.basisFun_eq_pi_basisFun, differentiableAt_euclidean, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, neg_fst, differentiableOn_euclidean, EuclideanSpace.ball_zero_eq, differentiable_piLp, idemSnd_apply, Matrix.ofLp_toEuclideanLin_apply, toLp_neg, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', linearEquiv_apply, PiLp.basis_toMatrix_basisFun_mul, toLp_add, MeasureTheory.charFunDual_prod', coe_sndL, PiLp.hasFDerivAt_ofLp, ofLp_add, LinearEquiv.withLpCongr_symm, LinearMap.coe_withLpMap, idemFst_add_idemSnd, add_fst, idemFst_apply, Matrix.toLpLin_mul, MeasureTheory.charFunDual_eq_pi_iff', coe_addEquiv_lpPiLp, sub_snd, Matrix.toEuclideanLin_apply_piLp_toLp, zero_snd, PiLp.hasFDerivAt_apply, volume_euclideanSpace_eq_dirac, coe_addEquiv, PiLp.proj_apply, Matrix.toLpLin_symm_comp, Submodule.fstL_comp_coe_orthogonalDecomposition, toLp_eq_zero, PiLp.neg_apply, PiLp.coe_symm_continuousLinearEquiv, LinearIsometryEquiv.withLpProdAssoc_apply, NumberField.mixedEmbedding.euclidean.finrank, ofLp_zero, PiLp.zero_apply, addEquiv_symm_apply, ofLp_sum, differentiableWithinAt_piLp, PiLp.hasStrictFDerivAt_ofLp, Matrix.cstar_norm_def, PiLp.basisFun_map, PiLp.continuousLinearEquiv_apply, linearEquiv_symm_apply, coe_symm_linearEquiv, Matrix.toLpLin_apply, LinearEquiv.withLpCongr_trans, EuclideanSpace.single_eq_zero_iff, Matrix.l2_opNorm_def, Matrix.toEuclideanLin_toLp, toLp_sub, instProdIsBoundedSMul, fstL_apply, IccRightChart_extend_top, Matrix.toLpLinAlgEquiv_symm_apply, PiLp.instIsBoundedSMul, MeasureTheory.charFunDual_eq_prod_iff', InnerProductSpace.symm_toEuclideanLin_rankOne, coe_symm_addEquiv, Matrix.toLpLin_eq_toLin, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, LinearIsometryEquiv.withLpProdAssoc_symm_apply, fstβ_apply, prodContinuousLinearEquiv_apply, PiLp.hasStrictFDerivAt_toLp, hasStrictFDerivAt_euclidean
|
instDecidableEq π | CompOp | β |
instDistribMulAction π | CompOp | 6 mathmath: Matrix.l2_opNorm_toEuclideanCLM, Matrix.cstar_nnnorm_def, Matrix.toEuclideanCLM_toLp, Matrix.ofLp_toEuclideanCLM, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, Matrix.cstar_norm_def
|
instModule π | CompOp | 177 mathmath: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, Pi.comul_eq_adjoint, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, PiLp.continuousLinearEquiv_symm_apply, PiLp.basisFun_equivFun, Submodule.orthogonalDecomposition_symm_apply, LinearIsometryEquiv.piLpCongrRight_symm, Submodule.toLinearEquiv_orthogonalDecomposition_symm, OrthonormalBasis.repr_injective, LinearIsometryEquiv.withLpProdComm_symm, Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, Matrix.l2_opNorm_mulVec, coe_linearEquiv, LinearMap.IsSymmetric.diagonalization_apply_self_apply, Submodule.toLinearEquiv_orthogonalDecomposition, instModuleFinite, LinearEquiv.coe_withLpCongr, Matrix.spectrum_toLpLin, sndL_apply, prodContinuousLinearEquiv_symm_apply, ProbabilityTheory.HasGaussianLaw.toLp_pi, OrthonormalBasis.repr_self, LinearIsometryEquiv.piLpCongrRight_apply, Matrix.toLpLin_mul_same, OrthonormalBasis.measurePreserving_repr, PiLp.coe_continuousLinearEquiv, Matrix.toEuclideanLin_apply, LinearMap.withLpMap_id, Euclidean.closedBall_eq_image, Submodule.coe_orthogonalDecomposition_symm, MeasureTheory.charFunDual_pi', Quaternion.linearIsometryEquivTuple_symm_apply, Pi.counit_eq_adjoint, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.coe_toOrthonormalBasis_repr, LinearIsometryEquiv.piLpCongrLeft_apply, OrthonormalBasis.coe_ofRepr, Complex.orthonormalBasisOneI_repr_apply, Matrix.toLpLin_symm_pow, Matrix.toEuclideanCLM_toLp, PiLp.hasFDerivAt_toLp, Matrix.toLpLin_one, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.IsSymmetric.diagonalization_symm_apply, LinearMap.withLpMap_comp, toAddEquiv_linearEquiv, OrthonormalBasis.tensorProduct_repr_tmul_apply', Matrix.l2_opNNNorm_mulVec, PiLp.basisFun_repr, Matrix.toLpLin_pow, OrthonormalBasis.equiv_apply, Matrix.ofLp_toLpLin, Module.Basis.coe_toOrthonormalBasis_repr_symm, OrthonormalBasis.repr_apply_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, Submodule.coe_orthogonalDecomposition, LinearIsometryEquiv.piLpCurry_apply, LinearEquiv.withLpCongr_refl, hasStrictFDerivAt_piLp, LinearMap.toMatrix_innerββ_apply, prodContinuousLinearEquiv_symm_apply_ofLp, PiLp.basisFun_apply, LinearIsometryEquiv.piLpCongrRight_single, finrank_euclideanSpace, Matrix.toLpLin_toLp, Submodule.fst_orthogonalDecomposition_apply, hasFDerivWithinAt_piLp, differentiableOn_piLp, Matrix.ofLp_toEuclideanCLM, coe_fstL, Matrix.toLpLin_symm_id, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, ProbabilityTheory.indepFun_iff_charFunDual_prod', LinearIsometryEquiv.withLpProdCongr_symm_apply, differentiableAt_piLp, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, Matrix.l2_opNNNorm_def, EuclideanSpace.basisFun_repr, Submodule.sndL_comp_coe_orthogonalDecomposition, Complex.orthonormalBasisOneI_repr_symm_apply, LinearIsometryEquiv.piLpCongrRight_refl, coe_lpPiLpβα΅’, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, LinearIsometryEquiv.coe_withLpProdUnique, OrthonormalBasis.sum_repr_symm, Pi.orthonormalBasis.toBasis, PiLp.projβ_apply, OrthonormalBasis.measurePreserving_repr_symm, EuclideanSpace.piLpCongrLeft_single, LinearIsometryEquiv.piLpCurry_symm_apply, hasFDerivWithinAt_euclidean, sndβ_apply, PiLp.hasStrictFDerivAt_apply, Matrix.toEuclideanLin_eq_toLin, Euclidean.closedBall_eq_preimage, Matrix.isHermitian_iff_isSymmetric, PiLp.basisFun_eq_pi_basisFun, InnerProductSpace.toMatrix_rankOne, differentiableAt_euclidean, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, differentiableOn_euclidean, coe_lpPiLpβα΅’_symm, differentiable_piLp, Matrix.ofLp_toEuclideanLin_apply, Euclidean.ball_eq_preimage, OrthonormalBasis.repr_symm_single, LinearIsometryEquiv.withLpProdCongr_apply, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', linearEquiv_apply, LinearIsometryEquiv.withLpProdUnique_symm_apply, toMatrix_innerSL_apply, PiLp.basis_toMatrix_basisFun_mul, MeasureTheory.charFunDual_prod', coe_sndL, PiLp.hasFDerivAt_ofLp, LinearEquiv.withLpCongr_symm, LinearMap.coe_withLpMap, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', Matrix.toLpLin_mul, MeasureTheory.charFunDual_eq_pi_iff', Matrix.toEuclideanLin_apply_piLp_toLp, LinearIsometryEquiv.withLpProdUnique_apply, PiLp.hasFDerivAt_apply, OrthonormalBasis.coe_toBasis_repr, PiLp.proj_apply, OrthonormalBasis.sum_repr, Matrix.toLpLin_symm_comp, Submodule.fstL_comp_coe_orthogonalDecomposition, LinearIsometryEquiv.piLpCongrLeft_single, OrthonormalBasis.coe_toBasis_repr_apply, PiLp.coe_symm_continuousLinearEquiv, LinearIsometry.withLpProdMap_apply, Submodule.snd_orthogonalDecomposition_apply, LinearIsometryEquiv.withLpProdComm_apply, LinearIsometryEquiv.withLpProdAssoc_apply, NumberField.mixedEmbedding.euclidean.finrank, ProbabilityTheory.HasGaussianLaw.toLp_prodMk, Submodule.orthogonalDecomposition_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, differentiableWithinAt_piLp, PiLp.hasStrictFDerivAt_ofLp, Matrix.cstar_norm_def, PiLp.basisFun_map, Quaternion.linearIsometryEquivTuple_apply, PiLp.continuousLinearEquiv_apply, linearEquiv_symm_apply, coe_symm_linearEquiv, Matrix.toLpLin_apply, LinearEquiv.withLpCongr_trans, Matrix.l2_opNorm_def, Matrix.toEuclideanLin_toLp, LinearIsometryEquiv.piLpCongrLeft_symm, LinearIsometryEquiv.withLpUniqueProd_apply, Pi.orthonormalBasis_repr, fstL_apply, Matrix.toLpLinAlgEquiv_symm_apply, MeasureTheory.charFunDual_eq_prod_iff', finrank_euclideanSpace_fin, LinearIsometryEquiv.withLpUniqueProd_symm_apply, OrthonormalBasis.repr_reindex, InnerProductSpace.symm_toEuclideanLin_rankOne, OrthonormalBasis.tensorProduct_repr_tmul_apply, Matrix.toLpLin_eq_toLin, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, LinearIsometryEquiv.withLpProdAssoc_symm_apply, LinearIsometryEquiv.coe_withLpUniqueProd, fstβ_apply, prodContinuousLinearEquiv_apply, PiLp.hasStrictFDerivAt_toLp, hasStrictFDerivAt_euclidean
|
instMulAction π | CompOp | β |
instSMul π | CompOp | 13 mathmath: ofLp_smul, smul_snd, PiLp.instNormSMulClass, EuclideanHalfSpace.convex, EuclideanQuadrant.convex, instIsScalarTower, PiLp.smul_apply, toLp_smul, smul_fst, instProdNormSMulClass, instSMulCommClass, instProdIsBoundedSMul, PiLp.instIsBoundedSMul
|
instUnique π | CompOp | β |
instVAdd π | CompOp | 2 mathmath: instVAddCommClass, instVAddAssocClass
|
linearEquiv π | CompOp | 15 mathmath: PiLp.basisFun_equivFun, Submodule.toLinearEquiv_orthogonalDecomposition_symm, coe_linearEquiv, Submodule.toLinearEquiv_orthogonalDecomposition, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.coe_toOrthonormalBasis_repr, toAddEquiv_linearEquiv, Module.Basis.coe_toOrthonormalBasis_repr_symm, Pi.orthonormalBasis.toBasis, PiLp.basisFun_eq_pi_basisFun, linearEquiv_apply, OrthonormalBasis.coe_toBasis_repr, PiLp.basisFun_map, linearEquiv_symm_apply, coe_symm_linearEquiv
|
map π | CompOp | 6 mathmath: LinearEquiv.coe_withLpCongr, coe_congr, map_comp, Isometry.withLpProdMap, map_id, LinearMap.coe_withLpMap
|
ofLp π | CompOp | 226 mathmath: OrthonormalBasis.singleton_repr, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, prod_inner_apply, ofLp_listSum, PiLp.nndist_eq_sum, measurable_ofLp, ofLp_smul, EuclideanSpace.closedBall_zero_eq, addEquiv_apply, Matrix.l2_opNorm_mulVec, frontier_halfSpace, coe_linearEquiv, prod_nnnorm_ofLp, ofLp_neg, LinearMap.IsSymmetric.diagonalization_apply_self_apply, PiLp.norm_ofLp, ofLp_sub, ofLp_multisetSum, EuclideanSpace.inner_single_left, EuclideanSpace.norm_sq_eq, EuclideanHalfSpace.ext_iff, ofLp_fst, Matrix.IsHermitian.eigenvalues_eq, LinearIsometryEquiv.piLpCongrRight_apply, EuclideanSpace.nndist_eq, PiLp.nnnorm_eq_of_L2, MeasureTheory.integrable_piLp_iff, Matrix.IsHermitian.eigenvectorUnitary_col_eq, PiLp.coe_continuousLinearEquiv, Matrix.toEuclideanLin_apply, coe_equiv_lpPiLp_symm, Quaternion.linearIsometryEquivTuple_symm_apply, PiLp.dist_eq_card, unitization_algebraMap, MeasurableEquiv.toLp_symm_apply, differentiable_euclidean, contDiffWithinAt_euclidean, contDiffAt_piLp_apply, IccLeftChart_extend_interior_pos, Matrix.IsHermitian.eigenvectorUnitary_mulVec, PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp, MeasureTheory.charFun_eq_prod_iff, LinearIsometryEquiv.piLpCongrLeft_apply, PiLp.sub_apply, Complex.orthonormalBasisOneI_repr_apply, PiLp.edist_eq_sum, PiLp.nndist_apply_le, coe_addEquiv_lpPiLp_symm, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.IsSymmetric.diagonalization_symm_apply, OrthonormalBasis.tensorProduct_repr_tmul_apply', PiLp.dist_eq_of_L1, PiLp.enorm_apply_le, prod_isometry_ofLp_infty, Matrix.l2_opNNNorm_mulVec, PiLp.nnnorm_apply_le, frontier_range_modelWithCornersEuclideanHalfSpace, PiLp.basisFun_repr, prod_norm_ofLp, OrthonormalBasis.equiv_apply, Matrix.ofLp_toLpLin, interior_halfSpace, PiLp.dist_eq_iSup, toLp_ofLp, PiLp.norm_eq_sum, MeasureTheory.charFun_pi, MeasureTheory.Integrable.eval_piLp, OrthonormalBasis.repr_apply_apply, EuclideanHalfSpace.convex, LinearIsometryEquiv.piLpCurry_apply, PiLp.lipschitzWith_ofLp, EuclideanSpace.sphere_zero_eq, hasStrictFDerivAt_piLp, LinearMap.toMatrix_innerββ_apply, prodContinuousLinearEquiv_symm_apply_ofLp, contDiffAt_euclidean, contDiffOn_euclidean, PiLp.volume_preserving_ofLp, hasFDerivWithinAt_piLp, differentiableOn_piLp, InnerProductGeometry.norm_ofLp_crossProduct, prod_lipschitzWith_ofLp, closure_open_halfSpace, Matrix.ofLp_toEuclideanCLM, ofLp_eq_zero, PiLp.nnnorm_eq_ciSup, differentiableWithinAt_euclidean, PiLp.norm_sq_eq_of_L2, PiLp.isOpenMap_apply, ofLp_injective, PiLp.norm_eq_of_L1, coe_equiv_lpPiLp, LinearIsometryEquiv.withLpProdCongr_symm_apply, differentiableAt_piLp, contDiff_ofLp, range_euclideanHalfSpace, prod_uniformContinuous_ofLp, contDiff_piLp, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, PiLp.norm_eq_ciSup, EuclideanSpace.basisFun_repr, ProbabilityTheory.indepFun_iff_charFun_prod, OrthonormalBasis.equiv_apply_euclideanSpace, PiLp.dist_apply_le, PiLp.edist_eq_iSup, Complex.orthonormalBasisOneI_repr_symm_apply, IsometryEquiv.withLpProdCongr_apply, PiLp.continuous_apply, coe_lpPiLpβα΅’, unitization_norm_def, EuclideanSpace.norm_eq, Matrix.IsHermitian.eigenvectorUnitary_apply, PiLp.edist_apply_le, contDiffOn_piLp, PiLp.antilipschitzWith_ofLp, ProbabilityTheory.covarianceBilin_apply_pi, EuclideanSpace.inner_eq_star_dotProduct, OrthonormalBasis.sum_repr_symm, PiLp.smul_apply, equiv_apply, PiLp.projβ_apply, MeasureTheory.MemLp.eval_piLp, MeasureTheory.memLp_piLp_iff, ofLp_surjective, unitizationAlgEquiv_symm_apply_ofLp, PiLp.analyticOn_ofLp, LinearIsometryEquiv.piLpCurry_symm_apply, hasFDerivWithinAt_euclidean, PiLp.dist_sq_eq_of_L2, PiLp.hasStrictFDerivAt_apply, PiLp.add_apply, EuclideanSpace.basisFun_inner, InnerProductSpace.toMatrix_rankOne, EuclideanSpace.ofLp_single, differentiableAt_euclidean, PiLp.continuous_ofLp, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, PiLp.norm_eq_of_nat, PiLp.toLp_apply, differentiableOn_euclidean, EuclideanSpace.ball_zero_eq, coe_lpPiLpβα΅’_symm, PiLp.norm_apply_le, differentiable_piLp, contDiffOn_piLp_apply, Matrix.ofLp_toEuclideanLin_apply, EuclideanSpace.inner_basisFun_real, iccLeftChart_extend_zero, interior_range_modelWithCornersEuclideanHalfSpace, toMatrix_innerSL_apply, PiLp.edist_eq_card, PiLp.nnnorm_eq_of_L1, PiLp.contDiff_ofLp, PiLp.hasFDerivAt_ofLp, ofLp_add, ProbabilityTheory.iIndepFun_iff_charFun_pi, ofLp_bijective, contDiff_piLp_apply, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', contDiffWithinAt_piLp, PiLp.uniformContinuous_ofLp, coe_addEquiv_lpPiLp, EuclideanSpace.dist_eq, PiLp.isometry_ofLp_infty, PiLp.hasFDerivAt_apply, coe_addEquiv, PiLp.proj_apply, OrthonormalBasis.sum_repr, PiLp.dist_eq_of_L2, OrthonormalBasis.coe_toBasis_repr_apply, PiLp.neg_apply, OrthonormalBasis.coe_equiv_euclideanSpace, ofLp_snd, EuclideanSpace.dist_sq_eq, Matrix.IsHermitian.eigenvectorUnitary_transpose_apply, PiLp.nnnorm_eq_sum, EuclideanSpace.coe_measurableEquiv, ofLp_zero, unitization_mul, EuclideanSpace.nnnorm_eq, PiLp.inner_apply, PiLp.ext_iff, range_modelWithCornersEuclideanHalfSpace, PiLp.zero_apply, EuclideanSpace.inner_single_right, ofLp_sum, contDiffAt_piLp, differentiableWithinAt_piLp, PiLp.hasStrictFDerivAt_ofLp, PiLp.continuousLinearEquiv_apply, unitizationAlgEquiv_apply, PiLp.norm_eq_of_L2, Matrix.toLpLin_apply, IsometryEquiv.withLpProdCongr_symm_apply, Matrix.IsHermitian.mulVec_eigenvectorBasis, closure_halfSpace, EuclideanSpace.edist_eq, EuclideanSpace.single_apply, Pi.orthonormalBasis_repr, MeasureTheory.charFun_eq_pi_iff, unitization_nnnorm_def, MeasureTheory.charFun_prod, PiLp.edist_eq_of_L1, contDiffWithinAt_piLp_apply, OrthonormalBasis.repr_reindex, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, ofLp_toLp, contDiff_euclidean, PiLp.nndist_eq_of_L2, OrthonormalBasis.tensorProduct_repr_tmul_apply, equiv_symm_apply_ofLp, RCLike.inner_eq_wInner_one, PiLp.nnnorm_ofLp, PiLp.dist_eq_sum, PiLp.sumPiLpEquivProdLpPiLp_apply_ofLp, PiLp.edist_eq_of_L2, prod_continuous_ofLp, MeasurableEquiv.coe_toLp_symm, analyticOn_ofLp, PiLp.nndist_eq_iSup, PiLp.norm_eq_card, PiLp.nndist_eq_of_L1, prod_antilipschitzWith_ofLp, prodContinuousLinearEquiv_apply, hasStrictFDerivAt_euclidean
|