lpSpace

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

Statistics

Metric	Count
Definitions Memℓp, PreLp, algebra, unique, instAddCommGroupPreLp, lp, coeFnAddMonoidHom, coeFun, evalCLM, evalₗ, inftyNormedAlgebra, inftyNormedCommRing, inftyNormedRing, inftyRing, inftyStarRing, instAlgebraSubtypePreLpMemAddSubgroupTopENNReal, instInvolutiveStar, instModulePreLp, instModuleSubtypePreLpMemAddSubgroup, instMulSubtypePreLpMemAddSubgroupTopENNReal, instNormSubtypePreLpMemAddSubgroup, instNormedSpace, instStarAddMonoid, instStarSubtypePreLpMemAddSubgroup, linearMapOfLE, lsingle, nonUnitalNormedCommRing, nonUnitalNormedRing, nonUnitalRing, normedAddCommGroup, single, singleAddMonoidHom, singleContinuousAddMonoidHom, singleContinuousLinearMap, toNorm, tsumCLM, zeroBasis, «termℓ^_(_,_)»»), «termℓ²(_,_)»»), «termℓ¹(_,_)»»), «termℓ⁰(_,_)»»), lpInftySubalgebra, lpInftySubring, lpSubmodule	44
Theorems coordinate, coordinate, uniformly_bounded, add, bddAbove, const_mul, const_smul, finite_dsupport, finset_sum, infty_mul, infty_pow, mono, mono', neg, neg_iff, norm, of_exponent_ge, of_norm, star_iff, star_mem, sub, summable, summable_of_one, 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_linearMapOfLE_apply, coe_lpSubmodule, completeSpace, eq_zero', eq_zero_iff_coeFn_eq_zero, evalₗ_apply, 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, linearMapOfLE_comp, lipschitzWith_one_eval, 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_mono, norm_neg, norm_nonneg', norm_rpow_eq_tsum, norm_single, norm_sub_norm_compl_sub_single, norm_sum_single, norm_toNorm, norm_tsum_le, 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, toAddMonoidHom_linearMapOfLE, toNorm_coe, tsumCLM_apply, tsum_mul_le_mul_norm, tsum_mul_le_mul_norm', uniformContinuous_coe, zeroBasis_apply, zeroBasis_repr_apply, zeroBasis_repr_symm_apply_coe, memℓp_gen, memℓp_gen', memℓp_gen_iff, memℓp_gen_iff', memℓp_gen_iff'', memℓp_infty, memℓp_infty_iff, memℓp_norm_iff, memℓp_zero, memℓp_zero_iff, natCast_memℓp_infty, one_memℓp_infty, zero_mem_ℓp', zero_memℓp	138
Total	182

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 dist_eq_norm 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 📖	mathematical	LipschitzWith Real PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real.metricSpace Memℓp Real.normedAddCommGroup Top.top ENNReal instTopENNReal	Memℓp Real 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	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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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	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	Memℓp Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	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	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	Memℓp NonUnitalNormedRing.toNormedAddCommGroup Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Top.top ENNReal instTopENNReal	—	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	Memℓp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Top.top ENNReal instTopENNReal	—	Subring.pow_mem
mono 📖	mathematical	Memℓp Real Real.normedAddCommGroup Real.instLE Norm.norm NormedAddCommGroup.toNorm	Memℓp	—	LE.le.trans Real.le_norm_self ENNReal.trichotomy Set.Finite.subset LT.lt.trans_le memℓp_infty_iff BddAbove.range_mono memℓp_gen_iff Summable.of_norm_bounded Real.instCompleteSpace Real.norm_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.rpow_nonneg norm_nonneg Real.rpow_le_rpow le_of_lt
mono' 📖	mathematical	Memℓp Real Real.instLE Norm.norm NormedAddCommGroup.toNorm	Memℓp	—	mono norm
neg 📖	mathematical	Memℓp	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
norm 📖	mathematical	Memℓp	Memℓp Real Real.normedAddCommGroup Norm.norm NormedAddCommGroup.toNorm	—	memℓp_norm_iff
of_exponent_ge 📖	mathematical	Memℓp ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	Memℓp	—	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
of_norm 📖	mathematical	Memℓp Real Real.normedAddCommGroup Norm.norm NormedAddCommGroup.toNorm	Memℓp	—	memℓp_norm_iff
star_iff 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup	Memℓp Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	star_mem star_star
star_mem 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup Memℓp	Memℓp Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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	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 Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal SummationFilter.unconditional	—	memℓp_gen_iff
summable_of_one 📖	mathematical	Memℓp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Summable ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SummationFilter.unconditional	—	Summable.of_norm Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.rpow_one summable

