lpSpace

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

Statistics

Metric	Count
Definitions Memℓp, algebraOfNormedAlgebra, PreLp, algebra, unique, instAddCommGroupPreLp, lp, coeFnAddMonoidHom, coeFun, inftyNormedAlgebra, inftyNormedCommRing, inftyNormedRing, inftyRing, inftyStarRing, instCoeOutSubtypePreLpMemAddSubgroupForall, instInvolutiveStar, instModulePreLp, instModuleSubtypePreLpMemAddSubgroup, instMulSubtypePreLpMemAddSubgroupTopENNReal, instNormSubtypePreLpMemAddSubgroup, instNormedSpace, instStarAddMonoid, instStarSubtypePreLpMemAddSubgroup, lsingle, nonUnitalNormedCommRing, nonUnitalNormedRing, nonUnitalRing, normedAddCommGroup, single, singleAddMonoidHom, singleContinuousAddMonoidHom, singleContinuousLinearMap, «termℓ^∞(_)»»), «termℓ^∞(_,_)»»), lpInftySubalgebra, lpInftySubring, lpSubmodule	37
Theorems coordinate, coordinate, uniformly_bounded, add, bddAbove, const_mul, const_smul, finite_dsupport, finset_sum, infty_mul, infty_pow, neg, neg_iff, of_exponent_ge, star_iff, star_mem, sub, summable, algebraMap_memℓp_infty, intCast_memℓp_infty, coeFnAddMonoidHom_apply, coeFn_add, coeFn_neg, coeFn_single, coeFn_smul, coeFn_star, coeFn_sub, coeFn_sum, coeFn_zero, coe_lpSubmodule, completeSpace, eq_zero', eq_zero_iff_coeFn_eq_zero, ext, ext_continuousAddMonoidHom, ext_continuousAddMonoidHom_iff, ext_continuousLinearMap, ext_continuousLinearMap_iff, ext_iff, hasSum_norm, hasSum_single, inftyCStarRing, infty_coeFn_intCast, infty_coeFn_mul, infty_coeFn_natCast, infty_coeFn_one, infty_coeFn_pow, infty_isScalarTower, infty_smulCommClass, instIsBoundedSMulSubtypePreLpMemAddSubgroup, instIsCentralScalarPreLp, instIsCentralScalarSubtypePreLpMemAddSubgroup, instIsScalarTowerPreLp, instIsScalarTowerSubtypePreLpMemAddSubgroup, instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, instNormedStarGroupSubtypePreLpMemAddSubgroup, instSMulCommClassPreLp, instSMulCommClassSubtypePreLpMemAddSubgroup, instStarModuleSubtypePreLpMemAddSubgroup, isLUB_norm, isometry_single, lsingle_apply, mem_lp_const_smul, memℓp, memℓp_of_tendsto, monotone, norm_apply_le_norm, norm_apply_le_of_tendsto, norm_compl_sum_single, norm_const_smul, norm_const_smul_le, norm_eq_card_dsupport, norm_eq_ciSup, norm_eq_tsum_rpow, norm_eq_zero_iff, norm_le_of_forall_le, norm_le_of_forall_le', norm_le_of_forall_sum_le, norm_le_of_tendsto, norm_le_of_tsum_le, norm_neg, norm_nonneg', norm_rpow_eq_tsum, norm_single, norm_sub_norm_compl_sub_single, norm_sum_single, norm_zero, singleAddMonoidHom_apply, singleContinuousAddMonoidHom_apply, singleContinuousLinearMap_apply, single_add, single_apply, single_apply_ne, single_apply_self, single_neg, single_smul, single_sub, single_zero, star_apply, sum_rpow_le_norm_rpow, sum_rpow_le_of_tendsto, summable_mul, tendsto_lp_of_tendsto_pi, tsum_mul_le_mul_norm, tsum_mul_le_mul_norm', uniformContinuous_coe, memℓp_gen, memℓp_gen', memℓp_gen_iff, memℓp_infty, memℓp_infty_iff, memℓp_zero, memℓp_zero_iff, natCast_memℓp_infty, one_memℓp_infty, zero_mem_ℓp', zero_memℓp	117
Total	154

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coordinate 📖	mathematical	—	LipschitzOnWith PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace lp.inftyNormedRing NormedCommRing.toNormedRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField Real.metricSpace	—	NormedDivisionRing.to_normOneClass lp.norm_apply_le_norm ENNReal.top_ne_zero lp.norm_le_of_forall_le mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing NNReal.coe_nonneg dist_nonneg

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coordinate 📖	mathematical	—	LipschitzWith PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace lp.inftyNormedRing NormedCommRing.toNormedRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField Real.metricSpace	—	NormedDivisionRing.to_normOneClass LipschitzOnWith.coordinate
uniformly_bounded 📖	—	LipschitzWith Real PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace Memℓp Real.normedAddCommGroup Top.top ENNReal instTopENNReal	—	—	sub_add_cancel abs_add_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_le_add covariant_swap_add_of_covariant_add lipschitzWith_iff_dist_le_mul

