SuperpolynomialDecay

📁 Source: Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

Statistics

Metric	Count
Definitions SuperpolynomialDecay	1
Theorems add, congr', const_mul, inv_param_mul, mul, mul_const, mul_param, mul_param_pow, mul_param_zpow, mul_polynomial, param_inv_mul, param_mul, param_pow_mul, param_zpow_mul, polynomial_mul, trans_abs_le, trans_eventuallyLE, trans_eventually_abs_le, superpolynomialDecay_const_mul_iff, superpolynomialDecay_iff_abs_isBoundedUnder, superpolynomialDecay_iff_abs_tendsto_zero, superpolynomialDecay_iff_isBigO, superpolynomialDecay_iff_isLittleO, superpolynomialDecay_iff_norm_tendsto_zero, superpolynomialDecay_iff_superpolynomialDecay_abs, superpolynomialDecay_iff_superpolynomialDecay_norm, superpolynomialDecay_iff_zpow_tendsto_zero, superpolynomialDecay_mul_const_iff, superpolynomialDecay_mul_param_iff, superpolynomialDecay_mul_param_pow_iff, superpolynomialDecay_param_mul_iff, superpolynomialDecay_param_pow_mul_iff, superpolynomialDecay_zero	33
Total	34

Asymptotics

Definitions

Name	Category	Theorems
SuperpolynomialDecay 📖	MathDef	34 math math: SuperpolynomialDecay.param_inv_mul, SuperpolynomialDecay.param_pow_mul, SuperpolynomialDecay.add, superpolynomialDecay_iff_zpow_tendsto_zero, superpolynomialDecay_zero, SuperpolynomialDecay.mul_polynomial, SuperpolynomialDecay.mul, SuperpolynomialDecay.trans_eventuallyLE, superpolynomialDecay_iff_isLittleO, superpolynomialDecay_iff_abs_isBoundedUnder, SuperpolynomialDecay.congr, superpolynomialDecay_mul_param_pow_iff, superpolynomialDecay_iff_isBigO, SuperpolynomialDecay.const_mul, SuperpolynomialDecay.trans_abs_le, superpolynomialDecay_iff_norm_tendsto_zero, SuperpolynomialDecay.trans_eventually_abs_le, SuperpolynomialDecay.inv_param_mul, SuperpolynomialDecay.param_zpow_mul, superpolynomialDecay_mul_const_iff, superpolynomialDecay_param_mul_iff, SuperpolynomialDecay.mul_param_zpow, SuperpolynomialDecay.mul_param, SuperpolynomialDecay.param_mul, superpolynomialDecay_iff_superpolynomialDecay_abs, SuperpolynomialDecay.mul_param_pow, superpolynomialDecay_const_mul_iff, SuperpolynomialDecay.polynomial_mul, SuperpolynomialDecay.mul_const, SuperpolynomialDecay.congr', superpolynomialDecay_param_pow_mul_iff, superpolynomialDecay_iff_abs_tendsto_zero, superpolynomialDecay_mul_param_iff, superpolynomialDecay_iff_superpolynomialDecay_norm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
superpolynomialDecay_const_mul_iff 📖	mathematical	—	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	SuperpolynomialDecay.congr SuperpolynomialDecay.const_mul inv_mul_cancel₀ one_mul
superpolynomialDecay_iff_abs_isBoundedUnder 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Filter.Tendsto.isBoundedUnder_le BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.Tendsto.abs IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing superpolynomialDecay_iff_abs_tendsto_zero tendsto_const_nhds Filter.Tendsto.mul_const IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing tendsto_zero_iff_abs_tendsto_zero Filter.Tendsto.inv_tendsto_atTop MulZeroClass.zero_mul tendsto_of_tendsto_of_tendsto_of_le_of_le' Filter.Eventually.of_forall abs_nonneg IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add Filter.Eventually.mp Filter.eventually_map Filter.Eventually.mono Filter.Tendsto.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Eq.trans_le abs_mul mul_assoc pow_succ' inv_mul_cancel₀ one_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono
superpolynomialDecay_iff_abs_tendsto_zero 📖	mathematical	—	SuperpolynomialDecay CommRing.toCommSemiring Filter.Tendsto abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	tendsto_zero_iff_abs_tendsto_zero IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing
superpolynomialDecay_iff_isBigO 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Semifield.toCommSemiring Field.toSemifield NormedField.toField IsBigO NormedField.toNorm DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	superpolynomialDecay_iff_zpow_tendsto_zero Filter.Tendsto.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing isBigO_of_div_tendsto_nhds Filter.Eventually.mono zpow_ne_zero zpow_neg div_eq_mul_inv mul_comm IsBigO.trans IsBigO.mul NormedDivisionRing.toNormMulClass isBigO_refl IsBigO.of_bound' neg_add_rev zpow_add₀ add_neg_cancel_comm_assoc zpow_one norm_inv instReflLe IsBigO.trans_tendsto Filter.Tendsto.inv_tendsto_atTop
superpolynomialDecay_iff_isLittleO 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Semifield.toCommSemiring Field.toSemifield NormedField.toField IsLittleO NormedField.toNorm DivInvMonoid.toZPow DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing	—	Filter.Tendsto.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing isLittleO_of_tendsto' Filter.Eventually.mono one_div Filter.Tendsto.inv_tendsto_atTop one_mul IsLittleO.mul_isBigO NormedDivisionRing.toNormMulClass superpolynomialDecay_iff_isBigO IsLittleO.trans_isBigO IsBigO.of_bound' le_of_eq zpow_one_add₀ add_sub_cancel norm_zpow IsLittleO.isBigO
superpolynomialDecay_iff_norm_tendsto_zero 📖	mathematical	—	SuperpolynomialDecay UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Semifield.toCommSemiring Field.toSemifield NormedField.toField Filter.Tendsto Real Norm.norm NormedField.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring nhds Real.pseudoMetricSpace Real.instZero	—	tendsto_zero_iff_norm_tendsto_zero
superpolynomialDecay_iff_superpolynomialDecay_abs 📖	mathematical	—	SuperpolynomialDecay CommRing.toCommSemiring abs DistribLattice.toLattice instDistribLatticeOfLinearOrder AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	superpolynomialDecay_iff_abs_tendsto_zero abs_mul IsStrictOrderedRing.toIsOrderedRing abs_pow
superpolynomialDecay_iff_superpolynomialDecay_norm 📖	mathematical	—	SuperpolynomialDecay UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Semifield.toCommSemiring Field.toSemifield NormedField.toField Real Real.pseudoMetricSpace Real.instCommSemiring Norm.norm NormedField.toNorm	—	superpolynomialDecay_iff_norm_tendsto_zero norm_mul NormedDivisionRing.toNormMulClass norm_pow NormedDivisionRing.to_normOneClass
superpolynomialDecay_iff_zpow_tendsto_zero 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Filter.Tendsto Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing nhds MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	CanLift.prf instCanLiftIntNatCastLeOfNat zpow_natCast Filter.Tendsto.comp tendsto_zpow_atTop_zero pow_zero one_mul Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing MulZeroClass.zero_mul
superpolynomialDecay_mul_const_iff 📖	mathematical	—	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	SuperpolynomialDecay.congr SuperpolynomialDecay.mul_const mul_assoc mul_inv_cancel₀ mul_one
superpolynomialDecay_mul_param_iff 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	mul_comm superpolynomialDecay_param_mul_iff
superpolynomialDecay_mul_param_pow_iff 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	mul_comm superpolynomialDecay_param_pow_mul_iff
superpolynomialDecay_param_mul_iff 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	SuperpolynomialDecay.congr' SuperpolynomialDecay.inv_param_mul Filter.Eventually.mono Filter.Tendsto.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing inv_mul_cancel₀ one_mul SuperpolynomialDecay.param_mul
superpolynomialDecay_param_pow_mul_iff 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	pow_zero one_mul pow_succ mul_comm mul_assoc superpolynomialDecay_param_mul_iff
superpolynomialDecay_zero 📖	mathematical	—	SuperpolynomialDecay Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	MulZeroClass.mul_zero tendsto_const_nhds

