EuclideanSpace 📖 | CompOp | 213 mathmath: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, Pi.comul_eq_adjoint, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, EuclideanSpace.orthonormal_single, EuclideanSpace.closedBall_zero_eq, OrthonormalBasis.repr_injective, Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, Matrix.l2_opNorm_mulVec, ProbabilityTheory.isGaussian_multivariateGaussian, ProbabilityTheory.covarianceBilin_multivariateGaussian, EuclideanSpace.inner_single_left, EuclideanSpace.basisFun_toBasis, DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots, EuclideanSpace.norm_sq_eq, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, contMDiff_neg_sphere, ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian, SmoothBumpCovering.exists_immersion_euclidean, EuclideanHalfSpace.ext_iff, EuclideanSpace.basisFun_apply, Diffeology.isPlot_id', Matrix.IsHermitian.eigenvalues_eq, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, OrthonormalBasis.repr_self, Icc_isBoundaryPoint_bot, EuclideanSpace.nndist_eq, stereographic'_source, OrthonormalBasis.measurePreserving_repr, instIsAddHaarMeasureEuclideanSpaceRealFinHausdorffMeasureCast, Matrix.IsHermitian.eigenvectorUnitary_col_eq, Matrix.toEuclideanLin_apply, mfderivWithin_projIcc_one, EuclideanSpace.norm_single, Euclidean.closedBall_eq_image, ProbabilityTheory.charFun_multivariateGaussian, Quaternion.linearIsometryEquivTuple_symm_apply, Pi.counit_eq_adjoint, ProbabilityTheory.covarianceBilin_apply_basisFun_self, Icc_isInteriorPoint_interior, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, mfderivWithin_comp_projIcc_one, contDiffWithinAt_euclidean, EuclideanSpace.volume_closedBall_fin_three, IccLeftChart_extend_interior_pos, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Matrix.IsHermitian.eigenvectorUnitary_mulVec, EuclideanSpace.real_norm_sq_eq, EuclideanSpace.dist_single_same, Module.Basis.coe_toOrthonormalBasis_repr, contMDiff_coe_sphere, Matrix.gram_eq_conjTranspose_mul, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, OrthonormalBasis.coe_ofRepr, EuclideanSpace.nnnorm_single, Complex.orthonormalBasisOneI_repr_apply, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, Matrix.toEuclideanCLM_toLp, Diffeology.IsPlot.dSmooth, ProbabilityTheory.multivariateGaussian_of_not_posSemidef, DiffeologicalSpace.CorePlotsOn.isPlotOn_reparam, EuclideanSpace.volume_closedBall_fin_two, Matrix.piLp_ofLp_toEuclideanLin, stereographic'_target, OrthonormalBasis.tensorProduct_repr_tmul_apply', EuclideanSpace.coe_proj, Matrix.l2_opNNNorm_mulVec, frontier_range_modelWithCornersEuclideanHalfSpace, EuclideanSpace.instIsManifoldSphere, Matrix.isSymmetric_toEuclideanLin_iff, ProbabilityTheory.map_pi_eq_stdGaussian, ProbabilityTheory.integral_id_multivariateGaussian, OrthonormalBasis.equiv_apply, Module.Basis.coe_toOrthonormalBasis_repr_symm, contMDiff_subtype_coe_Icc, OrthonormalBasis.repr_apply_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, EuclideanSpace.edist_single_same, EuclideanHalfSpace.convex, EuclideanSpace.sphere_zero_eq, LinearMap.toMatrix_innerₛₗ_apply, Matrix.inner_toEuclideanCLM, DiffeologicalSpace.plot_reparam, contDiffAt_euclidean, ProbabilityTheory.variance_eval_multivariateGaussian, finrank_euclideanSpace, mfderiv_coe_sphere_injective, contDiffOn_euclidean, InnerProductGeometry.norm_ofLp_crossProduct, Matrix.ofLp_toEuclideanCLM, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, EuclideanQuadrant.convex, range_euclideanHalfSpace, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, IccLeftChart_extend_bot, Matrix.l2_opNNNorm_def, EuclideanSpace.basisFun_repr, OrthonormalBasis.equiv_apply_euclideanSpace, Complex.orthonormalBasisOneI_repr_symm_apply, Manifold.riemannianEDist_def, modelWithCornersEuclideanHalfSpace_zero, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, EuclideanSpace.norm_eq, Matrix.IsHermitian.eigenvectorUnitary_apply, EuclideanSpace.inner_eq_star_dotProduct, OrthonormalBasis.sum_repr_symm, contMDiffWithinAt_comp_projIcc_iff, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, EuclideanSpace.volume_ball_fin_three, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, ProbabilityTheory.covarianceBilin_apply_basisFun, Diffeology.isPlot_iff_contDiff, OrthonormalBasis.measurePreserving_repr_symm, Diffeology.isPlot_iff_dSmooth, oneTangentSpaceIcc_def, EuclideanQuadrant.ext_iff, IccRightChart_extend_top_mem_frontier, hasFDerivWithinAt_euclidean, Matrix.IsHermitian.eigenvectorUnitary_coe, Matrix.toEuclideanLin_eq_toLin, Euclidean.closedBall_eq_preimage, Matrix.isHermitian_iff_isSymmetric, EuclideanSpace.basisFun_inner, InnerProductSpace.toMatrix_rankOne, differentiableAt_euclidean, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, Diffeology.isPlot_reparam, range_euclideanQuadrant, mdifferentiableWithinAt_comp_projIcc_iff, Diffeology.isOpen_iff_preimages_plots, differentiableOn_euclidean, Diffeology.IsContDiffCompatible.isPlot_iff, EuclideanSpace.ball_zero_eq, range_mfderiv_coe_sphere, Diffeology.IsPlot.continuous, Matrix.ofLp_toEuclideanLin_apply, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.inner_basisFun_real, iccLeftChart_extend_zero, Euclidean.ball_eq_preimage, EuclideanSpace.volume_ball, OrthonormalBasis.repr_symm_single, interior_range_modelWithCornersEuclideanHalfSpace, toMatrix_innerSL_apply, Diffeology.IsPlot.contDiff, ProbabilityTheory.measurePreserving_eval_multivariateGaussian, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', Matrix.toEuclideanLin_apply_piLp_toLp, EuclideanSpace.dist_eq, Diffeology.isPlot_id, contMDiffOn_comp_projIcc_iff, volume_euclideanSpace_eq_dirac, OrthonormalBasis.coe_toBasis_repr, OrthonormalBasis.sum_repr, EuclideanSpace.infinite, exists_embedding_euclidean_of_compact, ProbabilityTheory.integral_id_multivariateGaussian', OrthonormalBasis.coe_toBasis_repr_apply, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OrthonormalBasis.coe_equiv_euclideanSpace, EuclideanSpace.dist_sq_eq, Matrix.IsHermitian.eigenvectorUnitary_transpose_apply, stereographic'_symm_apply, EuclideanSpace.coe_measurableEquiv, NumberField.mixedEmbedding.euclidean.finrank, ProbabilityTheory.multivariateGaussian_zero_one, EuclideanSpace.nnnorm_eq, range_modelWithCornersEuclideanHalfSpace, EuclideanSpace.restrict₂_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, EuclideanSpace.inner_single_right, Matrix.toEuclideanLin_eq_toLin_orthonormal, EuclideanSpace.measurableEquiv_toEquiv, EuclideanSpace.euclideanHausdorffMeasure_eq_volume, Matrix.cstar_norm_def, ContMDiff.codRestrict_sphere, Quaternion.linearIsometryEquivTuple_apply, mfderiv_subtype_coe_Icc_one, Diffeology.IsPlot.dSmooth_comp, EuclideanSpace.single_eq_zero_iff, Matrix.IsHermitian.mulVec_eigenvectorBasis, Matrix.l2_opNorm_def, Matrix.toEuclideanLin_toLp, OrthonormalBasis.measurePreserving_measurableEquiv, EuclideanSpace.nndist_single_same, EuclideanSpace.edist_eq, Pi.orthonormalBasis_repr, IccRightChart_extend_top, boundary_Icc, ProbabilityTheory.covariance_eval_multivariateGaussian, DiffeologicalSpace.CorePlotsOn.isPlotOn_univ, EuclideanSpace.volume_closedBall, finrank_euclideanSpace_fin, boundary_product, OrthonormalBasis.repr_reindex, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, EuclideanSpace.coe_measurableEquiv_symm, contDiff_euclidean, IccLeftChart_extend_bot_mem_frontier, OrthonormalBasis.tensorProduct_repr_tmul_apply, Icc_isBoundaryPoint_top, MeasureTheory.Measure.euclideanHausdorffMeasure_def, instIsManifoldIcc, Diffeology.dSmooth_iff, contMDiffOn_projIcc, DiffeologicalSpace.isOpen_iff_preimages_plots, contMDiff_circleExp, hasStrictFDerivAt_euclidean
|