Memℓp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Memℓp	Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ENNReal.trichotomy memℓp_zero Set.Finite.subset Set.Finite.union finite_dsupport Mathlib.Tactic.Contrapose.contrapose₂ add_zero memℓp_infty bddAbove le_trans norm_add_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add memℓp_gen Nat.instAtLeastTwoHAddOfNat Summable.of_nonneg_of_le Real.rpow_nonneg norm_nonneg LE.le.trans Real.rpow_le_rpow LT.lt.le one_mul NNReal.coe_le_coe NNReal.rpow_add_le_add_rpow Fin.sum_univ_succ Finset.sum_congr Finset.univ_unique Finset.sum_singleton Fintype.card_fin Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg NNReal.coe_nonneg Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Summable.add IsTopologicalSemiring.toContinuousAdd summable
bddAbove 📖	mathematical	Memℓp Top.top ENNReal instTopENNReal	BddAbove Real Real.instLE Set.range Norm.norm NormedAddCommGroup.toNorm	—	memℓp_infty_iff
const_mul 📖	mathematical	Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing	—	const_smul NonUnitalSeminormedRing.isBoundedSMul
const_smul 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid Memℓp	Pi.instSMul	—	ENNReal.trichotomy memℓp_zero Set.Finite.subset finite_dsupport not_imp_not smul_zero bddAbove memℓp_infty LE.le.trans norm_smul_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg memℓp_gen Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal summable NNReal.summable_of_le NNReal.rpow_le_rpow nnnorm_smul_le le_of_lt
finite_dsupport 📖	mathematical	Memℓp ENNReal instZeroENNReal	Set.Finite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	memℓp_zero_iff
finset_sum 📖	mathematical	Memℓp	Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Finset.induction_on Finset.sum_insert add Finset.mem_insert_self Finset.mem_insert_of_mem
infty_mul 📖	mathematical	Memℓp NonUnitalNormedRing.toNormedAddCommGroup Top.top ENNReal instTopENNReal	Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	memℓp_infty_iff bddAbove norm_mul_le mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono norm_nonneg LE.le.trans
infty_pow 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Top.top ENNReal instTopENNReal	Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Subring.pow_mem
neg 📖	mathematical	Memℓp	Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	ENNReal.trichotomy memℓp_zero finite_dsupport memℓp_infty norm_neg bddAbove memℓp_gen summable
neg_iff 📖	mathematical	—	Memℓp Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg neg_neg
of_exponent_ge 📖	—	Memℓp ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	—	—	ENNReal.trichotomy₂ memℓp_infty Set.Finite.bddAbove instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Set.Finite.image finite_dsupport norm_zero LE.le.trans le_max_right memℓp_gen Real.zero_rpow LT.lt.ne' summable_of_ne_finset_zero SummationFilter.instHasSupportOfLeAtTop SummationFilter.instLeAtTopUnconditional Filter.Tendsto.bddAbove_range_of_cofinite BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Summable.tendsto_cofinite_zero instIsTopologicalAddGroupReal summable Real.rpow_nonneg norm_nonneg mul_inv_cancel₀ Real.rpow_one Real.rpow_le_rpow inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.le Summable.of_norm_bounded_eventually Real.instCompleteSpace Set.Finite.subset Filter.Tendsto.eventually_lt_const Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.one_le_rpow Mathlib.Tactic.Contrapose.contrapose₂ Real.rpow_le_rpow_of_exponent_ge' abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono
star_iff 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup	Memℓp Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	star_mem star_star
star_mem 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup Memℓp	Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	ENNReal.trichotomy memℓp_zero finite_dsupport memℓp_infty norm_star bddAbove memℓp_gen summable
sub 📖	mathematical	Memℓp	Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	sub_eq_add_neg add neg
summable 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal Memℓp	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm SummationFilter.unconditional	—	memℓp_gen_iff

Pi

Definitions

Name	Category	Theorems
algebraOfNormedAlgebra 📖	CompOp	1 math math: algebraMap_memℓp_infty

PreLp

Definitions