Asymptotics.SuperpolynomialDecay

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	mul_add Distrib.leftDistribClass add_zero Filter.Tendsto.add
congr' 📖	mathematical	Asymptotics.SuperpolynomialDecay Filter.EventuallyEq	Asymptotics.SuperpolynomialDecay	—	Filter.Tendsto.congr' Filter.EventuallyEq.mul Filter.EventuallyEq.refl
const_mul 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	congr mul_const mul_comm
inv_param_mul 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield	Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	zpow_neg zpow_one param_zpow_mul
mul 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	pow_zero one_mul mul_assoc MulZeroClass.mul_zero Filter.Tendsto.mul
mul_const 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	MulZeroClass.zero_mul Filter.Tendsto.mul_const instSeparatelyContinuousMulOfContinuousMul
mul_param 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	congr param_mul mul_comm
mul_param_pow 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	congr param_pow_mul mul_comm
mul_param_zpow 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield	Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing	—	congr param_zpow_mul mul_comm
mul_polynomial 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.eval	—	congr polynomial_mul mul_comm
param_inv_mul 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield	Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	congr inv_param_mul mul_comm
param_mul 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	tendsto_nhds Filter.sets_of_superset
param_pow_mul 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.instPow Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	pow_zero one_mul pow_succ' mul_assoc param_mul
param_zpow_mul 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield	Asymptotics.SuperpolynomialDecay Semifield.toCommSemiring Field.toSemifield Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing	—	Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero Filter.Tendsto.congr' Filter.Eventually.mono Filter.Tendsto.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing IsSimpleRing.instNontrivial DivisionRing.isSimpleRing zpow_add₀ mul_assoc
polynomial_mul 📖	mathematical	Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.eval	—	Polynomial.induction_on' Polynomial.eval_add add_mul Distrib.rightDistribClass add Polynomial.eval_monomial mul_assoc const_mul param_pow_mul
trans_abs_le 📖	mathematical	Asymptotics.SuperpolynomialDecay CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	Asymptotics.SuperpolynomialDecay CommRing.toCommSemiring	—	trans_eventually_abs_le Filter.Eventually.of_forall
trans_eventuallyLE 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Asymptotics.SuperpolynomialDecay	Asymptotics.SuperpolynomialDecay	—	tendsto_of_tendsto_of_tendsto_of_le_of_le' Filter.mp_mem Filter.univ_mem' mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono pow_nonneg IsOrderedRing.toZeroLEOneClass
trans_eventually_abs_le 📖	mathematical	Asymptotics.SuperpolynomialDecay CommRing.toCommSemiring Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	Asymptotics.SuperpolynomialDecay CommRing.toCommSemiring	—	Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds Filter.Eventually.of_forall abs_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing covariant_swap_add_of_covariant_add Filter.Eventually.mono abs_mul mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono

---

← Back to Index