PiLp

📁 Source: Mathlib/Analysis/Normed/Lp/PiLp.lean

Statistics

Metric	Count
Definitions piLpCongrLeft, piLpCongrRight, piLpCurry, PiLp, basisFun, bornology, continuousLinearEquiv, equivₗᵢ, homeomorph, instDist, instEDist, instEMetricSpace, instMetricSpace, instNorm, instPseudoEMetricSpace, instPseudoMetricSpace, normedAddCommGroup, normedAddCommGroupToPi, normedSpace, normedSpaceSeminormedAddCommGroupToPi, proj, projₗ, pseudoEmetricAux, pseudoMetricAux, pseudoMetricSpaceToPi, seminormedAddCommGroup, seminormedAddCommGroupToPi, sumPiLpEquivProdLpPiLp, topologicalSpace, uniformEquiv, uniformSpace, instCoeFunPiLpForall, instInhabitedPiLp	33
Theorems piLpCongrLeft_apply, piLpCongrLeft_single, piLpCongrLeft_symm, piLpCongrRight_apply, piLpCongrRight_refl, piLpCongrRight_single, piLpCongrRight_symm, piLpCurry_apply, piLpCurry_symm_apply, add_apply, antilipschitzWith_ofLp, antilipschitzWith_toLp, basisFun_apply, basisFun_eq_pi_basisFun, basisFun_equivFun, basisFun_map, basisFun_repr, basis_toMatrix_basisFun_mul, coe_continuousLinearEquiv, coe_symm_continuousLinearEquiv, completeSpace, continuousLinearEquiv_apply, continuousLinearEquiv_symm_apply, continuous_apply, continuous_ofLp, continuous_toLp, dist_apply_le, dist_eq_card, dist_eq_iSup, dist_eq_of_L1, dist_eq_of_L2, dist_eq_sum, dist_pseudoMetricSpaceToPi, dist_sq_eq_of_L2, dist_toLp_single_same, edist_apply_le, edist_comm, edist_eq_card, edist_eq_iSup, edist_eq_of_L1, edist_eq_of_L2, edist_eq_sum, edist_self, edist_toLp_single_same, enorm_apply_le, ext, ext_iff, iSup_edist_ne_top_aux, instIsBoundedSMul, instNormSMulClass, instProdT0Space, isBoundedSMulSeminormedAddCommGroupToPi, isOpenMap_apply, isUniformInducing_toLp, isometry_ofLp_infty, lipschitzWith_ofLp, lipschitzWith_toLp, neg_apply, nndist_apply_le, nndist_eq_iSup, nndist_eq_of_L1, nndist_eq_of_L2, nndist_eq_sum, nndist_toLp_single_same, nnnorm_apply_le, nnnorm_eq_ciSup, nnnorm_eq_of_L1, nnnorm_eq_of_L2, nnnorm_eq_sum, nnnorm_ofLp, nnnorm_seminormedAddCommGroupToPi, nnnorm_toLp, nnnorm_toLp_const, nnnorm_toLp_const', nnnorm_toLp_one, nnnorm_toLp_single, normSMulClassSeminormedAddCommGroupToPi, norm_apply_le, norm_eq_card, norm_eq_ciSup, norm_eq_of_L1, norm_eq_of_L2, norm_eq_of_nat, norm_eq_sum, norm_ofLp, norm_seminormedAddCommGroupToPi, norm_sq_eq_of_L2, norm_toLp, norm_toLp_const, norm_toLp_const', norm_toLp_one, norm_toLp_single, proj_apply, projₗ_apply, secondCountableTopology, smul_apply, sub_apply, sumPiLpEquivProdLpPiLp_apply_ofLp, sumPiLpEquivProdLpPiLp_symm_apply_ofLp, toEquiv_homeomorph, toEquiv_uniformEquiv, toHomeomorph_uniformEquiv, toLp_apply, uniformContinuous_ofLp, uniformContinuous_toLp, zero_apply	106
Total	139

LinearIsometryEquiv

Definitions

Name	Category	Theorems
piLpCongrLeft 📖	CompOp	4 math math: piLpCongrLeft_apply, EuclideanSpace.piLpCongrLeft_single, piLpCongrLeft_single, piLpCongrLeft_symm
piLpCongrRight 📖	CompOp	4 math math: piLpCongrRight_symm, piLpCongrRight_apply, piLpCongrRight_single, piLpCongrRight_refl
piLpCurry 📖	CompOp	2 math math: piLpCurry_apply, piLpCurry_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piLpCongrLeft_apply 📖	mathematical	—	WithLp.ofLp DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike piLpCongrLeft Equiv Equiv.instEquivLike Equiv.piCongrLeft'	—	RingHomInvPair.ids
piLpCongrLeft_single 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike piLpCongrLeft WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Equiv Equiv.instEquivLike	—	PiLp.ext RingHomInvPair.ids Equiv.symm_apply_apply
piLpCongrLeft_symm 📖	mathematical	—	symm PiLp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.Function.module AddCommGroup.toAddCommMonoid piLpCongrLeft Equiv.symm	—	ext RingHomInvPair.ids PiLp.ext Equiv.piCongrLeft'_symm
piLpCongrRight_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike piLpCongrRight WithLp.toLp WithLp.ofLp	—	RingHomInvPair.ids
piLpCongrRight_refl 📖	mathematical	—	piLpCongrRight refl PiLp PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid	—	RingHomInvPair.ids
piLpCongrRight_single 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid EquivLike.toFunLike instEquivLike piLpCongrRight WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	RingHomInvPair.ids PiLp.ext Pi.apply_single map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass instSemilinearIsometryEquivClass
piLpCongrRight_symm 📖	mathematical	—	symm PiLp RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp.seminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid piLpCongrRight	—	RingHomInvPair.ids
piLpCurry_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp PiLp.seminormedAddCommGroup Sigma.instFintype WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup EquivLike.toFunLike instEquivLike piLpCurry WithLp.toLp Sigma.curry WithLp.ofLp	—	RingHomInvPair.ids
piLpCurry_symm_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp PiLp.seminormedAddCommGroup Sigma.instFintype WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup EquivLike.toFunLike instEquivLike symm piLpCurry WithLp.toLp Sigma.uncurry WithLp.ofLp	—	RingHomInvPair.ids

PiLp

Definitions