Name	Category	Theorems
algebra 📖	CompOp	—
unique 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Memℓp 📖	MathDef	18 math math: zero_memℓp, zero_mem_ℓp', memℓp_infty, memℓp_zero_iff, memℓp_gen_iff, lp.memℓp, memℓp_infty_iff, lp.memℓp_of_tendsto, memℓp_gen, one_memℓp_infty, memℓp_gen', algebraMap_memℓp_infty, Memℓp.all, Memℓp.star_iff, intCast_memℓp_infty, memℓp_zero, Memℓp.neg_iff, natCast_memℓp_infty
PreLp 📖	CompOp	124 math math: lp.norm_apply_le_norm, lp.isLUB_norm, IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, lp.instNormedStarGroupSubtypePreLpMemAddSubgroup, lp.inner_eq_tsum, lp.coeFn_star, lp.norm_eq_zero_iff, IsHilbertSum.linearIsometryEquiv_symm_apply, lp.eq_zero_iff_coeFn_eq_zero, lp.coeFnAddMonoidHom_apply, lp.sum_rpow_le_norm_rpow, lp.norm_sum_single, IsHilbertSum.hasSum_linearIsometryEquiv_symm, coe_equiv_lpPiLp_symm, lp.inftyCStarRing, lp.norm_rpow_eq_tsum, lp.instIsCentralScalarPreLp, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, lp.coeFn_single, lp.summable_mul, lp.hasSum_single, lp.memℓp, lp.coeFn_zero, lp.norm_const_smul, coe_addEquiv_lpPiLp_symm, lp.single_apply_ne, lp.singleAddMonoidHom_apply, HilbertBasis.hasSum_repr, lp.singleContinuousAddMonoidHom_apply, lp.inner_single_right, lp.norm_nonneg', lp.single_neg, coe_ringEquiv_lpBCF, lp.single_zero, coe_lpBCFₗᵢ, lp.infty_coeFn_mul, lp.coeFn_add, OrthogonalFamily.hasSum_linearIsometry, lp.instSMulCommClassSubtypePreLpMemAddSubgroup, lp.monotone, lp.singleContinuousLinearMap_apply, LipschitzWith.coordinate, Orthonormal.linearIsometryEquiv_symm_apply_single_one, OrthogonalFamily.summable_of_lp, lp.coeFn_sub, lp.ext_continuousAddMonoidHom_iff, lp.infty_coeFn_pow, lp.infty_smulCommClass, lp.norm_eq_card_dsupport, GromovHausdorff.ghDist_eq_hausdorffDist, lp.instStarModuleSubtypePreLpMemAddSubgroup, coe_equiv_lpPiLp, lp.coeFn_sum, lp.norm_compl_sum_single, KuratowskiEmbedding.embeddingOfSubset_isometry, lp.coe_lpSubmodule, GromovHausdorff.eq_toGHSpace, lp.single_sub, coe_lpPiLpₗᵢ, lp.lsingle_apply, lp.norm_neg, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, lp.coeFn_smul, lp.summable_inner, lp.infty_coeFn_one, coe_addEquiv_lpBCF_symm, lp.single_smul, lp.ext_iff, lp.norm_zero, LipschitzOnWith.coordinate, lp.instIsCentralScalarSubtypePreLpMemAddSubgroup, lp.instIsScalarTowerPreLp, lp.inner_single_left, lp.hasSum_norm, lp.infty_coeFn_intCast, lp.tsum_mul_le_mul_norm', coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, lp.norm_single, coe_addEquiv_lpBCF, lp.mem_lp_const_smul, OrthogonalFamily.range_linearIsometry, lp.single_add, lp.norm_sub_norm_compl_sub_single, lp.infty_coeFn_natCast, lp.hasSum_inner, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, coe_addEquiv_lpPiLp, lp.infty_isScalarTower, lp.eq_zero', lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, lp.single_apply, lp.isometry_single, KuratowskiEmbedding.embeddingOfSubset_dist_le, coe_ringEquiv_lpBCF_symm, lp.norm_eq_tsum_rpow, lp.coeFn_neg, lp.norm_const_smul_le, lp.norm_eq_ciSup, lp.completeSpace, KuratowskiEmbedding.exists_isometric_embedding, lp.instIsBoundedSMulSubtypePreLpMemAddSubgroup, KuratowskiEmbedding.embeddingOfSubset_coe, lp.star_apply, equiv_lpPiLp_norm, lp.uniformContinuous_coe, coe_algEquiv_lpBCF_symm, lp.instSMulCommClassPreLp, OrthogonalFamily.linearIsometry_apply, lp.single_apply_self, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, lp.instIsScalarTowerSubtypePreLpMemAddSubgroup, HilbertBasis.hasSum_repr_symm, kuratowskiEmbedding.isometry, lp.tsum_mul_le_mul_norm, lp.ext_continuousLinearMap_iff
instAddCommGroupPreLp 📖	CompOp	124 math math: lp.norm_apply_le_norm, lp.isLUB_norm, IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, lp.instNormedStarGroupSubtypePreLpMemAddSubgroup, lp.inner_eq_tsum, lp.coeFn_star, lp.norm_eq_zero_iff, IsHilbertSum.linearIsometryEquiv_symm_apply, lp.eq_zero_iff_coeFn_eq_zero, lp.coeFnAddMonoidHom_apply, lp.sum_rpow_le_norm_rpow, lp.norm_sum_single, IsHilbertSum.hasSum_linearIsometryEquiv_symm, coe_equiv_lpPiLp_symm, lp.inftyCStarRing, lp.norm_rpow_eq_tsum, lp.instIsCentralScalarPreLp, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, lp.coeFn_single, lp.summable_mul, lp.hasSum_single, lp.memℓp, lp.coeFn_zero, lp.norm_const_smul, coe_addEquiv_lpPiLp_symm, lp.single_apply_ne, lp.singleAddMonoidHom_apply, HilbertBasis.hasSum_repr, lp.singleContinuousAddMonoidHom_apply, lp.inner_single_right, lp.norm_nonneg', lp.single_neg, coe_ringEquiv_lpBCF, lp.single_zero, coe_lpBCFₗᵢ, lp.infty_coeFn_mul, lp.coeFn_add, OrthogonalFamily.hasSum_linearIsometry, lp.instSMulCommClassSubtypePreLpMemAddSubgroup, lp.monotone, lp.singleContinuousLinearMap_apply, LipschitzWith.coordinate, Orthonormal.linearIsometryEquiv_symm_apply_single_one, OrthogonalFamily.summable_of_lp, lp.coeFn_sub, lp.ext_continuousAddMonoidHom_iff, lp.infty_coeFn_pow, lp.infty_smulCommClass, lp.norm_eq_card_dsupport, GromovHausdorff.ghDist_eq_hausdorffDist, lp.instStarModuleSubtypePreLpMemAddSubgroup, coe_equiv_lpPiLp, lp.coeFn_sum, lp.norm_compl_sum_single, KuratowskiEmbedding.embeddingOfSubset_isometry, lp.coe_lpSubmodule, GromovHausdorff.eq_toGHSpace, lp.single_sub, coe_lpPiLpₗᵢ, lp.lsingle_apply, lp.norm_neg, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, lp.coeFn_smul, lp.summable_inner, lp.infty_coeFn_one, coe_addEquiv_lpBCF_symm, lp.single_smul, lp.ext_iff, lp.norm_zero, LipschitzOnWith.coordinate, lp.instIsCentralScalarSubtypePreLpMemAddSubgroup, lp.instIsScalarTowerPreLp, lp.inner_single_left, lp.hasSum_norm, lp.infty_coeFn_intCast, lp.tsum_mul_le_mul_norm', coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, lp.norm_single, coe_addEquiv_lpBCF, lp.mem_lp_const_smul, OrthogonalFamily.range_linearIsometry, lp.single_add, lp.norm_sub_norm_compl_sub_single, lp.infty_coeFn_natCast, lp.hasSum_inner, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, coe_addEquiv_lpPiLp, lp.infty_isScalarTower, lp.eq_zero', lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, lp.single_apply, lp.isometry_single, KuratowskiEmbedding.embeddingOfSubset_dist_le, coe_ringEquiv_lpBCF_symm, lp.norm_eq_tsum_rpow, lp.coeFn_neg, lp.norm_const_smul_le, lp.norm_eq_ciSup, lp.completeSpace, KuratowskiEmbedding.exists_isometric_embedding, lp.instIsBoundedSMulSubtypePreLpMemAddSubgroup, KuratowskiEmbedding.embeddingOfSubset_coe, lp.star_apply, equiv_lpPiLp_norm, lp.uniformContinuous_coe, coe_algEquiv_lpBCF_symm, lp.instSMulCommClassPreLp, OrthogonalFamily.linearIsometry_apply, lp.single_apply_self, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, lp.instIsScalarTowerSubtypePreLpMemAddSubgroup, HilbertBasis.hasSum_repr_symm, kuratowskiEmbedding.isometry, lp.tsum_mul_le_mul_norm, lp.ext_continuousLinearMap_iff
lp 📖	CompOp	121 math math: lp.norm_apply_le_norm, lp.isLUB_norm, IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, lp.instNormedStarGroupSubtypePreLpMemAddSubgroup, lp.inner_eq_tsum, lp.coeFn_star, lp.norm_eq_zero_iff, IsHilbertSum.linearIsometryEquiv_symm_apply, lp.eq_zero_iff_coeFn_eq_zero, lp.coeFnAddMonoidHom_apply, lp.sum_rpow_le_norm_rpow, lp.norm_sum_single, IsHilbertSum.hasSum_linearIsometryEquiv_symm, coe_equiv_lpPiLp_symm, lp.inftyCStarRing, lp.norm_rpow_eq_tsum, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, lp.coeFn_single, lp.summable_mul, lp.hasSum_single, lp.memℓp, lp.coeFn_zero, lp.norm_const_smul, coe_addEquiv_lpPiLp_symm, lp.single_apply_ne, lp.singleAddMonoidHom_apply, HilbertBasis.hasSum_repr, lp.singleContinuousAddMonoidHom_apply, lp.inner_single_right, lp.norm_nonneg', lp.single_neg, coe_ringEquiv_lpBCF, lp.single_zero, coe_lpBCFₗᵢ, lp.infty_coeFn_mul, lp.coeFn_add, OrthogonalFamily.hasSum_linearIsometry, lp.instSMulCommClassSubtypePreLpMemAddSubgroup, lp.monotone, lp.singleContinuousLinearMap_apply, LipschitzWith.coordinate, Orthonormal.linearIsometryEquiv_symm_apply_single_one, OrthogonalFamily.summable_of_lp, lp.coeFn_sub, lp.ext_continuousAddMonoidHom_iff, lp.infty_coeFn_pow, lp.infty_smulCommClass, lp.norm_eq_card_dsupport, GromovHausdorff.ghDist_eq_hausdorffDist, lp.instStarModuleSubtypePreLpMemAddSubgroup, coe_equiv_lpPiLp, lp.coeFn_sum, lp.norm_compl_sum_single, KuratowskiEmbedding.embeddingOfSubset_isometry, lp.coe_lpSubmodule, GromovHausdorff.eq_toGHSpace, lp.single_sub, coe_lpPiLpₗᵢ, lp.lsingle_apply, lp.norm_neg, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, lp.coeFn_smul, lp.summable_inner, lp.infty_coeFn_one, coe_addEquiv_lpBCF_symm, lp.single_smul, lp.ext_iff, lp.norm_zero, LipschitzOnWith.coordinate, lp.instIsCentralScalarSubtypePreLpMemAddSubgroup, lp.inner_single_left, lp.hasSum_norm, lp.infty_coeFn_intCast, lp.tsum_mul_le_mul_norm', coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, lp.norm_single, coe_addEquiv_lpBCF, lp.mem_lp_const_smul, OrthogonalFamily.range_linearIsometry, lp.single_add, lp.norm_sub_norm_compl_sub_single, lp.infty_coeFn_natCast, lp.hasSum_inner, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, coe_addEquiv_lpPiLp, lp.infty_isScalarTower, lp.eq_zero', lp.instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, lp.single_apply, lp.isometry_single, KuratowskiEmbedding.embeddingOfSubset_dist_le, coe_ringEquiv_lpBCF_symm, lp.norm_eq_tsum_rpow, lp.coeFn_neg, lp.norm_const_smul_le, lp.norm_eq_ciSup, lp.completeSpace, KuratowskiEmbedding.exists_isometric_embedding, lp.instIsBoundedSMulSubtypePreLpMemAddSubgroup, KuratowskiEmbedding.embeddingOfSubset_coe, lp.star_apply, equiv_lpPiLp_norm, lp.uniformContinuous_coe, coe_algEquiv_lpBCF_symm, OrthogonalFamily.linearIsometry_apply, lp.single_apply_self, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, lp.instIsScalarTowerSubtypePreLpMemAddSubgroup, HilbertBasis.hasSum_repr_symm, kuratowskiEmbedding.isometry, lp.tsum_mul_le_mul_norm, lp.ext_continuousLinearMap_iff
lpInftySubalgebra 📖	CompOp	—
lpInftySubring 📖	CompOp	—
lpSubmodule 📖	CompOp	1 math math: lp.coe_lpSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_memℓp_infty 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField Pi.semiring Ring.toSemiring RingHom.instFunLike algebraMap Pi.algebraOfNormedAlgebra Top.top ENNReal instTopENNReal	—	Algebra.algebraMap_eq_smul_one Memℓp.const_smul NormedSpace.toIsBoundedSMul one_memℓp_infty
intCast_memℓp_infty 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Pi.instIntCast AddGroupWithOne.toIntCast Top.top ENNReal instTopENNReal	—	intCast_mem Subring.instSubringClass
memℓp_gen 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal SummationFilter.unconditional	Memℓp	—	ENNReal.trichotomy memℓp_zero Real.rpow_zero Set.Finite.subset Set.Finite.of_summable_const Real.instIsOrderedAddMonoid Real.instArchimedean HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Set.subset_univ memℓp_infty Set.image_univ Set.Finite.bddAbove instIsDirectedOrder Real.instIsOrderedRing Set.Finite.image memℓp_gen_iff
memℓp_gen' 📖	mathematical	Real Real.instLE Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal	Memℓp	—	memℓp_gen hasSum_of_isLUB_of_nonneg Real.instIsOrderedAddMonoid instOrderTopologyReal Real.rpow_nonneg norm_nonneg isLUB_ciSup
memℓp_gen_iff 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Memℓp Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm SummationFilter.unconditional	—	LT.lt.ne' ENNReal.toReal_pos_iff LT.lt.ne
memℓp_infty 📖	mathematical	BddAbove Real Real.instLE Set.range Norm.norm NormedAddCommGroup.toNorm	Memℓp Top.top ENNReal instTopENNReal	—	memℓp_infty_iff
memℓp_infty_iff 📖	mathematical	—	Memℓp Top.top ENNReal instTopENNReal BddAbove Real Real.instLE Set.range Norm.norm NormedAddCommGroup.toNorm	—	—
memℓp_zero 📖	mathematical	—	Memℓp ENNReal instZeroENNReal	—	memℓp_zero_iff
memℓp_zero_iff 📖	mathematical	—	Memℓp ENNReal instZeroENNReal Set.Finite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
natCast_memℓp_infty 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Pi.instNatCast AddMonoidWithOne.toNatCast Top.top ENNReal instTopENNReal	—	natCast_mem SubsemiringClass.addSubmonoidWithOneClass SubringClass.toSubsemiringClass Subring.instSubringClass
one_memℓp_infty 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Pi.instOne Top.top ENNReal instTopENNReal	—	Eq.le NormOneClass.norm_one
zero_mem_ℓp' 📖	mathematical	—	Memℓp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	zero_memℓp
zero_memℓp 📖	mathematical	—	Memℓp Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	ENNReal.trichotomy memℓp_zero memℓp_infty norm_zero BddAbove.mono Set.range_const_subset bddAbove_singleton memℓp_gen Real.zero_rpow LT.lt.ne'