PreLp

Definitions

Name	Category	Theorems
algebra 📖	CompOp	—
unique 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Memℓp 📖	MathDef	36 math math: Memℓp.const_smul, zero_memℓp, zero_mem_ℓp', memℓp_infty, Memℓp.star_mem, memℓp_zero_iff, memℓp_norm_iff, memℓp_gen_iff, lp.memℓp, Memℓp.mono', Memℓp.finset_sum, memℓp_infty_iff, Memℓp.of_exponent_ge, Memℓp.mono, lp.memℓp_of_tendsto, memℓp_gen, one_memℓp_infty, memℓp_gen_iff'', Memℓp.of_norm, memℓp_gen', algebraMap_memℓp_infty, Memℓp.all, Memℓp.star_iff, intCast_memℓp_infty, memℓp_zero, Memℓp.infty_mul, Memℓp.neg_iff, Memℓp.infty_pow, Memℓp.const_mul, Memℓp.add, LipschitzWith.uniformly_bounded, Memℓp.neg, Memℓp.sub, memℓp_gen_iff', Memℓp.norm, natCast_memℓp_infty
PreLp 📖	CompOp	144 math math: lp.norm_apply_le_norm, lp.coe_linearMapOfLE_apply, lp.norm_le_of_tsum_le, 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_le_of_forall_le', lp.norm_sum_single, lp.toAddMonoidHom_linearMapOfLE, IsHilbertSum.hasSum_linearIsometryEquiv_symm, coe_equiv_lpPiLp_symm, lp.inftyCStarRing, lp.evalₗ_apply, 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, lp.zeroBasis_repr_apply, 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, lp.norm_le_of_tendsto, OrthogonalFamily.hasSum_linearIsometry, lp.instSMulCommClassSubtypePreLpMemAddSubgroup, lp.monotone, lp.singleContinuousLinearMap_apply, LipschitzWith.coordinate, Orthonormal.linearIsometryEquiv_symm_apply_single_one, LipschitzOnWith.extend_lp_infty, 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.lipschitzWith_one_eval, lp.instStarModuleSubtypePreLpMemAddSubgroup, coe_equiv_lpPiLp, lp.zeroBasis_apply, 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.norm_le_of_forall_sum_le, lp.norm_le_of_forall_le, 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, lp.tsumCLM_apply, 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, lp.norm_tsum_le, coe_addEquiv_lpPiLp, lp.infty_isScalarTower, lp.linearMapOfLE_comp, lp.eq_zero', lp.tendsto_lp_of_tendsto_pi, 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.zeroBasis_repr_symm_apply_coe, lp.norm_toNorm, 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.norm_mono, lp.instSMulCommClassPreLp, OrthogonalFamily.linearIsometry_apply, lp.single_apply_self, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, lp.toNorm_coe, lp.instIsScalarTowerSubtypePreLpMemAddSubgroup, HilbertBasis.hasSum_repr_symm, kuratowskiEmbedding.isometry, lp.tsum_mul_le_mul_norm, lp.ext_continuousLinearMap_iff
instAddCommGroupPreLp 📖	CompOp	144 math math: lp.norm_apply_le_norm, lp.coe_linearMapOfLE_apply, lp.norm_le_of_tsum_le, 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_le_of_forall_le', lp.norm_sum_single, lp.toAddMonoidHom_linearMapOfLE, IsHilbertSum.hasSum_linearIsometryEquiv_symm, coe_equiv_lpPiLp_symm, lp.inftyCStarRing, lp.evalₗ_apply, 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, lp.zeroBasis_repr_apply, 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, lp.norm_le_of_tendsto, OrthogonalFamily.hasSum_linearIsometry, lp.instSMulCommClassSubtypePreLpMemAddSubgroup, lp.monotone, lp.singleContinuousLinearMap_apply, LipschitzWith.coordinate, Orthonormal.linearIsometryEquiv_symm_apply_single_one, LipschitzOnWith.extend_lp_infty, 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.lipschitzWith_one_eval, lp.instStarModuleSubtypePreLpMemAddSubgroup, coe_equiv_lpPiLp, lp.zeroBasis_apply, 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.norm_le_of_forall_sum_le, lp.norm_le_of_forall_le, 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, lp.tsumCLM_apply, 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, lp.norm_tsum_le, coe_addEquiv_lpPiLp, lp.infty_isScalarTower, lp.linearMapOfLE_comp, lp.eq_zero', lp.tendsto_lp_of_tendsto_pi, 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.zeroBasis_repr_symm_apply_coe, lp.norm_toNorm, 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.norm_mono, lp.instSMulCommClassPreLp, OrthogonalFamily.linearIsometry_apply, lp.single_apply_self, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, lp.toNorm_coe, lp.instIsScalarTowerSubtypePreLpMemAddSubgroup, HilbertBasis.hasSum_repr_symm, kuratowskiEmbedding.isometry, lp.tsum_mul_le_mul_norm, lp.ext_continuousLinearMap_iff
lp 📖	CompOp	141 math math: lp.norm_apply_le_norm, lp.coe_linearMapOfLE_apply, lp.norm_le_of_tsum_le, 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_le_of_forall_le', lp.norm_sum_single, lp.toAddMonoidHom_linearMapOfLE, IsHilbertSum.hasSum_linearIsometryEquiv_symm, coe_equiv_lpPiLp_symm, lp.inftyCStarRing, lp.evalₗ_apply, 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, lp.zeroBasis_repr_apply, 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, lp.norm_le_of_tendsto, OrthogonalFamily.hasSum_linearIsometry, lp.instSMulCommClassSubtypePreLpMemAddSubgroup, lp.monotone, lp.singleContinuousLinearMap_apply, LipschitzWith.coordinate, Orthonormal.linearIsometryEquiv_symm_apply_single_one, LipschitzOnWith.extend_lp_infty, 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.lipschitzWith_one_eval, lp.instStarModuleSubtypePreLpMemAddSubgroup, coe_equiv_lpPiLp, lp.zeroBasis_apply, 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.norm_le_of_forall_sum_le, lp.norm_le_of_forall_le, 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, lp.tsumCLM_apply, 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, lp.norm_tsum_le, coe_addEquiv_lpPiLp, lp.infty_isScalarTower, lp.linearMapOfLE_comp, lp.eq_zero', lp.tendsto_lp_of_tendsto_pi, 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.zeroBasis_repr_symm_apply_coe, lp.norm_toNorm, 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.norm_mono, OrthogonalFamily.linearIsometry_apply, lp.single_apply_self, IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, coe_algEquiv_lpBCF, GromovHausdorff.eq_toGHSpace_iff, lp.toNorm_coe, 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 NormedRing.toRing RingHom.instFunLike algebraMap Pi.algebra NormedAlgebra.toAlgebra NormedRing.toSeminormedRing 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 Ring.toAddGroupWithOne NormedRing.toRing 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 Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal SummationFilter.unconditional	—	LT.lt.ne' ENNReal.toReal_pos_iff LT.lt.ne
memℓp_gen_iff' 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Memℓp Real Real.instLE Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal tsum UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	—	ENNReal.toReal_pos_iff isLUB_hasSum Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.rpow_nonneg norm_nonneg Summable.hasSum LT.lt.ne' LT.lt.ne memℓp_gen'
memℓp_gen_iff'' 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Memℓp Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm NormedAddCommGroup.toNorm ENNReal.toReal	—	tsum_nonneg Real.instIsOrderedAddMonoid HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.rpow_nonneg norm_nonneg memℓp_gen_iff' memℓp_gen'
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_norm_iff 📖	mathematical	—	Memℓp Real Real.normedAddCommGroup Norm.norm NormedAddCommGroup.toNorm	—	ENNReal.trichotomy norm_norm memℓp_gen_iff
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 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing 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 AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing 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	—
evalCLM 📖	CompOp	—
evalₗ 📖	CompOp	1 math math: evalₗ_apply
inftyNormedAlgebra 📖	CompOp	—
inftyNormedCommRing 📖	CompOp	4 math math: GromovHausdorff.ghDist_eq_hausdorffDist, GromovHausdorff.eq_toGHSpace, KuratowskiEmbedding.embeddingOfSubset_dist_le, GromovHausdorff.eq_toGHSpace_iff
inftyNormedRing 📖	CompOp	9 math math: LipschitzWith.coordinate, LipschitzOnWith.extend_lp_infty, GromovHausdorff.ghDist_eq_hausdorffDist, KuratowskiEmbedding.embeddingOfSubset_isometry, GromovHausdorff.eq_toGHSpace, LipschitzOnWith.coordinate, KuratowskiEmbedding.exists_isometric_embedding, 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
instAlgebraSubtypePreLpMemAddSubgroupTopENNReal 📖	CompOp	2 math math: coe_algEquiv_lpBCF_symm, coe_algEquiv_lpBCF
instInvolutiveStar 📖	CompOp	—
instModulePreLp 📖	CompOp	5 math math: instIsCentralScalarPreLp, coe_lpSubmodule, instIsScalarTowerPreLp, mem_lp_const_smul, instSMulCommClassPreLp
instModuleSubtypePreLpMemAddSubgroup 📖	CompOp	45 math math: coe_linearMapOfLE_apply, IsHilbertSum.surjective_isometry, OrthogonalFamily.linearIsometry_apply_single, IsHilbertSum.linearIsometryEquiv_symm_apply, toAddMonoidHom_linearMapOfLE, IsHilbertSum.hasSum_linearIsometryEquiv_symm, evalₗ_apply, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, norm_const_smul, zeroBasis_repr_apply, HilbertBasis.hasSum_repr, coe_lpBCFₗᵢ, OrthogonalFamily.hasSum_linearIsometry, instSMulCommClassSubtypePreLpMemAddSubgroup, singleContinuousLinearMap_apply, Orthonormal.linearIsometryEquiv_symm_apply_single_one, infty_smulCommClass, instStarModuleSubtypePreLpMemAddSubgroup, zeroBasis_apply, coe_lpPiLpₗᵢ, lsingle_apply, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, coeFn_smul, single_smul, instIsCentralScalarSubtypePreLpMemAddSubgroup, coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, tsumCLM_apply, OrthogonalFamily.range_linearIsometry, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, infty_isScalarTower, linearMapOfLE_comp, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, fourierBasis_repr, zeroBasis_repr_symm_apply_coe, 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	30 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_le_of_tendsto, 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, norm_tsum_le, instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty, norm_eq_tsum_rpow, norm_toNorm, norm_const_smul_le, norm_eq_ciSup, equiv_lpPiLp_norm, norm_mono, tsum_mul_le_mul_norm
instNormedSpace 📖	CompOp	—
instStarAddMonoid 📖	CompOp	1 math math: instNormedStarGroupSubtypePreLpMemAddSubgroup
instStarSubtypePreLpMemAddSubgroup 📖	CompOp	3 math math: coeFn_star, instStarModuleSubtypePreLpMemAddSubgroup, star_apply
linearMapOfLE 📖	CompOp	3 math math: coe_linearMapOfLE_apply, toAddMonoidHom_linearMapOfLE, linearMapOfLE_comp
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	42 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, lipschitzWith_one_eval, coe_lpPiLpₗᵢ, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, inner_single_left, coe_lpBCFₗᵢ_symm, coe_lpPiLpₗᵢ_symm, tsumCLM_apply, OrthogonalFamily.range_linearIsometry, hasSum_inner, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, HilbertBasis.repr_self, infty_isScalarTower, tendsto_lp_of_tendsto_pi, 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	29 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, zeroBasis_apply, 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
toNorm 📖	CompOp	2 math math: norm_toNorm, toNorm_coe
tsumCLM 📖	CompOp	1 math math: tsumCLM_apply
zeroBasis 📖	CompOp	3 math math: zeroBasis_repr_apply, zeroBasis_apply, zeroBasis_repr_symm_apply_coe
«termℓ^_(_,_)» 📖» "API Documentation")	CompOp	—
«termℓ²(_,_)» 📖» "API Documentation")	CompOp	—
«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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup Pi.instSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid	—	—
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 NormedAddCommGroup.toSeminormedAddCommGroup 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_linearMapOfLE_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 ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp DFunLike.coe LinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup LinearMap.instFunLike linearMapOfLE	—	—
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 NormedRing.toRing instAddCommGroupPreLp instModulePreLp lpSubmodule lp	—	—
completeSpace 📖	mathematical	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	CompleteSpace PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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
evalₗ_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 Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleSubtypePreLpMemAddSubgroup LinearMap.instFunLike evalₗ	—	—
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 Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid 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 Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPow Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal.toReal 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	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 Ring.toAddGroupWithOne inftyRing Pi.instIntCast NormedRing.toRing	—	—
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 AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne inftyRing Pi.instNatCast NormedRing.toRing	—	—
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 AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne inftyRing Pi.instOne NormedRing.toRing	—	—
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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring inftyRing Pi.instPow NormedRing.toRing	—	—
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	IsScalarTower PreLp NonUnitalNormedRing.toNormedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup fact_one_le_top_ennreal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing nonUnitalNormedRing instModuleSubtypePreLpMemAddSubgroup NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing 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	SMulCommClass PreLp NonUnitalNormedRing.toNormedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup fact_one_le_top_ennreal ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NonUnitalSeminormedRing.toPseudoMetricSpace NonUnitalNormedRing.toNonUnitalSeminormedRing nonUnitalNormedRing instModuleSubtypePreLpMemAddSubgroup NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing 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	IsBoundedSMul PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing AddSubgroup.zero 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 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	IsCentralScalar PreLp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPreLp DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModulePreLp MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring MulOpposite.instNormedRing	—	—
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	IsCentralScalar PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup MulOpposite MulOpposite.instMonoid MulOpposite.instSemiring MulOpposite.instNormedRing IsBoundedSMul.op SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid	—	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	IsScalarTower PreLp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPreLp DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModulePreLp	—	—
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	IsScalarTower PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup	—	smul_assoc instIsScalarTowerPreLp
instNormOneClassSubtypePreLpMemAddSubgroupTopENNRealOfNonempty 📖	mathematical	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	NormOneClass PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal instNormSubtypePreLpMemAddSubgroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne inftyRing	—	NormOneClass.norm_one ciSup_const
instNormedStarGroupSubtypePreLpMemAddSubgroup 📖	mathematical	NormedStarGroup NormedAddCommGroup.toSeminormedAddCommGroup	NormedStarGroup PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp NormedAddCommGroup.toSeminormedAddCommGroup 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	SMulCommClass PreLp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPreLp DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModulePreLp	—	—
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	SMulCommClass PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction 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	StarModule PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instStarSubtypePreLpMemAddSubgroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction 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
linearMapOfLE_comp 📖	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 ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	LinearMap.comp PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Ring.toSemiring NormedRing.toRing AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids linearMapOfLE LE.le.trans ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder	—	LinearMap.ext RingHomCompTriple.ids LE.le.trans ext
lipschitzWith_one_eval 📖	mathematical	—	LipschitzWith PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace normedAddCommGroup NNReal NNReal.instOne	—	LipschitzWith.mk_one dist_eq_norm norm_apply_le_norm LT.lt.ne' 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 Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction 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 Preorder.toLE PartialOrder.toPreorder 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	Real Real.instLE Norm.norm 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 Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup AddSubgroup.sub Finset.sum AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup single ENNReal.toReal 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup NormedDivisionRing.toNormedRing 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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Module.toDistribMulAction 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 instReflLe IsLUB.mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_nonneg isLUB_norm norm_le_of_forall_le mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing LE.le.trans norm_smul_le norm_nonneg' NNReal.mul_rpow hasSum_norm HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal hasSum_mono IsOrderedRing.toIsOrderedAddMonoid 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 Real.instPow tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddCommGroup.toNorm ENNReal.toReal 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	Real Real.instLE Norm.norm 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	Real Real.instLE Norm.norm 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	Real Real.instLE Norm.norm 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 📖	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	Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup	—	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	Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup	—	Real.rpow_le_rpow_iff norm_nonneg' norm_rpow_eq_tsum
norm_mono 📖	mathematical	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp	Real Real.instLE Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup	—	ENNReal.trichotomy norm_le_of_forall_le norm_nonneg fact_one_le_top_ennreal LE.le.trans norm_apply_le_norm norm_le_of_forall_sum_le norm_nonneg' Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.rpow_le_rpow le_of_lt sum_rpow_le_norm_rpow
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 instReflLe 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 Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup ENNReal.toReal 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.rpow_nonneg norm_nonneg 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 Real.instSub Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup ENNReal.toReal 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 Real.instPow Norm.norm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup Finset.sum AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup single ENNReal.toReal 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_toNorm 📖	mathematical	—	Norm.norm PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp instNormSubtypePreLpMemAddSubgroup toNorm	—	ENNReal.trichotomy Memℓp.finite_dsupport memℓp norm_eq_card_dsupport Set.Finite.toFinset.congr_simp norm_norm norm_eq_tsum_rpow one_div
norm_tsum_le 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal SummationFilter.unconditional instNormSubtypePreLpMemAddSubgroup	—	norm_tsum_le_tsum_norm Summable.of_norm Real.instCompleteSpace norm_norm Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.rpow_one Memℓp.summable norm_eq_tsum_rpow div_self
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 Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid 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 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 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 NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	—
sum_rpow_le_norm_rpow 📖	mathematical	Real Real.instLT Real.instZero ENNReal.toReal	Real Real.instLE Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm NormedAddCommGroup.toNorm PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal.toReal 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	Real Real.instLE Finset.sum Real.instAddCommMonoid Real.instPow Norm.norm 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 📖	mathematical	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.Tendsto PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup	—	Filter.HasBasis.tendsto_right_iff Metric.nhds_basis_closedBall Filter.HasBasis.mem_of_mem NormedAddCommGroup.uniformity_basis_dist Filter.Eventually.mono CauchySeq.eventually_eventually mem_closedBall_iff_norm 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
toAddMonoidHom_linearMapOfLE 📖	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 ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	LinearMap.toAddMonoidHom PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Ring.toSemiring NormedRing.toRing AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup RingHom.id Semiring.toNonAssocSemiring linearMapOfLE AddSubgroup.inclusion monotone	—	AddMonoidHom.ext monotone ext
toNorm_coe 📖	mathematical	—	PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp toNorm Norm.norm NormedAddCommGroup.toNorm	—	—
tsumCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring PreLp AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup normedAddCommGroup fact_one_le_one_ennreal ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleSubtypePreLpMemAddSubgroup ContinuousLinearMap.funLike tsumCLM tsum SummationFilter.unconditional	—	fact_one_le_one_ennreal
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
zeroBasis_apply 📖	mathematical	—	DFunLike.coe Module.Basis PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal instZeroENNReal Ring.toSemiring NormedRing.toRing AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup instModuleSubtypePreLpMemAddSubgroup Semiring.toModule NonUnitalSeminormedRing.isBoundedSMul NonUnitalNormedRing.toNonUnitalSeminormedRing Module.Basis.instFunLike zeroBasis single AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ext NonUnitalSeminormedRing.isBoundedSMul Finsupp.single_apply
zeroBasis_repr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal instZeroENNReal Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModuleSubtypePreLpMemAddSubgroup Semiring.toModule Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike Module.Basis.repr NonUnitalSeminormedRing.isBoundedSMul NonUnitalNormedRing.toNonUnitalSeminormedRing zeroBasis Finsupp.ofSupportFinite	—	NonUnitalSeminormedRing.isBoundedSMul
zeroBasis_repr_symm_apply_coe 📖	mathematical	—	PreLp NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp ENNReal instZeroENNReal DFunLike.coe LinearEquiv Ring.toSemiring NormedRing.toRing RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Finsupp.module Semiring.toModule instModuleSubtypePreLpMemAddSubgroup EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm Module.Basis.repr NonUnitalSeminormedRing.isBoundedSMul NonUnitalNormedRing.toNonUnitalSeminormedRing zeroBasis Finsupp.instFunLike	—	NonUnitalSeminormedRing.isBoundedSMul

---

← Back to Index