Name	Category	Theorems
basisFun 📖	CompOp	9 math math: basisFun_equivFun, EuclideanSpace.basisFun_toBasis, basisFun_repr, basisFun_apply, Matrix.toEuclideanLin_eq_toLin, basisFun_eq_pi_basisFun, basis_toMatrix_basisFun_mul, basisFun_map, Matrix.toLpLin_eq_toLin
bornology 📖	CompOp	—
continuousLinearEquiv 📖	CompOp	11 math math: continuousLinearEquiv_symm_apply, coe_continuousLinearEquiv, MeasureTheory.charFunDual_pi', hasFDerivAt_toLp, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', hasFDerivAt_ofLp, MeasureTheory.charFunDual_eq_pi_iff', coe_symm_continuousLinearEquiv, hasStrictFDerivAt_ofLp, continuousLinearEquiv_apply, hasStrictFDerivAt_toLp
equivₗᵢ 📖	CompOp	—
homeomorph 📖	CompOp	2 math math: toEquiv_homeomorph, toHomeomorph_uniformEquiv
instDist 📖	CompOp	12 math math: dist_eq_card, EuclideanSpace.dist_single_same, dist_eq_of_L1, dist_pseudoMetricSpaceToPi, dist_eq_iSup, dist_apply_le, dist_toLp_single_same, dist_sq_eq_of_L2, EuclideanSpace.dist_eq, dist_eq_of_L2, EuclideanSpace.dist_sq_eq, dist_eq_sum
instEDist 📖	CompOp	11 math math: edist_self, edist_eq_sum, EuclideanSpace.edist_single_same, edist_eq_iSup, edist_apply_le, edist_eq_card, edist_toLp_single_same, EuclideanSpace.edist_eq, edist_eq_of_L1, edist_comm, edist_eq_of_L2
instEMetricSpace 📖	CompOp	2 math math: Matrix.l2_opNNNorm_def, Matrix.l2_opNorm_def
instMetricSpace 📖	CompOp	—
instNorm 📖	CompOp	30 math math: Matrix.frobenius_norm_replicateCol, norm_toLp_const', Matrix.l2_opNorm_mulVec, norm_toLp_one, norm_ofLp, EuclideanSpace.norm_sq_eq, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, norm_toLp_single, EuclideanSpace.norm_single, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, InnerProductGeometry.norm_toLp_symm_crossProduct, instNormSMulClass, Behrend.norm_of_mem_sphere, norm_eq_sum, InnerProductGeometry.norm_ofLp_crossProduct, norm_sq_eq_of_L2, norm_eq_of_L1, norm_eq_ciSup, EuclideanSpace.norm_eq, norm_seminormedAddCommGroupToPi, norm_eq_of_nat, norm_toLp_const, norm_apply_le, Matrix.frobenius_norm_diagonal, equiv_lpPiLp_norm, norm_toLp, norm_eq_of_L2, Matrix.frobenius_norm_replicateRow, Quaternion.norm_toLp_equivTuple, norm_eq_card
instPseudoEMetricSpace 📖	CompOp	5 math math: lipschitzWith_toLp, antilipschitzWith_toLp, lipschitzWith_ofLp, antilipschitzWith_ofLp, isometry_ofLp_infty
instPseudoMetricSpace 📖	CompOp	31 math math: Matrix.l2_opNorm_toEuclideanCLM, nndist_eq_sum, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, EuclideanSpace.closedBall_zero_eq, Matrix.cstar_nnnorm_def, Behrend.sphere_subset_preimage_metric_sphere, EuclideanSpace.nndist_eq, Euclidean.closedBall_eq_image, EuclideanSpace.volume_closedBall_fin_three, nndist_toLp_single_same, nndist_apply_le, Matrix.toEuclideanCLM_toLp, EuclideanSpace.volume_closedBall_fin_two, EuclideanSpace.sphere_zero_eq, Matrix.ofLp_toEuclideanCLM, Matrix.l2_opNNNorm_def, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, EuclideanSpace.volume_ball_fin_three, Euclidean.closedBall_eq_preimage, EuclideanSpace.ball_zero_eq, EuclideanSpace.volume_ball_fin_two, Euclidean.ball_eq_preimage, EuclideanSpace.volume_ball, Matrix.cstar_norm_def, Matrix.l2_opNorm_def, EuclideanSpace.nndist_single_same, instIsBoundedSMul, EuclideanSpace.volume_closedBall, nndist_eq_of_L2, nndist_eq_iSup, nndist_eq_of_L1
normedAddCommGroup 📖	CompOp	141 math math: Matrix.l2_opNorm_toEuclideanCLM, Pi.comul_eq_adjoint, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, contDiff_toLp, contDiffOn_piLp', Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, contDiff_piLp', EuclideanSpace.basisFun_toBasis, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, contMDiff_neg_sphere, SmoothBumpCovering.exists_immersion_euclidean, EuclideanSpace.basisFun_apply, ProbabilityTheory.HasGaussianLaw.toLp_pi, Matrix.IsHermitian.eigenvalues_eq, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, Icc_isBoundaryPoint_bot, OrthonormalBasis.measurePreserving_repr, Matrix.IsHermitian.eigenvectorUnitary_col_eq, Matrix.toEuclideanLin_apply, mfderivWithin_projIcc_one, Euclidean.closedBall_eq_image, MeasureTheory.charFunDual_pi', Pi.counit_eq_adjoint, ProbabilityTheory.covarianceBilin_apply_basisFun_self, Icc_isInteriorPoint_interior, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, EuclideanSpace.instFactEqNatFinrankFin, mfderivWithin_comp_projIcc_one, contDiffWithinAt_euclidean, contDiffAt_piLp_apply, EuclideanSpace.volume_closedBall_fin_three, IccLeftChart_extend_interior_pos, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Matrix.IsHermitian.eigenvectorUnitary_mulVec, contMDiff_coe_sphere, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, volume_preserving_toLp, InnerProductGeometry.norm_toLp_symm_crossProduct, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, Matrix.toEuclideanCLM_toLp, EuclideanSpace.volume_closedBall_fin_two, Pi.orthonormalBasis_apply, Matrix.piLp_ofLp_toEuclideanLin, frontier_range_modelWithCornersEuclideanHalfSpace, EuclideanSpace.instIsManifoldSphere, contMDiff_subtype_coe_Icc, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, EuclideanHalfSpace.convex, contDiffAt_piLp', contDiffAt_euclidean, finrank_euclideanSpace, mfderiv_coe_sphere_injective, contDiffOn_euclidean, volume_preserving_ofLp, InnerProductGeometry.norm_ofLp_crossProduct, Matrix.ofLp_toEuclideanCLM, Matrix.isPositive_toEuclideanLin_iff, EuclideanQuadrant.convex, contDiff_piLp, IccLeftChart_extend_bot, Matrix.l2_opNNNorm_def, EuclideanSpace.basisFun_repr, OrthonormalBasis.equiv_apply_euclideanSpace, Manifold.riemannianEDist_def, modelWithCornersEuclideanHalfSpace_zero, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, Matrix.IsHermitian.eigenvectorUnitary_apply, contDiffOn_piLp, ProbabilityTheory.covarianceBilin_apply_pi, Pi.orthonormalBasis.toBasis, 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, analyticOn_ofLp, oneTangentSpaceIcc_def, IccRightChart_extend_top_mem_frontier, Matrix.IsHermitian.eigenvectorUnitary_coe, Matrix.toEuclideanLin_eq_toLin, analyticOn_toLp, Euclidean.closedBall_eq_preimage, Matrix.isHermitian_iff_isSymmetric, EuclideanSpace.basisFun_inner, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, mdifferentiableWithinAt_comp_projIcc_iff, Diffeology.IsContDiffCompatible.isPlot_iff, range_mfderiv_coe_sphere, contDiffOn_piLp_apply, Matrix.ofLp_toEuclideanLin_apply, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.inner_basisFun_real, iccLeftChart_extend_zero, Euclidean.ball_eq_preimage, EuclideanSpace.volume_ball, interior_range_modelWithCornersEuclideanHalfSpace, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', Diffeology.IsPlot.contDiff, contDiff_ofLp, contDiff_piLp_apply, contDiffWithinAt_piLp, MeasureTheory.charFunDual_eq_pi_iff', Matrix.toEuclideanLin_apply_piLp_toLp, contMDiffOn_comp_projIcc_iff, volume_euclideanSpace_eq_dirac, exists_embedding_euclidean_of_compact, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OrthonormalBasis.coe_equiv_euclideanSpace, Matrix.IsHermitian.eigenvectorUnitary_transpose_apply, range_modelWithCornersEuclideanHalfSpace, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, Matrix.toEuclideanLin_eq_toLin_orthonormal, contDiffAt_piLp, Matrix.cstar_norm_def, ContMDiff.codRestrict_sphere, mfderiv_subtype_coe_Icc_one, MeasureTheory.eval_integral_piLp, Matrix.IsHermitian.mulVec_eigenvectorBasis, Matrix.l2_opNorm_def, Matrix.toEuclideanLin_toLp, OrthonormalBasis.measurePreserving_measurableEquiv, Pi.orthonormalBasis_repr, contDiffWithinAt_piLp', IccRightChart_extend_top, boundary_Icc, contDiffWithinAt_piLp_apply, EuclideanSpace.volume_closedBall, finrank_euclideanSpace_fin, boundary_product, Matrix.IsHermitian.star_eigenvectorUnitary_mulVec, InnerProductSpace.symm_toEuclideanLin_rankOne, contDiff_euclidean, IccLeftChart_extend_bot_mem_frontier, Icc_isBoundaryPoint_top, instIsManifoldIcc, contMDiffOn_projIcc, contMDiff_circleExp
normedAddCommGroupToPi 📖	CompOp	—
normedSpace 📖	CompOp	74 math math: Matrix.l2_opNorm_toEuclideanCLM, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, contDiff_toLp, contDiffOn_piLp', Matrix.cstar_nnnorm_def, contDiff_piLp', contMDiff_neg_sphere, SmoothBumpCovering.exists_immersion_euclidean, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, Icc_isBoundaryPoint_bot, mfderivWithin_projIcc_one, MeasureTheory.charFunDual_pi', Icc_isInteriorPoint_interior, mfderivWithin_comp_projIcc_one, contDiffWithinAt_euclidean, contDiffAt_piLp_apply, IccLeftChart_extend_interior_pos, contMDiff_coe_sphere, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, frontier_range_modelWithCornersEuclideanHalfSpace, EuclideanSpace.instIsManifoldSphere, contMDiff_subtype_coe_Icc, contDiffAt_piLp', contDiffAt_euclidean, mfderiv_coe_sphere_injective, contDiffOn_euclidean, contDiff_piLp, IccLeftChart_extend_bot, Matrix.l2_opNNNorm_def, Manifold.riemannianEDist_def, modelWithCornersEuclideanHalfSpace_zero, contDiffOn_piLp, contMDiffWithinAt_comp_projIcc_iff, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, Diffeology.isPlot_iff_contDiff, analyticOn_ofLp, oneTangentSpaceIcc_def, IccRightChart_extend_top_mem_frontier, analyticOn_toLp, mdifferentiableWithinAt_comp_projIcc_iff, Diffeology.IsContDiffCompatible.isPlot_iff, range_mfderiv_coe_sphere, contDiffOn_piLp_apply, iccLeftChart_extend_zero, interior_range_modelWithCornersEuclideanHalfSpace, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', Diffeology.IsPlot.contDiff, contDiff_ofLp, contDiff_piLp_apply, contDiffWithinAt_piLp, MeasureTheory.charFunDual_eq_pi_iff', contMDiffOn_comp_projIcc_iff, exists_embedding_euclidean_of_compact, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, range_modelWithCornersEuclideanHalfSpace, contDiffAt_piLp, Matrix.cstar_norm_def, ContMDiff.codRestrict_sphere, mfderiv_subtype_coe_Icc_one, MeasureTheory.eval_integral_piLp, Matrix.l2_opNorm_def, contDiffWithinAt_piLp', IccRightChart_extend_top, boundary_Icc, contDiffWithinAt_piLp_apply, boundary_product, InnerProductSpace.symm_toEuclideanLin_rankOne, contDiff_euclidean, IccLeftChart_extend_bot_mem_frontier, Icc_isBoundaryPoint_top, instIsManifoldIcc, contMDiffOn_projIcc, contMDiff_circleExp
normedSpaceSeminormedAddCommGroupToPi 📖	CompOp	—
proj 📖	CompOp	7 math math: hasStrictFDerivAt_piLp, hasFDerivWithinAt_piLp, hasFDerivWithinAt_euclidean, hasStrictFDerivAt_apply, hasFDerivAt_apply, proj_apply, hasStrictFDerivAt_euclidean
projₗ 📖	CompOp	1 math math: projₗ_apply
pseudoEmetricAux 📖	CompOp	—
pseudoMetricAux 📖	CompOp	—
pseudoMetricSpaceToPi 📖	CompOp	2 math math: isBoundedSMulSeminormedAddCommGroupToPi, dist_pseudoMetricSpaceToPi
seminormedAddCommGroup 📖	CompOp	98 math math: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, LinearIsometryEquiv.piLpCongrRight_symm, EuclideanSpace.orthonormal_single, OrthonormalBasis.repr_injective, Matrix.cstar_nnnorm_def, LinearMap.IsSymmetric.diagonalization_apply_self_apply, EuclideanSpace.inner_single_left, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, OrthonormalBasis.repr_self, LinearIsometryEquiv.piLpCongrRight_apply, OrthonormalBasis.measurePreserving_repr, nnnorm_eq_of_L2, MeasureTheory.integrable_piLp_iff, Quaternion.linearIsometryEquivTuple_symm_apply, LDL.lowerInv_orthogonal, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, nnnorm_toLp_one, sumPiLpEquivProdLpPiLp_symm_apply_ofLp, Module.Basis.coe_toOrthonormalBasis_repr, LinearIsometryEquiv.piLpCongrLeft_apply, OrthonormalBasis.coe_ofRepr, EuclideanSpace.nnnorm_single, Complex.orthonormalBasisOneI_repr_apply, nnnorm_toLp_single, Matrix.toEuclideanCLM_toLp, nnnorm_toLp_const', LinearMap.IsSymmetric.diagonalization_symm_apply, OrthonormalBasis.tensorProduct_repr_tmul_apply', enorm_apply_le, Matrix.l2_opNNNorm_mulVec, nnnorm_apply_le, OrthonormalBasis.equiv_apply, Module.Basis.coe_toOrthonormalBasis_repr_symm, MeasureTheory.charFun_pi, OrthonormalBasis.repr_apply_apply, LinearIsometryEquiv.piLpCurry_apply, LinearMap.toMatrix_innerₛₗ_apply, RCLike.wInner_one_eq_inner, LinearIsometryEquiv.piLpCongrRight_single, Matrix.ofLp_toEuclideanCLM, nnnorm_eq_ciSup, LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, Matrix.l2_opNNNorm_def, EuclideanSpace.basisFun_repr, Complex.orthonormalBasisOneI_repr_symm_apply, LinearIsometryEquiv.piLpCongrRight_refl, coe_lpPiLpₗᵢ, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, Matrix.frobenius_nnnorm_replicateRow, EuclideanSpace.inner_eq_star_dotProduct, OrthonormalBasis.sum_repr_symm, Matrix.frobenius_nnnorm_replicateCol, nnnorm_toLp, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, Matrix.frobenius_nnnorm_diagonal, MeasureTheory.memLp_piLp_iff, OrthonormalBasis.measurePreserving_repr_symm, EuclideanSpace.piLpCongrLeft_single, LinearIsometryEquiv.piLpCurry_symm_apply, Matrix.isHermitian_iff_isSymmetric, EuclideanSpace.basisFun_inner, InnerProductSpace.toMatrix_rankOne, coe_lpPiLpₗᵢ_symm, EuclideanSpace.inner_basisFun_real, MeasureTheory.Integrable.of_eval_piLp, OrthonormalBasis.repr_symm_single, toMatrix_innerSL_apply, nnnorm_eq_of_L1, ProbabilityTheory.iIndepFun_iff_charFun_pi, InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular', MeasureTheory.MemLp.of_eval_piLp, OrthonormalBasis.coe_toBasis_repr, OrthonormalBasis.sum_repr, LinearIsometryEquiv.piLpCongrLeft_single, OrthonormalBasis.coe_toBasis_repr_apply, EuclideanSpace.inner_toLp_toLp, nnnorm_eq_sum, EuclideanSpace.nnnorm_eq, inner_apply, EuclideanSpace.inner_single_right, Matrix.cstar_norm_def, inner_matrix_row_row, Quaternion.linearIsometryEquivTuple_apply, nnnorm_seminormedAddCommGroupToPi, nnnorm_toLp_const, Matrix.l2_opNorm_def, LinearIsometryEquiv.piLpCongrLeft_symm, Pi.orthonormalBasis_repr, MeasureTheory.charFun_eq_pi_iff, OrthonormalBasis.repr_reindex, InnerProductSpace.symm_toEuclideanLin_rankOne, OrthonormalBasis.tensorProduct_repr_tmul_apply, RCLike.inner_eq_wInner_one, nnnorm_ofLp, sumPiLpEquivProdLpPiLp_apply_ofLp, inner_matrix_col_col
seminormedAddCommGroupToPi 📖	CompOp	3 math math: norm_seminormedAddCommGroupToPi, normSMulClassSeminormedAddCommGroupToPi, nnnorm_seminormedAddCommGroupToPi
sumPiLpEquivProdLpPiLp 📖	CompOp	2 math math: sumPiLpEquivProdLpPiLp_symm_apply_ofLp, sumPiLpEquivProdLpPiLp_apply_ofLp
topologicalSpace 📖	CompOp	94 math math: Matrix.l2_opNorm_toEuclideanCLM, Pi.comul_eq_adjoint, continuousLinearEquiv_symm_apply, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, Matrix.spectrum_toEuclideanLin, Matrix.cstar_nnnorm_def, Matrix.l2_opNorm_mulVec, frontier_halfSpace, DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots, SmoothBumpCovering.exists_immersion_euclidean, ProbabilityTheory.HasGaussianLaw.toLp_pi, stereographic'_source, MeasureTheory.integrable_piLp_iff, instProdT0Space, coe_continuousLinearEquiv, Matrix.toEuclideanLin_apply, Euclidean.closedBall_eq_image, MeasureTheory.charFunDual_pi', Pi.counit_eq_adjoint, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, continuous_toLp, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Matrix.toEuclideanCLM_toLp, hasFDerivAt_toLp, Matrix.piLp_ofLp_toEuclideanLin, stereographic'_target, Matrix.l2_opNNNorm_mulVec, frontier_range_modelWithCornersEuclideanHalfSpace, interior_halfSpace, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, EuclideanHalfSpace.convex, hasStrictFDerivAt_piLp, finrank_euclideanSpace, hasFDerivWithinAt_piLp, differentiableOn_piLp, closure_open_halfSpace, Matrix.ofLp_toEuclideanCLM, differentiableWithinAt_euclidean, Matrix.isPositive_toEuclideanLin_iff, isOpenMap_apply, EuclideanQuadrant.convex, differentiableAt_piLp, Matrix.l2_opNNNorm_def, borelSpace, continuous_apply, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice, MeasureTheory.memLp_piLp_iff, toEquiv_homeomorph, IccRightChart_extend_top_mem_frontier, hasFDerivWithinAt_euclidean, secondCountableTopology, hasStrictFDerivAt_apply, Matrix.toEuclideanLin_eq_toLin, Euclidean.closedBall_eq_preimage, Matrix.isHermitian_iff_isSymmetric, differentiableAt_euclidean, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, continuous_ofLp, Diffeology.isOpen_iff_preimages_plots, differentiableOn_euclidean, Diffeology.IsPlot.continuous, differentiable_piLp, Matrix.ofLp_toEuclideanLin_apply, MeasureTheory.Integrable.of_eval_piLp, Euclidean.ball_eq_preimage, interior_range_modelWithCornersEuclideanHalfSpace, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', hasFDerivAt_ofLp, MeasureTheory.charFunDual_eq_pi_iff', MeasureTheory.MemLp.of_eval_piLp, Matrix.toEuclideanLin_apply_piLp_toLp, hasFDerivAt_apply, proj_apply, exists_embedding_euclidean_of_compact, coe_symm_continuousLinearEquiv, stereographic'_symm_apply, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, differentiableWithinAt_piLp, hasStrictFDerivAt_ofLp, Matrix.cstar_norm_def, continuousLinearEquiv_apply, Matrix.l2_opNorm_def, Matrix.toEuclideanLin_toLp, closure_halfSpace, DiffeologicalSpace.CorePlotsOn.isPlotOn_univ, finrank_euclideanSpace_fin, InnerProductSpace.symm_toEuclideanLin_rankOne, interior_euclideanQuadrant, IccLeftChart_extend_bot_mem_frontier, DiffeologicalSpace.isOpen_iff_preimages_plots, hasStrictFDerivAt_toLp, hasStrictFDerivAt_euclidean
uniformEquiv 📖	CompOp	2 math math: toEquiv_uniformEquiv, toHomeomorph_uniformEquiv
uniformSpace 📖	CompOp	12 math math: Matrix.l2_opNorm_toEuclideanCLM, Matrix.cstar_nnnorm_def, completeSpace, toEquiv_uniformEquiv, Matrix.toEuclideanCLM_toLp, Matrix.ofLp_toEuclideanCLM, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, toHomeomorph_uniformEquiv, isUniformInducing_toLp, uniformContinuous_ofLp, uniformContinuous_toLp, Matrix.cstar_norm_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	WithLp.ofLp PiLp AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup	—	—
antilipschitzWith_ofLp 📖	mathematical	—	AntilipschitzWith WithLp instPseudoEMetricSpace pseudoEMetricSpacePi NNReal Real NNReal.instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal WithLp.ofLp	—	—
antilipschitzWith_toLp 📖	mathematical	—	AntilipschitzWith WithLp pseudoEMetricSpacePi instPseudoEMetricSpace NNReal instOneNNReal WithLp.toLp	—	LipschitzWith.to_rightInverse lipschitzWith_ofLp WithLp.ofLp_toLp
basisFun_apply 📖	mathematical	—	DFunLike.coe Module.Basis PiLp Ring.toSemiring AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Ring.toAddCommGroup WithLp.instModule Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Module.Basis.instFunLike basisFun WithLp.toLp Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	RingHomInvPair.ids Module.Basis.coe_ofEquivFun
basisFun_eq_pi_basisFun 📖	mathematical	—	basisFun Module.Basis.map WithLp Ring.toSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Ring.toAddCommGroup WithLp.instModule NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Pi.basisFun LinearEquiv.symm RingHom.id RingHomInvPair.ids WithLp.linearEquiv	—	—
basisFun_equivFun 📖	mathematical	—	Module.Basis.equivFun PiLp Ring.toSemiring AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Ring.toAddCommGroup WithLp.instModule Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule basisFun WithLp.linearEquiv	—	Module.Basis.equivFun_ofEquivFun
basisFun_map 📖	mathematical	—	Module.Basis.map PiLp Ring.toSemiring AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Ring.toAddCommGroup WithLp.instModule Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule basisFun WithLp.linearEquiv Pi.basisFun	—	—
basisFun_repr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids PiLp AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Ring.toAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid WithLp.instModule Pi.Function.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basisFun WithLp.ofLp	—	RingHomInvPair.ids
basis_toMatrix_basisFun_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalSeminormedCommRing.toNonUnitalCommRing SeminormedCommRing.toNonUnitalSeminormedCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Module.Basis.toMatrix PiLp CommRing.toCommSemiring SeminormedCommRing.toCommRing AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing WithLp.instModule CommSemiring.toSemiring Pi.Function.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing Semiring.toModule DFunLike.coe Module.Basis Ring.toAddCommGroup Module.Basis.instFunLike basisFun Finite.of_fintype Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.of Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr WithLp.toLp Matrix.transpose	—	Finite.of_fintype RingHomInvPair.ids basis_toMatrix_basisFun_mul LinearEquiv.symm_apply_apply Module.Basis.toMatrix_map
coe_continuousLinearEquiv 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.topologicalSpace Pi.addCommMonoid WithLp.instModule Pi.module EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquiv WithLp.ofLp	—	RingHomInvPair.ids
coe_symm_continuousLinearEquiv 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup PiLp topologicalSpace WithLp.instAddCommGroup Pi.addCommGroup Pi.module WithLp.instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquiv WithLp.toLp	—	RingHomInvPair.ids
completeSpace 📖	mathematical	CompleteSpace	PiLp uniformSpace	—	UniformEquiv.completeSpace_iff Pi.complete
continuousLinearEquiv_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids PiLp topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.topologicalSpace Pi.addCommMonoid WithLp.instModule Pi.module EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquiv WithLp.ofLp	—	RingHomInvPair.ids
continuousLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Pi.addCommMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup PiLp topologicalSpace WithLp.instAddCommGroup Pi.addCommGroup Pi.module WithLp.instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquiv WithLp.toLp	—	RingHomInvPair.ids
continuous_apply 📖	mathematical	—	Continuous PiLp topologicalSpace WithLp.ofLp	—	Continuous.comp continuous_apply continuous_ofLp
continuous_ofLp 📖	mathematical	—	Continuous WithLp topologicalSpace Pi.topologicalSpace WithLp.ofLp	—	continuous_induced_dom
continuous_toLp 📖	mathematical	—	Continuous WithLp Pi.topologicalSpace topologicalSpace WithLp.toLp	—	continuous_induced_rng continuous_id
dist_apply_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist WithLp.ofLp PiLp instDist	—	nndist_apply_le
dist_eq_card 📖	mathematical	—	Dist.dist PiLp ENNReal instZeroENNReal instDist Real Real.instNatCast Finset.card Set.Finite.toFinset setOf WithLp.ofLp Real.instZero Set.toFinite Subtype.finite Finite.of_fintype Set Set.instMembership	—	—
dist_eq_iSup 📖	mathematical	—	Dist.dist PiLp Top.top ENNReal instTopENNReal instDist iSup Real Real.instSupSet WithLp.ofLp	—	—
dist_eq_of_L1 📖	mathematical	—	Dist.dist PiLp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal instDist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace Finset.sum Real Real.instAddCommMonoid Finset.univ WithLp.ofLp	—	fact_one_le_one_ennreal dist_eq_norm Finset.sum_congr norm_eq_of_L1
dist_eq_of_L2 📖	mathematical	—	Dist.dist PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instDist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace Real.sqrt Finset.sum Real Real.instAddCommMonoid Finset.univ Monoid.toNatPow Real.instMonoid WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal dist_eq_norm Finset.sum_congr norm_eq_of_L2
dist_eq_sum 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Dist.dist PiLp instDist Real.instPow Finset.sum Real.instAddCommMonoid Finset.univ WithLp.ofLp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	ENNReal.toReal_pos_iff LT.lt.ne' LT.lt.ne
dist_pseudoMetricSpaceToPi 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist pseudoMetricSpaceToPi WithLp instDist WithLp.toLp	—	—
dist_sq_eq_of_L2 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Dist.dist PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instDist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace Finset.sum Real.instAddCommMonoid Finset.univ WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal dist_eq_norm Finset.sum_congr norm_sq_eq_of_L2
dist_toLp_single_same 📖	mathematical	—	Dist.dist WithLp instDist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	nndist_toLp_single_same
edist_apply_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist PseudoEMetricSpace.toEDist WithLp.ofLp PiLp instEDist	—	—
edist_comm 📖	mathematical	—	EDist.edist PiLp instEDist PseudoEMetricSpace.toEDist	—	ENNReal.trichotomy Set.toFinite Subtype.finite Finite.of_fintype PseudoEMetricSpace.edist_comm edist_eq_card Set.Finite.toFinset.congr_simp edist_eq_sum Finset.sum_congr
edist_eq_card 📖	mathematical	—	EDist.edist PiLp ENNReal instZeroENNReal instEDist AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Finset.card Set.Finite.toFinset setOf WithLp.ofLp Set.toFinite Subtype.finite Finite.of_fintype Set Set.instMembership	—	—
edist_eq_iSup 📖	mathematical	—	EDist.edist PiLp Top.top ENNReal instTopENNReal instEDist iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder WithLp.ofLp	—	—
edist_eq_of_L1 📖	mathematical	—	EDist.edist PiLp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal instEDist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Finset.sum ENNReal.instAddCommMonoid Finset.univ WithLp.ofLp	—	edist_eq_sum Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Finset.sum_congr ENNReal.rpow_one div_self
edist_eq_of_L2 📖	mathematical	—	EDist.edist PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instEDist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Real ENNReal.instPowReal Finset.sum ENNReal.instAddCommMonoid Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring WithLp.ofLp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat edist_eq_sum ENNReal.toReal_ofNat Real.instIsOrderedRing Real.instNontrivial Finset.sum_congr ENNReal.rpow_ofNat one_div
edist_eq_sum 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	EDist.edist PiLp instEDist ENNReal ENNReal.instPowReal Finset.sum ENNReal.instAddCommMonoid Finset.univ WithLp.ofLp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	ENNReal.toReal_pos_iff LT.lt.ne' LT.lt.ne
edist_self 📖	mathematical	—	EDist.edist PiLp instEDist PseudoEMetricSpace.toEDist ENNReal instZeroENNReal	—	ENNReal.trichotomy Set.toFinite Subtype.finite Finite.of_fintype edist_eq_card PseudoEMetricSpace.edist_self Set.Finite.toFinset.congr_simp Set.toFinite_toFinset Set.toFinset_empty CharP.cast_eq_zero CharP.ofCharZero ENNReal.instCharZero ENNReal.iSup_zero edist_eq_sum Finset.sum_congr ENNReal.zero_rpow_of_pos Finset.sum_const_zero one_div inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
edist_toLp_single_same 📖	mathematical	—	EDist.edist WithLp instEDist PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	edist_nndist nndist_toLp_single_same
enorm_apply_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup SeminormedAddGroup.toContinuousENorm WithLp.ofLp PiLp seminormedAddCommGroup	—	edist_zero_right edist_apply_le
ext 📖	—	WithLp.ofLp	—	—	WithLp.ofLp_injective
ext_iff 📖	mathematical	—	WithLp.ofLp	—	ext
iSup_edist_ne_top_aux 📖	—	—	—	—	nonempty_fintype dist_nonneg Finite.exists_le instIsDirectedOrder Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsOrderedRing.toPosMulMono Real.instIsOrderedRing Nonneg.isOrderedRing Nonneg.instArchimedean Real.instArchimedean ne_of_lt LE.le.trans_lt iSup_le PseudoMetricSpace.edist_dist ENNReal.ofReal_eq_coe_nnreal ENNReal.coe_lt_top
instIsBoundedSMul 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	PiLp instPseudoMetricSpace WithLp.instAddCommGroup Pi.addCommGroup WithLp.instSMul Pi.instSMul	—	IsBoundedSMul.of_nnnorm_smul_le ENNReal.dichotomy fact_one_le_top_ennreal nnnorm_ofLp WithLp.ofLp_smul nnnorm_smul_le Pi.instIsBoundedSMul LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ENNReal.toReal_pos_iff_ne_top nnnorm_eq_sum one_div NNReal.rpow_inv_le_iff NNReal.mul_rpow NNReal.rpow_mul inv_mul_cancel₀ LT.lt.ne' NNReal.rpow_one Finset.mul_sum Finset.sum_congr Finset.sum_le_sum NNReal.addLeftMono NNReal.rpow_le_rpow le_of_lt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one
instNormSMulClass 📖	mathematical	NormSMulClass SeminormedRing.toNorm SeminormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	PiLp instNorm WithLp.instSMul Pi.instSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	NormSMulClass.of_nnnorm_smul ENNReal.dichotomy fact_one_le_top_ennreal nnnorm_ofLp WithLp.ofLp_smul nnnorm_smul Pi.instNormSMulClass LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ENNReal.toReal_pos_iff_ne_top nnnorm_eq_sum one_div NNReal.rpow_inv_eq_iff LT.lt.ne' NNReal.mul_rpow NNReal.rpow_mul inv_mul_cancel₀ NNReal.rpow_one Finset.mul_sum Finset.sum_congr
instProdT0Space 📖	mathematical	T0Space	PiLp topologicalSpace	—	Homeomorph.t0Space Pi.instT0Space
isBoundedSMulSeminormedAddCommGroupToPi 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SeminormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	pseudoMetricSpaceToPi Pi.instZero Pi.instSMul	—	dist_zero_right dist_smul_pair instIsBoundedSMul dist_pair_smul
isOpenMap_apply 📖	mathematical	—	IsOpenMap PiLp topologicalSpace WithLp.ofLp	—	IsOpenMap.comp isOpenMap_eval Homeomorph.isOpenMap
isUniformInducing_toLp 📖	mathematical	—	IsUniformInducing WithLp Pi.uniformSpace PseudoEMetricSpace.toUniformSpace uniformSpace WithLp.toLp	—	AntilipschitzWith.isUniformInducing antilipschitzWith_toLp LipschitzWith.uniformContinuous lipschitzWith_toLp
isometry_ofLp_infty 📖	mathematical	—	Isometry WithLp Top.top ENNReal instTopENNReal instPseudoEMetricSpace fact_one_le_top_ennreal pseudoEMetricSpacePi WithLp.ofLp	—	le_antisymm fact_one_le_top_ennreal one_mul lipschitzWith_ofLp ENNReal.div_top NNReal.rpow_zero antilipschitzWith_ofLp
lipschitzWith_ofLp 📖	mathematical	—	LipschitzWith WithLp instPseudoEMetricSpace pseudoEMetricSpacePi NNReal instOneNNReal WithLp.ofLp	—	—
lipschitzWith_toLp 📖	mathematical	—	LipschitzWith WithLp pseudoEMetricSpacePi instPseudoEMetricSpace NNReal Real NNReal.instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal WithLp.toLp	—	AntilipschitzWith.to_rightInverse antilipschitzWith_ofLp WithLp.ofLp_toLp
neg_apply 📖	mathematical	—	WithLp.ofLp PiLp NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup	—	—
nndist_apply_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNDist.nndist PseudoMetricSpace.toNNDist WithLp.ofLp PiLp instPseudoMetricSpace	—	edist_apply_le
nndist_eq_iSup 📖	mathematical	—	NNDist.nndist PiLp Top.top ENNReal instTopENNReal PseudoMetricSpace.toNNDist instPseudoMetricSpace fact_one_le_top_ennreal iSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot WithLp.ofLp	—	NNReal.eq fact_one_le_top_ennreal NNReal.coe_iSup dist_eq_iSup
nndist_eq_of_L1 📖	mathematical	—	NNDist.nndist PiLp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal PseudoMetricSpace.toNNDist instPseudoMetricSpace fact_one_le_one_ennreal SeminormedAddCommGroup.toPseudoMetricSpace Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ WithLp.ofLp	—	NNReal.eq fact_one_le_one_ennreal NNReal.coe_sum Finset.sum_congr dist_eq_of_L1
nndist_eq_of_L2 📖	mathematical	—	NNDist.nndist PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat PseudoMetricSpace.toNNDist instPseudoMetricSpace fact_one_le_two_ennreal SeminormedAddCommGroup.toPseudoMetricSpace DFunLike.coe OrderIso NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instFunLikeOrderIso NNReal.sqrt Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat NNReal.eq fact_one_le_two_ennreal Real.coe_sqrt NNReal.coe_sum Finset.sum_congr dist_eq_of_L2
nndist_eq_sum 📖	mathematical	—	NNDist.nndist PiLp PseudoMetricSpace.toNNDist instPseudoMetricSpace NNReal Real NNReal.instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ WithLp.ofLp ENNReal.toReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	NNReal.eq NNReal.coe_sum Finset.sum_congr dist_eq_sum ENNReal.toReal_pos_iff_ne_top
nndist_toLp_single_same 📖	mathematical	—	NNDist.nndist WithLp PseudoMetricSpace.toNNDist instPseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	nndist_eq_nnnorm WithLp.toLp_sub Pi.single_sub nnnorm_toLp_single
nnnorm_apply_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup WithLp.ofLp PiLp seminormedAddCommGroup	—	nndist_zero_right nndist_apply_le
nnnorm_eq_ciSup 📖	mathematical	—	NNNorm.nnnorm PiLp Top.top ENNReal instTopENNReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup fact_one_le_top_ennreal iSup NNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot WithLp.ofLp	—	NNReal.eq fact_one_le_top_ennreal NNReal.coe_iSup
nnnorm_eq_of_L1 📖	mathematical	—	NNNorm.nnnorm PiLp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup fact_one_le_one_ennreal Finset.sum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ WithLp.ofLp	—	NNReal.eq fact_one_le_one_ennreal NNReal.coe_sum Finset.sum_congr norm_eq_of_L1
nnnorm_eq_of_L2 📖	mathematical	—	NNNorm.nnnorm PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup fact_one_le_two_ennreal DFunLike.coe OrderIso NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal instFunLikeOrderIso NNReal.sqrt Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat NNReal.eq fact_one_le_two_ennreal Real.coe_sqrt NNReal.coe_sum Finset.sum_congr norm_eq_of_L2
nnnorm_eq_sum 📖	mathematical	—	NNNorm.nnnorm PiLp SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup NNReal Real NNReal.instPowReal Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Finset.univ WithLp.ofLp ENNReal.toReal DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	NNReal.eq norm_eq_sum ENNReal.toReal_pos_iff_ne_top one_div NNReal.coe_sum Finset.sum_congr
nnnorm_ofLp 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm Pi.seminormedAddGroup SeminormedAddCommGroup.toSeminormedAddGroup WithLp.ofLp Top.top ENNReal instTopENNReal PiLp seminormedAddCommGroup fact_one_le_top_ennreal	—	fact_one_le_top_ennreal nnnorm_eq_ciSup Pi.nnnorm_def Finset.sup_univ_eq_ciSup
nnnorm_seminormedAddCommGroupToPi 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroupToPi WithLp seminormedAddCommGroup WithLp.toLp	—	—
nnnorm_toLp 📖	mathematical	—	NNNorm.nnnorm WithLp Top.top ENNReal instTopENNReal SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup fact_one_le_top_ennreal WithLp.toLp Pi.seminormedAddGroup	—	fact_one_le_top_ennreal nnnorm_ofLp
nnnorm_toLp_const 📖	mathematical	—	NNNorm.nnnorm WithLp SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup WithLp.toLp NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Real NNReal.instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal	—	ENNReal.dichotomy LT.lt.ne' LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike nnnorm_eq_sum Finset.sum_congr Finset.sum_const nsmul_eq_mul NNReal.mul_rpow mul_one_div_cancel NNReal.rpow_one ENNReal.toReal_div
nnnorm_toLp_const' 📖	mathematical	—	NNNorm.nnnorm WithLp SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup WithLp.toLp NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Real NNReal.instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal	—	em fact_one_le_top_ennreal nnnorm_eq_ciSup ciSup_const ENNReal.div_top NNReal.rpow_zero one_mul nnnorm_toLp_const
nnnorm_toLp_one 📖	mathematical	—	NNNorm.nnnorm WithLp SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup WithLp.toLp Pi.instOne NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal Real NNReal.instPowReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal	—	nnnorm_toLp_const
nnnorm_toLp_single 📖	mathematical	—	NNNorm.nnnorm WithLp SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup seminormedAddCommGroup WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	nnnorm_eq_ciSup ciSup_eq_of_forall_le_of_forall_lt_exists_gt Decidable.eq_or_ne Pi.single_eq_same le_refl Pi.single_eq_of_ne' nnnorm_zero zero_le NNReal.instCanonicallyOrderedAdd LT.lt.trans_eq Nat.cast_zero LT.lt.ne' LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.out nnnorm_eq_sum ENNReal.coe_ne_top ENNReal.coe_toReal Fintype.sum_eq_single toLp_apply Pi.single_eq_of_ne NNReal.zero_rpow NNReal.rpow_mul one_div mul_inv_cancel₀ NNReal.rpow_one
normSMulClassSeminormedAddCommGroupToPi 📖	mathematical	NormSMulClass SeminormedRing.toNorm SeminormedAddCommGroup.toNorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	seminormedAddCommGroupToPi Pi.instSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	norm_smul instNormSMulClass
norm_apply_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm WithLp.ofLp PiLp instNorm	—	dist_zero_right dist_apply_le
norm_eq_card 📖	mathematical	—	Norm.norm PiLp ENNReal instZeroENNReal instNorm Real Real.instNatCast Finset.card Set.Finite.toFinset setOf WithLp.ofLp Real.instZero Set.toFinite Subtype.finite Finite.of_fintype Set Set.instMembership	—	—
norm_eq_ciSup 📖	mathematical	—	Norm.norm PiLp Top.top ENNReal instTopENNReal instNorm iSup Real Real.instSupSet WithLp.ofLp	—	—
norm_eq_of_L1 📖	mathematical	—	Norm.norm PiLp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal instNorm SeminormedAddCommGroup.toNorm Finset.sum Real Real.instAddCommMonoid Finset.univ WithLp.ofLp	—	norm_eq_sum Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Finset.sum_congr Real.rpow_one div_self
norm_eq_of_L2 📖	mathematical	—	Norm.norm PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instNorm SeminormedAddCommGroup.toNorm Real.sqrt Finset.sum Real Real.instAddCommMonoid Finset.univ Monoid.toNatPow Real.instMonoid WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat norm_eq_of_nat fact_one_le_two_ennreal ENNReal.instCharZero Real.sqrt_eq_rpow Nat.cast_one
norm_eq_of_nat 📖	mathematical	ENNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Norm.norm PiLp instNorm SeminormedAddCommGroup.toNorm Real Real.instPow Finset.sum Real.instAddCommMonoid Finset.univ Monoid.toNatPow Real.instMonoid WithLp.ofLp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast	—	ENNReal.toReal_pos_iff_ne_top ne_of_eq_of_ne ENNReal.natCast_ne_top norm_eq_sum Finset.sum_congr ENNReal.toReal_natCast Real.rpow_natCast one_div
norm_eq_sum 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Norm.norm PiLp instNorm Real.instPow Finset.sum Real.instAddCommMonoid Finset.univ WithLp.ofLp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	ENNReal.toReal_pos_iff LT.lt.ne' LT.lt.ne
norm_ofLp 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm Pi.seminormedAddCommGroup WithLp.ofLp Top.top ENNReal instTopENNReal PiLp instNorm	—	fact_one_le_top_ennreal nnnorm_ofLp
norm_seminormedAddCommGroupToPi 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm seminormedAddCommGroupToPi WithLp instNorm WithLp.toLp	—	—
norm_sq_eq_of_L2 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Norm.norm PiLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat instNorm SeminormedAddCommGroup.toNorm Finset.sum Real.instAddCommMonoid Finset.univ WithLp.ofLp	—	Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal nnnorm_eq_of_L2 NNReal.sq_sqrt NNReal.coe_sum
norm_toLp 📖	mathematical	—	Norm.norm WithLp Top.top ENNReal instTopENNReal instNorm SeminormedAddCommGroup.toNorm WithLp.toLp Pi.seminormedAddCommGroup	—	norm_ofLp
norm_toLp_const 📖	mathematical	—	Norm.norm WithLp instNorm SeminormedAddCommGroup.toNorm WithLp.toLp Real Real.instMul Real.instPow NNReal.toReal NNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal	—	nnnorm_toLp_const one_div ENNReal.toReal_inv NNReal.coe_natCast
norm_toLp_const' 📖	mathematical	—	Norm.norm WithLp instNorm SeminormedAddCommGroup.toNorm WithLp.toLp Real Real.instMul Real.instPow NNReal.toReal NNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal	—	nnnorm_toLp_const' one_div ENNReal.toReal_inv NNReal.coe_natCast
norm_toLp_one 📖	mathematical	—	Norm.norm WithLp instNorm SeminormedAddCommGroup.toNorm WithLp.toLp Pi.instOne Real Real.instMul Real.instPow NNReal.toReal NNReal AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal Fintype.card ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne instAddCommMonoidWithOneENNReal	—	norm_toLp_const
norm_toLp_single 📖	mathematical	—	Norm.norm WithLp instNorm SeminormedAddCommGroup.toNorm WithLp.toLp Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	nnnorm_toLp_single
proj_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring PiLp topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup WithLp.instModule Pi.module ContinuousLinearMap.funLike proj WithLp.ofLp	—	—
projₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PiLp AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup WithLp.instModule Pi.module LinearMap.instFunLike projₗ WithLp.ofLp	—	—
secondCountableTopology 📖	mathematical	SecondCountableTopology	PiLp topologicalSpace	—	Homeomorph.secondCountableTopology TopologicalSpace.instSecondCountableTopologyForallOfCountable
smul_apply 📖	mathematical	—	WithLp.ofLp PiLp WithLp.instSMul Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddZero.toZero AddZeroClass.toAddZero	—	—
sub_apply 📖	mathematical	—	WithLp.ofLp PiLp SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	—
sumPiLpEquivProdLpPiLp_apply_ofLp 📖	mathematical	—	WithLp.ofLp WithLp DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids seminormedAddCommGroup instFintypeSum WithLp.instProdSeminormedAddCommGroup WithLp.instModule Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup Pi.module AddCommGroup.toAddCommMonoid Prod.instAddCommGroup Prod.instModule WithLp.instAddCommGroup EquivLike.toFunLike LinearIsometryEquiv.instEquivLike sumPiLpEquivProdLpPiLp WithLp.toLp	—	RingHomInvPair.ids
sumPiLpEquivProdLpPiLp_symm_apply_ofLp 📖	mathematical	—	WithLp.ofLp DFunLike.coe LinearIsometryEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids WithLp WithLp.instProdSeminormedAddCommGroup seminormedAddCommGroup instFintypeSum WithLp.instModule Prod.instAddCommGroup SeminormedAddCommGroup.toAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Pi.module EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm sumPiLpEquivProdLpPiLp LinearEquiv Prod.instAddCommMonoid Pi.addCommMonoid LinearEquiv.instEquivLike LinearEquiv.symm LinearEquiv.prodCongr WithLp.linearEquiv	—	RingHomInvPair.ids
toEquiv_homeomorph 📖	mathematical	—	Homeomorph.toEquiv PiLp topologicalSpace Pi.topologicalSpace homeomorph WithLp.equiv	—	—
toEquiv_uniformEquiv 📖	mathematical	—	UniformEquiv.toEquiv PiLp uniformSpace Pi.uniformSpace uniformEquiv WithLp.equiv	—	—
toHomeomorph_uniformEquiv 📖	mathematical	—	UniformEquiv.toHomeomorph PiLp uniformSpace Pi.uniformSpace uniformEquiv homeomorph UniformSpace.toTopologicalSpace	—	—
toLp_apply 📖	mathematical	—	WithLp.ofLp WithLp.toLp	—	—
uniformContinuous_ofLp 📖	mathematical	—	UniformContinuous WithLp uniformSpace Pi.uniformSpace WithLp.ofLp	—	uniformContinuous_comap
uniformContinuous_toLp 📖	mathematical	—	UniformContinuous WithLp Pi.uniformSpace uniformSpace WithLp.toLp	—	uniformContinuous_comap' uniformContinuous_id
zero_apply 📖	mathematical	—	WithLp.ofLp PiLp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup SeminormedAddCommGroup.toAddCommGroup	—	—