lp

Definitions

Name	Category	Theorems
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
coeFun 📖	CompOp	—
inftyNormedAlgebra 📖	CompOp	2 math math: coe_algEquiv_lpBCF_symm, coe_algEquiv_lpBCF
inftyNormedCommRing 📖	CompOp	4 math math: GromovHausdorff.ghDist_eq_hausdorffDist, GromovHausdorff.eq_toGHSpace, KuratowskiEmbedding.embeddingOfSubset_dist_le, GromovHausdorff.eq_toGHSpace_iff
inftyNormedRing 📖	CompOp	10 math math: LipschitzWith.coordinate, GromovHausdorff.ghDist_eq_hausdorffDist, KuratowskiEmbedding.embeddingOfSubset_isometry, GromovHausdorff.eq_toGHSpace, LipschitzOnWith.coordinate, KuratowskiEmbedding.exists_isometric_embedding, coe_algEquiv_lpBCF_symm, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, kuratowskiEmbedding.isometry
inftyRing 📖	CompOp	7 math math: infty_coeFn_pow, infty_coeFn_one, infty_coeFn_intCast, infty_coeFn_natCast, instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, coe_algEquiv_lpBCF_symm, coe_algEquiv_lpBCF
inftyStarRing 📖	CompOp	1 math math: inftyCStarRing
instCoeOutSubtypePreLpMemAddSubgroupForall 📖	CompOp	—
instInvolutiveStar 📖	CompOp	—
instModulePreLp 📖	CompOp	5 math math: instIsCentralScalarPreLp, coe_lpSubmodule, instIsScalarTowerPreLp, mem_lp_const_smul, instSMulCommClassPreLp
instModuleSubtypePreLpMemAddSubgroup 📖	CompOp	37 math math: IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, IsHilbertSum.linearIsometryEquiv_symm_apply, IsHilbertSum.hasSum_linearIsometryEquiv_symm, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, norm_const_smul, HilbertBasis.hasSum_repr, coe_lpBCFₗᵢ, OrthogonalFamily.hasSum_linearIsometry, instSMulCommClassSubtypePreLpMemAddSubgroup, singleContinuousLinearMap_apply, Orthonormal.linearIsometryEquiv_symm_apply_single_one, infty_smulCommClass, instStarModuleSubtypePreLpMemAddSubgroup, coe_lpPiLpₗᵢ, lsingle_apply, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, coeFn_smul, single_smul, instIsCentralScalarSubtypePreLpMemAddSubgroup, coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, OrthogonalFamily.range_linearIsometry, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, infty_isScalarTower, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, norm_const_smul_le, instIsBoundedSMulSubtypePreLpMemAddSubgroup, OrthogonalFamily.linearIsometry_apply, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, instIsScalarTowerSubtypePreLpMemAddSubgroup, HilbertBasis.hasSum_repr_symm, ext_continuousLinearMap_iff
instMulSubtypePreLpMemAddSubgroupTopENNReal 📖	CompOp	3 math math: coe_ringEquiv_lpBCF, infty_coeFn_mul, coe_ringEquiv_lpBCF_symm
instNormSubtypePreLpMemAddSubgroup 📖	CompOp	26 math math: norm_apply_le_norm, norm_le_of_tsum_le, isLUB_norm, norm_eq_zero_iff, sum_rpow_le_norm_rpow, norm_le_of_forall_le', norm_sum_single, norm_rpow_eq_tsum, norm_const_smul, norm_nonneg', norm_eq_card_dsupport, norm_compl_sum_single, norm_neg, norm_zero, hasSum_norm, norm_le_of_forall_sum_le, norm_le_of_forall_le, tsum_mul_le_mul_norm', norm_single, norm_sub_norm_compl_sub_single, instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, norm_eq_tsum_rpow, norm_const_smul_le, norm_eq_ciSup, equiv_lpPiLp_norm, tsum_mul_le_mul_norm
instNormedSpace 📖	CompOp	—
instStarAddMonoid 📖	CompOp	1 math math: instNormedStarGroupSubtypePreLpMemAddSubgroup
instStarSubtypePreLpMemAddSubgroup 📖	CompOp	3 math math: coeFn_star, instStarModuleSubtypePreLpMemAddSubgroup, star_apply
lsingle 📖	CompOp	1 math math: lsingle_apply
nonUnitalNormedCommRing 📖	CompOp	—
nonUnitalNormedRing 📖	CompOp	3 math math: inftyCStarRing, infty_smulCommClass, infty_isScalarTower
nonUnitalRing 📖	CompOp	2 math math: infty_smulCommClass, infty_isScalarTower
normedAddCommGroup 📖	CompOp	39 math math: IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, instNormedStarGroupSubtypePreLpMemAddSubgroup, inner_eq_tsum, IsHilbertSum.linearIsometryEquiv_symm_apply, IsHilbertSum.hasSum_linearIsometryEquiv_symm, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, hasSum_single, HilbertBasis.hasSum_repr, singleContinuousAddMonoidHom_apply, inner_single_right, coe_lpBCFₗᵢ, OrthogonalFamily.hasSum_linearIsometry, singleContinuousLinearMap_apply, Orthonormal.linearIsometryEquiv_symm_apply_single_one, ext_continuousAddMonoidHom_iff, infty_smulCommClass, coe_lpPiLpₗᵢ, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, inner_single_left, coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, OrthogonalFamily.range_linearIsometry, hasSum_inner, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, infty_isScalarTower, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, isometry_single, completeSpace, instIsBoundedSMulSubtypePreLpMemAddSubgroup, uniformContinuous_coe, OrthogonalFamily.linearIsometry_apply, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, HilbertBasis.hasSum_repr_symm, ext_continuousLinearMap_iff
single 📖	CompOp	28 math math: OrthogonalFamily.linearIsometry_apply_single, norm_sum_single, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, coeFn_single, hasSum_single, single_apply_ne, singleAddMonoidHom_apply, singleContinuousAddMonoidHom_apply, inner_single_right, single_neg, single_zero, singleContinuousLinearMap_apply, Orthonormal.linearIsometryEquiv_symm_apply_single_one, norm_compl_sum_single, single_sub, lsingle_apply, HilbertBasis.repr_symm_single, single_smul, inner_single_left, norm_single, single_add, norm_sub_norm_compl_sub_single, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, IsHilbertSum.linearIsometryEquiv_symm_apply_single, single_apply, isometry_single, single_apply_self
singleAddMonoidHom 📖	CompOp	1 math math: singleAddMonoidHom_apply
singleContinuousAddMonoidHom 📖	CompOp	2 math math: singleContinuousAddMonoidHom_apply, ext_continuousAddMonoidHom_iff
singleContinuousLinearMap 📖	CompOp	2 math math: singleContinuousLinearMap_apply, ext_continuousLinearMap_iff
«termℓ^∞(_)» 📖» "API Documentation")	CompOp	—
«termℓ^∞(_,_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup Pi.addZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike coeFnAddMonoidHom	—	—
coeFn_add 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.add Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	—
coeFn_neg 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.neg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
coeFn_single 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp single Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
coeFn_smul 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup Pi.instSMul	—	—
coeFn_star 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Star.star instStarSubtypePreLpMemAddSubgroup Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	—
coeFn_sub 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.sub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—
coeFn_sum 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Finset.sum AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	AddSubgroup.val_finset_sum
coeFn_zero 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.zero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
coe_lpSubmodule 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	Submodule.toAddSubgroup PreLp instAddCommGroupPreLp instModulePreLp lpSubmodule lp	—	—
completeSpace 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp normedAddCommGroup	—	Metric.complete_of_cauchySeq_tendsto cauchySeq_tendsto_of_complete Pi.complete UniformContinuous.comp_cauchySeq uniformContinuous_coe memℓp_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat CauchySeq.isBounded_range tendsto_lp_of_tendsto_pi
eq_zero' 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.zero	—	instSubsingletonSubtype_mathlib Unique.instSubsingleton
eq_zero_iff_coeFn_eq_zero 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.zero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	ext_iff coeFn_zero
ext 📖	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp	—	—	—
ext_continuousAddMonoidHom 📖	—	ContinuousAddMonoidHom.comp PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid normedAddCommGroup AddCommMonoid.toAddMonoid singleContinuousAddMonoidHom	—	—	ContinuousAddMonoidHom.ext hasSum_single HasSum.tsum_eq SummationFilter.instNeBotUnconditional HasSum.map ContinuousAddMonoidHom.instAddMonoidHomClass ContinuousMap.continuous DFunLike.congr_fun
ext_continuousAddMonoidHom_iff 📖	mathematical	—	ContinuousAddMonoidHom.comp PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid normedAddCommGroup AddCommMonoid.toAddMonoid singleContinuousAddMonoidHom	—	ext_continuousAddMonoidHom
ext_continuousLinearMap 📖	—	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp normedAddCommGroup instModuleSubtypePreLpMemAddSubgroup RingHomCompTriple.ids singleContinuousLinearMap	—	—	RingHomCompTriple.ids ContinuousLinearMap.toContinuousAddMonoidHom_injective ext_continuousAddMonoidHom DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContinuousSemilinearMapClass.toContinuousMapClass
ext_continuousLinearMap_iff 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp normedAddCommGroup instModuleSubtypePreLpMemAddSubgroup RingHomCompTriple.ids singleContinuousLinearMap	—	RingHomCompTriple.ids ext_continuousLinearMap
ext_iff 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp	—	ext
hasSum_norm 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup SummationFilter.unconditional	—	norm_rpow_eq_tsum Summable.hasSum Memℓp.summable memℓp
hasSum_single 📖	mathematical	—	HasSum PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid single SummationFilter.unconditional	—	LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.out ENNReal.toReal_pos LT.lt.ne' hasSum_norm HasSum.eq_1 Metric.tendsto_nhds Filter.Eventually.mono Real.rpow_pos_of_pos Real.rpow_lt_rpow_iff dist_nonneg le_of_lt dist_eq_norm Finset.sum_congr single_neg Finset.sum_neg_distrib neg_sub_neg norm_neg norm_compl_sum_single Real.abs_rpow_of_nonneg norm_nonneg abs_norm dist_comm
inftyCStarRing 📖	mathematical	NormedStarGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing CStarRing	PreLp NonUnitalNormedRing.toNormedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal nonUnitalNormedRing inftyStarRing	—	sq Real.le_sqrt norm_nonneg norm_le_of_forall_le Real.sqrt_nonneg CStarRing.norm_star_mul_self norm_apply_le_norm ENNReal.top_ne_zero
infty_coeFn_intCast 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal AddGroupWithOne.toIntCast inftyRing Pi.instIntCast	—	—
infty_coeFn_mul 📖	mathematical	—	PreLp NonUnitalNormedRing.toNormedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal instMulSubtypePreLpMemAddSubgroupTopENNReal Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	—
infty_coeFn_natCast 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal AddMonoidWithOne.toNatCast inftyRing Pi.instNatCast	—	—
infty_coeFn_one 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal inftyRing Pi.instOne	—	—
infty_coeFn_pow 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring inftyRing Pi.instPow	—	—
infty_isScalarTower 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid IsScalarTower NonUnitalNonAssocSemiring.toDistribSMul	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal normedAddCommGroup fact_one_le_top_ennreal nonUnitalNormedRing instModuleSubtypePreLpMemAddSubgroup nonUnitalRing	—	fact_one_le_top_ennreal ext smul_assoc Pi.isScalarTower'
infty_smulCommClass 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid SMulCommClass NonUnitalNonAssocSemiring.toDistribSMul	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal normedAddCommGroup fact_one_le_top_ennreal nonUnitalNormedRing instModuleSubtypePreLpMemAddSubgroup nonUnitalRing	—	fact_one_le_top_ennreal ext SMulCommClass.smul_comm Pi.smulCommClass'
instIsBoundedSMulSubtypePreLpMemAddSubgroup 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp normedAddCommGroup AddSubgroup.zero instModuleSubtypePreLpMemAddSubgroup	—	IsBoundedSMul.of_norm_smul_le norm_const_smul_le LT.lt.ne' LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.out
instIsCentralScalarPreLp 📖	mathematical	IsCentralScalar SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring	PreLp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPreLp AddCommGroup.toAddCommMonoid instModulePreLp MulOpposite.instNormedRing	—	Pi.isCentralScalar
instIsCentralScalarSubtypePreLpMemAddSubgroup 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid IsCentralScalar MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup MulOpposite.instNormedRing IsBoundedSMul.op	—	IsBoundedSMul.op IsCentralScalar.op_smul_eq_smul instIsCentralScalarPreLp
instIsScalarTowerPreLp 📖	mathematical	IsScalarTower SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	PreLp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPreLp AddCommGroup.toAddCommMonoid instModulePreLp	—	Pi.isScalarTower
instIsScalarTowerSubtypePreLpMemAddSubgroup 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid IsScalarTower	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup	—	smul_assoc instIsScalarTowerPreLp
instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal instNormSubtypePreLpMemAddSubgroup inftyRing	—	NormOneClass.norm_one ciSup_const
instNormedStarGroupSubtypePreLpMemAddSubgroup 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp normedAddCommGroup instStarAddMonoid	—	le_of_eq ENNReal.trichotomy ENNReal.toReal_mono ENNReal.zero_ne_top Fact.elim Mathlib.Meta.NormNum.isNat_le_false Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_zero norm_star norm_eq_tsum_rpow
instSMulCommClassPreLp 📖	mathematical	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	PreLp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPreLp AddCommGroup.toAddCommMonoid instModulePreLp	—	Pi.smulCommClass
instSMulCommClassSubtypePreLpMemAddSubgroup 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid SMulCommClass	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup	—	SMulCommClass.smul_comm instSMulCommClassPreLp
instStarModuleSubtypePreLpMemAddSubgroup 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid StarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instStarSubtypePreLpMemAddSubgroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup	—	ext StarModule.star_smul Pi.instStarModuleForall
isLUB_norm 📖	mathematical	—	IsLUB Real Real.instLE Set.range Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal instNormSubtypePreLpMemAddSubgroup	—	norm_eq_ciSup isLUB_ciSup memℓp
isometry_single 📖	mathematical	—	Isometry PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace normedAddCommGroup single	—	AddMonoidHomClass.isometry_of_norm AddMonoidHom.instAddMonoidHomClass norm_single LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.out
lsingle_apply 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup LinearMap.instFunLike lsingle single	—	—
mem_lp_const_smul 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddCommMonoid instModulePreLp	—	Memℓp.const_smul memℓp
memℓp 📖	mathematical	—	Memℓp PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp	—	Subtype.prop
memℓp_of_tendsto 📖	mathematical	Bornology.IsBounded PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup Set.range Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Memℓp	—	Set.forall_mem_range Bornology.IsBounded.exists_norm_le eq_top_or_lt_top memℓp_infty norm_apply_le_of_tendsto Filter.Eventually.of_forall memℓp_gen' sum_rpow_le_of_tendsto LT.lt.ne
monotone 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	AddSubgroup PreLp AddCommGroup.toAddGroup instAddCommGroupPreLp AddSubgroup.instPartialOrder lp	—	Memℓp.of_exponent_ge
norm_apply_le_norm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup	—	eq_or_ne isLUB_norm ENNReal.toReal_pos Real.rpow_nonneg norm_nonneg Real.rpow_le_rpow_iff norm_nonneg' le_hasSum Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional hasSum_norm
norm_apply_le_of_tendsto 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal instNormSubtypePreLpMemAddSubgroup Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	NormedAddCommGroup.toNorm	—	Filter.Tendsto.norm Filter.Tendsto.comp Continuous.continuousAt continuous_apply le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Eventually.mono LE.le.trans norm_apply_le_norm ENNReal.top_ne_zero
norm_compl_sum_single 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup AddSubgroup.sub Finset.sum AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup single Real.instSub Real.instAddCommMonoid NormedAddCommGroup.toNorm	—	Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing sub_eq_zero_of_eq norm_sub_norm_compl_sub_single Mathlib.Tactic.Ring.neg_congr neg_eq_zero
norm_const_smul 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup Real Real.instMul NormedDivisionRing.toNorm	—	eq_or_ne zero_smul norm_zero norm_zero MulZeroClass.zero_mul le_antisymm norm_const_smul_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg mul_inv_cancel_left₀ norm_ne_zero_iff norm_inv inv_smul_smul₀
norm_const_smul_le 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup Real.instMul NormedRing.toNorm	—	ENNReal.trichotomy isEmpty_or_nonempty eq_zero' smul_zero fact_one_le_top_ennreal norm_zero MulZeroClass.mul_zero isLUB_norm IsLUB.mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_nonneg LE.le.trans norm_smul_le norm_nonneg' NNReal.mul_rpow hasSum_norm HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal hasSum_mono IsOrderedRing.toIsOrderedAddMonoid NNReal.instIsOrderedRing OrderTopology.to_orderClosedTopology NNReal.instOrderTopology coeFn_smul Pi.smul_apply NNReal.rpow_le_rpow nnnorm_smul_le le_of_lt SummationFilter.instNeBotUnconditional NNReal.rpow_le_rpow_iff
norm_eq_card_dsupport 📖	mathematical	—	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal instZeroENNReal instNormSubtypePreLpMemAddSubgroup Real Real.instNatCast Finset.card Set.Finite.toFinset setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Memℓp.finite_dsupport memℓp	—	—
norm_eq_ciSup 📖	mathematical	—	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal instNormSubtypePreLpMemAddSubgroup iSup Real Real.instSupSet NormedAddCommGroup.toNorm	—	—
norm_eq_tsum_rpow 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup Real.instPow tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toNorm SummationFilter.unconditional DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne	—	LT.lt.ne' ENNReal.toReal_pos_iff LT.lt.ne
norm_eq_zero_iff 📖	mathematical	—	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup Real Real.instZero AddSubgroup.zero	—	ENNReal.trichotomy ext Memℓp.finite_dsupport memℓp norm_eq_card_dsupport RCLike.charZero_rclike isEmpty_or_nonempty instSubsingletonSubtype_mathlib Unique.instSubsingleton isLUB_norm le_antisymm norm_nonneg hasSum_norm Real.zero_rpow LT.lt.ne' Real.rpow_nonneg Real.rpow_eq_zero_iff_of_nonneg hasSum_zero_iff_of_nonneg Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instLeAtTopUnconditional SummationFilter.instNeBotUnconditional norm_zero
norm_le_of_forall_le 📖	mathematical	Real Real.instLE Real.instZero Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal	instNormSubtypePreLpMemAddSubgroup	—	isEmpty_or_nonempty eq_zero' norm_zero fact_one_le_top_ennreal norm_le_of_forall_le'
norm_le_of_forall_le' 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal	instNormSubtypePreLpMemAddSubgroup	—	isLUB_norm
norm_le_of_forall_sum_le 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal Real.instLE Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp	instNormSubtypePreLpMemAddSubgroup	—	norm_le_of_tsum_le Summable.tsum_le_of_sum_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid SummationFilter.instNeBotUnconditional Memℓp.summable memℓp
norm_le_of_tendsto 📖	—	Filter.Eventually Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	—	Filter.Eventually.exists LE.le.trans norm_nonneg eq_top_or_lt_top norm_le_of_forall_le norm_apply_le_of_tendsto LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.elim ENNReal.toReal_pos LT.lt.ne' LT.lt.ne norm_le_of_forall_sum_le sum_rpow_le_of_tendsto
norm_le_of_tsum_le 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal Real.instLE tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SummationFilter.unconditional	instNormSubtypePreLpMemAddSubgroup	—	Real.rpow_le_rpow_iff norm_nonneg' norm_rpow_eq_tsum
norm_neg 📖	mathematical	—	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup AddSubgroup.neg	—	ENNReal.trichotomy Memℓp.finite_dsupport memℓp norm_eq_card_dsupport Set.Finite.toFinset.congr_simp isEmpty_or_nonempty eq_zero' neg_zero norm_zero IsLUB.unique isLUB_norm norm_neg HasSum.unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_norm Real.rpow_left_injOn LT.lt.ne' norm_nonneg'
norm_nonneg' 📖	mathematical	—	Real Real.instLE Real.instZero Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup	—	ENNReal.trichotomy Memℓp.finite_dsupport memℓp norm_eq_card_dsupport Real.instIsOrderedRing isEmpty_or_nonempty norm_eq_ciSup Real.iSup_of_isEmpty LE.le.trans norm_nonneg isLUB_norm norm_eq_tsum_rpow Real.rpow_nonneg tsum_nonneg Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal
norm_rpow_eq_tsum 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toNorm SummationFilter.unconditional	—	norm_eq_tsum_rpow Real.rpow_mul tsum_nonneg Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.zero_rpow LT.lt.ne' Real.rpow_le_rpow Mathlib.Meta.Positivity.nonneg_of_isNat Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero norm_nonneg le_of_lt Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.rpow_one
norm_single 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup single NormedAddCommGroup.toNorm	—	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' norm_zero norm_nonneg LT.lt.trans_eq norm_eq_tsum_rpow tsum_eq_single SummationFilter.instLeAtTopUnconditional coeFn_single Pi.single_eq_of_ne Real.zero_rpow LT.lt.ne' one_div Real.rpow_rpow_inv
norm_sub_norm_compl_sub_single 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Real.instSub Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup AddSubgroup.sub Finset.sum AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup single Real.instAddCommMonoid NormedAddCommGroup.toNorm	—	HasSum.unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional HasSum.sub instIsTopologicalAddGroupReal hasSum_norm sub_zero sub_self coeFn_sum Finset.sum_congr Finset.sum_apply Finset.sum_pi_single norm_zero Real.zero_rpow LT.lt.ne' hasSum_sum_of_ne_finset_zero SummationFilter.instLeAtTopUnconditional
norm_sum_single 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup Finset.sum AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup single Real.instAddCommMonoid NormedAddCommGroup.toNorm	—	HasSum.unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_norm coeFn_sum Finset.sum_congr Finset.sum_apply Finset.sum_pi_single norm_zero Real.zero_rpow LT.lt.ne' hasSum_sum_of_ne_finset_zero SummationFilter.instLeAtTopUnconditional
norm_zero 📖	mathematical	—	Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup AddSubgroup.zero Real Real.instZero	—	ENNReal.trichotomy Memℓp.finite_dsupport memℓp norm_eq_card_dsupport Set.Finite.toFinset.congr_simp Set.toFinite_toFinset Set.toFinset_empty CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike norm_zero Real.iSup_const_zero norm_eq_tsum_rpow one_div_ne_zero LT.lt.ne' Real.zero_rpow tsum_zero one_div
singleAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddMonoidHom.instFunLike singleAddMonoidHom single	—	—
singleContinuousAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe ContinuousAddMonoidHom PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid normedAddCommGroup ContinuousAddMonoidHom.instFunLike singleContinuousAddMonoidHom single	—	—
singleContinuousLinearMap_apply 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp normedAddCommGroup instModuleSubtypePreLpMemAddSubgroup ContinuousLinearMap.funLike singleContinuousLinearMap single	—	—
single_add 📖	mathematical	—	single AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.add	—	ext Pi.single_add
single_apply 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp single Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
single_apply_ne 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Pi.single_eq_of_ne
single_apply_self 📖	mathematical	—	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp single	—	Pi.single_eq_same
single_neg 📖	mathematical	—	single NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.neg	—	ext Pi.single_neg
single_smul 📖	mathematical	IsBoundedSMul SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	single PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup	—	ext Pi.single_smul
single_sub 📖	mathematical	—	single SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.sub	—	ext Pi.single_sub
single_zero 📖	mathematical	—	single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddSubgroup.zero	—	ext Pi.single_zero
star_apply 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Star.star instStarSubtypePreLpMemAddSubgroup InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	—
sum_rpow_le_norm_rpow 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Real.instLE Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup	—	norm_rpow_eq_tsum Real.rpow_nonneg norm_nonneg Summable.sum_le_tsum Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional Memℓp.summable memℓp
sum_rpow_le_of_tendsto 📖	mathematical	Filter.Eventually Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup Filter.Tendsto nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Finset.sum Real.instAddCommMonoid Real.instPow NormedAddCommGroup.toNorm ENNReal.toReal	—	LT.lt.ne' LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.elim ENNReal.toReal_pos continuous_finset_sum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_apply Continuous.rpow_const Continuous.norm LT.lt.le le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.Tendsto.comp ContinuousAt.tendsto Continuous.continuousAt Filter.Eventually.mono LE.le.trans sum_rpow_le_norm_rpow Real.rpow_le_rpow norm_nonneg le_of_lt
summable_mul 📖	mathematical	Real.HolderConjugate ENNReal.toReal	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SummationFilter.unconditional	—	tsum_mul_le_mul_norm
tendsto_lp_of_tendsto_pi 📖	—	CauchySeq PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup Nat.instPreorder Filter.Tendsto Filter.atTop nhds Pi.topologicalSpace UniformSpace.toTopologicalSpace	—	—	Filter.HasBasis.tendsto_right_iff Metric.nhds_basis_closedBall Filter.HasBasis.mem_of_mem NormedAddCommGroup.uniformity_basis_dist Filter.Eventually.mono CauchySeq.eventually_eventually norm_le_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat LT.lt.le tendsto_pi_nhds Filter.Tendsto.const_sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Filter.Tendsto.apply_nhds
tsum_mul_le_mul_norm 📖	mathematical	Real.HolderConjugate ENNReal.toReal	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SummationFilter.unconditional Real.instLE tsum instNormSubtypePreLpMemAddSubgroup	—	norm_nonneg hasSum_norm Real.HolderTriple.pos Real.HolderConjugate.symm Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg norm_nonneg' HasSum.summable HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional
tsum_mul_le_mul_norm' 📖	mathematical	Real.HolderConjugate ENNReal.toReal	Real Real.instLE tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SummationFilter.unconditional instNormSubtypePreLpMemAddSubgroup	—	tsum_mul_le_mul_norm
uniformContinuous_coe 📖	mathematical	—	UniformContinuous PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup Pi.uniformSpace	—	LT.lt.ne' LT.lt.trans_le zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Fact.elim uniformContinuous_pi Filter.HasBasis.uniformContinuous_iff NormedAddCommGroup.uniformity_basis_dist norm_apply_le_norm LE.le.trans_lt

---

← Back to Index