(root)

Definitions

Name	Category	Theorems
PiLp 📖	CompOp	127 math math: DirectSum.IsInternal.isometryL2OfOrthogonalFamily_symm_apply, PiLp.continuousLinearEquiv_symm_apply, PiLp.nndist_eq_sum, PiLp.basisFun_equivFun, PiLp.edist_self, LinearIsometryEquiv.piLpCongrRight_symm, contDiffOn_piLp', PiLp.completeSpace, frontier_halfSpace, PiLp.toEquiv_uniformEquiv, LinearMap.IsSymmetric.diagonalization_apply_self_apply, PiLp.norm_ofLp, contDiff_piLp', Behrend.sphere_subset_preimage_metric_sphere, LinearIsometryEquiv.piLpCongrRight_apply, PiLp.nnnorm_eq_of_L2, MeasureTheory.integrable_piLp_iff, PiLp.instProdT0Space, PiLp.coe_continuousLinearEquiv, coe_equiv_lpPiLp_symm, MeasureTheory.charFunDual_pi', PiLp.dist_eq_card, contDiffAt_piLp_apply, LinearIsometryEquiv.piLpCongrLeft_apply, PiLp.sub_apply, PiLp.edist_eq_sum, PiLp.nndist_apply_le, coe_addEquiv_lpPiLp_symm, PiLp.instNormSMulClass, PiLp.hasFDerivAt_toLp, Pi.orthonormalBasis_apply, LinearMap.IsSymmetric.diagonalization_symm_apply, PiLp.dist_eq_of_L1, PiLp.enorm_apply_le, PiLp.nnnorm_apply_le, PiLp.basisFun_repr, interior_halfSpace, PiLp.dist_eq_iSup, PiLp.norm_eq_sum, LinearIsometryEquiv.piLpCurry_apply, contDiffAt_piLp', hasStrictFDerivAt_piLp, PiLp.basisFun_apply, LinearIsometryEquiv.piLpCongrRight_single, hasFDerivWithinAt_piLp, differentiableOn_piLp, closure_open_halfSpace, PiLp.nnnorm_eq_ciSup, PiLp.norm_sq_eq_of_L2, PiLp.isOpenMap_apply, PiLp.norm_eq_of_L1, coe_equiv_lpPiLp, differentiableAt_piLp, contDiff_piLp, PiLp.norm_eq_ciSup, PiLp.borelSpace, PiLp.dist_apply_le, PiLp.edist_eq_iSup, LinearIsometryEquiv.piLpCongrRight_refl, PiLp.continuous_apply, coe_lpPiLpₗᵢ, PiLp.edist_apply_le, contDiffOn_piLp, Pi.orthonormalBasis.toBasis, PiLp.smul_apply, PiLp.projₗ_apply, MeasureTheory.memLp_piLp_iff, EuclideanSpace.piLpCongrLeft_single, PiLp.toEquiv_homeomorph, LinearIsometryEquiv.piLpCurry_symm_apply, PiLp.secondCountableTopology, PiLp.dist_sq_eq_of_L2, PiLp.hasStrictFDerivAt_apply, PiLp.toHomeomorph_uniformEquiv, PiLp.add_apply, PiLp.norm_eq_of_nat, coe_lpPiLpₗᵢ_symm, PiLp.norm_apply_le, differentiable_piLp, contDiffOn_piLp_apply, MeasureTheory.Integrable.of_eval_piLp, ProbabilityTheory.iIndepFun_iff_charFunDual_pi', PiLp.basis_toMatrix_basisFun_mul, PiLp.edist_eq_card, PiLp.nnnorm_eq_of_L1, PiLp.hasFDerivAt_ofLp, contDiff_piLp_apply, contDiffWithinAt_piLp, MeasureTheory.charFunDual_eq_pi_iff', MeasureTheory.MemLp.of_eval_piLp, coe_addEquiv_lpPiLp, PiLp.hasFDerivAt_apply, PiLp.proj_apply, PiLp.dist_eq_of_L2, LinearIsometryEquiv.piLpCongrLeft_single, PiLp.neg_apply, PiLp.coe_symm_continuousLinearEquiv, PiLp.nnnorm_eq_sum, PiLp.inner_apply, PiLp.zero_apply, contDiffAt_piLp, differentiableWithinAt_piLp, PiLp.hasStrictFDerivAt_ofLp, PiLp.basisFun_map, equiv_lpPiLp_norm, PiLp.continuousLinearEquiv_apply, PiLp.norm_eq_of_L2, MeasureTheory.eval_integral_piLp, closure_halfSpace, LinearIsometryEquiv.piLpCongrLeft_symm, Pi.orthonormalBasis_repr, contDiffWithinAt_piLp', PiLp.edist_eq_of_L1, PiLp.instIsBoundedSMul, contDiffWithinAt_piLp_apply, interior_euclideanQuadrant, PiLp.edist_comm, PiLp.nndist_eq_of_L2, RCLike.inner_eq_wInner_one, Matrix.toLpLin_eq_toLin, PiLp.nnnorm_ofLp, PiLp.dist_eq_sum, PiLp.edist_eq_of_L2, PiLp.nndist_eq_iSup, PiLp.norm_eq_card, PiLp.nndist_eq_of_L1, PiLp.hasStrictFDerivAt_toLp
instCoeFunPiLpForall 📖	CompOp	—
instInhabitedPiLp 📖	CompOp	—

---

← Back to Index