Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems `comp_summable_norm`, `const_smul_left`, `const_smul_self`, `eq_zero_of_norm_pow`, `eq_zero_of_norm_pow_within`, `exists_eq_mul`, `finsetProd`, `isBoundedUnder_le`, `listProd`, `multisetProd`, `natCast_atTop`, `nat_of_atTop`, `of_pow`, `pow_of_le_right`, `smul`, `smul_isLittleO`, `trans_tendsto`, `trans_tendsto_nhds`, `const_smul_left`, `const_smul_self`, `exists_eq_mul`, `right_le_add_of_lt_one`, `right_le_sub_of_lt_one`, `smul`, `const_smul_left`, `exists_eq_mul`, `finsetProd`, `listProd`, `multisetProd`, `natCast_atTop`, `of_tendsto_div_atBot`, `of_tendsto_div_atTop`, `right_isBigO_add`, `right_isBigO_add'`, `right_isBigO_sub`, `smul`, `smul_isBigO`, `tendsto_div_nhds_zero`, `tendsto_inv_smul_nhds_zero`, `tendsto_zero_of_tendsto`, `trans_tendsto`, `bound_of_isBigO_cofinite`, `bound_of_isBigO_nat_atTop`, `continuousAt_iff_isLittleO`, `div_isBoundedUnder_of_isBigO`, `isBigOWith_const_one`, `isBigOWith_iff_exists_eq_mul`, `isBigOWith_mul_iff_isBigOWith_div`, `isBigOWith_of_div_tendsto_nhds`, `isBigOWith_of_eq_mul`, `isBigOWith_pi`, `isBigOWith_principal`, `isBigOWith_top`, `isBigO_atTop_iff_eventually_exists`, `isBigO_atTop_iff_eventually_exists_pos`, `isBigO_cofinite_iff`, `isBigO_const_iff`, `isBigO_const_left_iff_pos_le_norm`, `isBigO_const_of_ne`, `isBigO_const_of_tendsto`, `isBigO_const_one`, `isBigO_const_smul_left`, `isBigO_const_smul_right`, `isBigO_iff_div_isBoundedUnder`, `isBigO_iff_exists_eq_mul`, `isBigO_iff_isBoundedUnder_le_div`, `isBigO_mul_iff_isBigO_div`, `isBigO_nat_atTop_iff`, `isBigO_nat_atTop_induction`, `isBigO_nat_atTop_induction_of_eventually_pos`, `isBigO_of_div_tendsto_nhds`, `isBigO_of_div_tendsto_nhds_of_ne_zero`, `isBigO_one_iff`, `isBigO_one_nat_atTop_iff`, `isBigO_one_nhds_ne_iff`, `isBigO_pi`, `isBigO_principal`, `isBigO_top`, `isLittleO_const_const_iff`, `isLittleO_const_id_atBot`, `isLittleO_const_id_atTop`, `isLittleO_const_id_cobounded`, `isLittleO_const_iff`, `isLittleO_const_iff_isLittleO_one`, `isLittleO_const_left`, `isLittleO_const_left_of_ne`, `isLittleO_const_smul_left`, `isLittleO_const_smul_right`, `isLittleO_id_const`, `isLittleO_id_one`, `isLittleO_iff_exists_eq_mul`, `isLittleO_iff_tendsto`, `isLittleO_iff_tendsto'`, `isLittleO_mul_iff_isLittleO_div`, `isLittleO_norm_pow_id`, `isLittleO_norm_pow_norm_pow`, `isLittleO_of_tendsto`, `isLittleO_of_tendsto'`, `isLittleO_one_iff`, `isLittleO_one_left_iff`, `isLittleO_pi`, `isLittleO_pow_id`, `isLittleO_pow_pow`, `isLittleO_pow_sub_pow_sub`, `isLittleO_pow_sub_sub`, `isLittleO_principal`, `isLittleO_pure`, `isLittleO_top`, `isBigOWith_principal`, `isBigOWith_rev_principal`, `isBigO_principal`, `isBigO_rev_principal`, `isBigO_const`, `isBigO_one`, `isBigO_one`, `isBigOWith_congr`, `isBigO_congr`, `isLittleO_congr`, `tendsto_zero_smul_of_tendsto_zero_of_bounded`, `isBigOWith_congr`, `isBigO_congr`, `isLittleO_congr`, `mul_tendsto_const`, `summable_of_isBigO`, `summable_of_isBigO_nat`	125
Total	125

Asymptotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bound_of_isBigO_cofinite` 📖	mathematical	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.cofinite`	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Norm.norm` `Real.instMul`	—	`IsBigO.exists_pos` `Filter.eventually_cofinite` `IsBigOWith_def` `Finset.exists_le` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Set.Finite.toFinset.congr_simp` `lt_max_iff` `max_mul_of_nonneg` `IsOrderedRing.toMulPosMono` `norm_nonneg` `le_max_iff` `not_le` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff`
`bound_of_isBigO_nat_atTop` 📖	mathematical	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder`	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Norm.norm` `Real.instMul`	—	`bound_of_isBigO_cofinite` `Nat.cofinite_eq_atTop`
`continuousAt_iff_isLittleO` 📖	mathematical	—	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `IsLittleO` `NormedRing.toNorm` `nhds` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `sub_zero`
`div_isBoundedUnder_of_isBigO` 📖	mathematical	`IsBigO` `NormedDivisionRing.toNorm`	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`IsBigO.exists_nonneg` `Filter.eventually_map` `Filter.Eventually.mono` `IsBigOWith.bound` `norm_div` `div_le_of_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg`
`isBigOWith_const_one` 📖	mathematical	—	`IsBigOWith` `Norm.norm`	—	`NormOneClass.norm_one` `mul_one`
`isBigOWith_iff_exists_eq_mul` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`IsBigOWith` `NormedDivisionRing.toNorm` `Filter.Eventually` `Norm.norm` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	—	`Filter.Eventually.mono` `IsBigOWith.bound` `norm_div` `div_le_of_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `Filter.EventuallyEq.symm` `IsBigOWith.eventually_mul_div_cancel` `isBigOWith_of_eq_mul`
`isBigOWith_mul_iff_isBigOWith_div` 📖	mathematical	`Filter.Eventually` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	`IsBigOWith` `NormedDivisionRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`isBigOWith_iff` `Filter.Eventually.congr` `Filter.Eventually.mp` `Filter.Eventually.of_forall` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_div` `mul_div_assoc` `le_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff`
`isBigOWith_of_div_tendsto_nhds` 📖	mathematical	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `Real` `Real.instLT` `Real.instZero` `Real.instInv` `Norm.norm` `NormedDivisionRing.toNorm`	`IsBigOWith`	—	`IsBigOWith_def` `Filter.Eventually.mono` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_norm` `le_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.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `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_zero_add` `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.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `norm_zero` `div_zero` `IsOrderedRing.toPosMulMono` `norm_div` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `IsStrictOrderedRing.toPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `PosMulReflectLE.toPosMulReflectLT` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `norm_pos_iff`
`isBigOWith_of_eq_mul` 📖	mathematical	`Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `SeminormedRing.toNorm` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing`	`IsBigOWith`	—	`IsBigOWith_def` `Filter.EventuallyEq.rw` `Filter.EventuallyEq.symm` `Filter.Eventually.mono` `LE.le.trans` `norm_mul_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg`
`isBigOWith_pi` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`IsBigOWith` `SeminormedAddCommGroup.toNorm` `Pi.seminormedAddCommGroup`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `pi_norm_le_iff_of_nonneg` `Finite.of_fintype`
`isBigOWith_principal` 📖	mathematical	—	`IsBigOWith` `Filter.principal` `Real` `Real.instLE` `Norm.norm` `Real.instMul`	—	`IsBigOWith_def` `Filter.eventually_principal`
`isBigOWith_top` 📖	mathematical	—	`IsBigOWith` `Top.top` `Filter` `Filter.instTop` `Real` `Real.instLE` `Norm.norm` `Real.instMul`	—	`IsBigOWith_def` `Filter.eventually_top`
`isBigO_atTop_iff_eventually_exists` 📖	mathematical	—	`IsBigO` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Filter.Eventually` `Real`	—	`isBigO_iff` `Filter.exists_eventually_atTop` `SemilatticeSup.instIsDirectedOrder`
`isBigO_atTop_iff_eventually_exists_pos` 📖	mathematical	—	`IsBigO` `SeminormedAddCommGroup.toNorm` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Filter.Eventually` `Real` `Real.instLT` `Real.instZero`	—	`SemilatticeSup.instIsDirectedOrder`
`isBigO_cofinite_iff` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.cofinite` `Real` `Real.instLE` `Norm.norm` `Real.instMul`	—	`bound_of_isBigO_cofinite` `norm_zero` `MulZeroClass.mul_zero` `IsBigO.mono` `isBigO_top` `le_top`
`isBigO_const_iff` 📖	mathematical	—	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.EventuallyEq` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	—	`isBigO_zero_right_iff` `IsBigO.isBoundedUnder_le` `eq_or_ne` `Filter.EventuallyEq.trans_isBigO` `isBigO_zero` `Filter.IsBoundedUnder.isBigO_const`
`isBigO_const_left_iff_pos_le_norm` 📖	mathematical	—	`IsBigO` `NormedAddCommGroup.toNorm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instLT` `Real.instZero` `Filter.Eventually` `Real.instLE` `Norm.norm`	—	`IsBigO.exists_pos` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `Filter.Eventually.mono` `IsBigOWith.bound` `div_le_iff₀'` `IsBigO.of_bound` `div_mul_eq_mul_div` `mul_div_assoc` `le_mul_of_one_le_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `one_le_div`
`isBigO_const_of_ne` 📖	mathematical	—	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	—	`IsBigO.isBoundedUnder_le` `Filter.IsBoundedUnder.isBigO_const`
`isBigO_const_of_tendsto` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`IsBigO` `NormedAddCommGroup.toNorm`	—	`Filter.IsBoundedUnder.isBigO_const` `Filter.Tendsto.isBoundedUnder_le` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Filter.Tendsto.norm`
`isBigO_const_one` 📖	mathematical	—	`IsBigO`	—	`IsBigOWith.isBigO` `isBigOWith_const_one`
`isBigO_const_smul_left` 📖	mathematical	—	`IsBigO` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_ne_zero_iff` `isBigO_norm_left` `norm_smul` `isBigO_const_mul_left_iff` `NormedDivisionRing.toNormMulClass`
`isBigO_const_smul_right` 📖	mathematical	—	`IsBigO` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_ne_zero_iff` `isBigO_norm_right` `norm_smul` `isBigO_const_mul_right_iff` `NormedDivisionRing.toNormMulClass`
`isBigO_iff_div_isBoundedUnder` 📖	mathematical	`Filter.Eventually`	`IsBigO` `NormedDivisionRing.toNorm` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`div_isBoundedUnder_of_isBigO` `IsBigO.of_bound` `Filter.Eventually.mp` `norm_div` `Filter.Eventually.mono` `norm_zero` `MulZeroClass.mul_zero` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff`
`isBigO_iff_exists_eq_mul` 📖	mathematical	—	`IsBigO` `NormedDivisionRing.toNorm` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	—	`IsBigO.exists_nonneg` `IsBigOWith.exists_eq_mul` `isBigO_iff_isBigOWith` `isBigOWith_of_eq_mul`
`isBigO_iff_isBoundedUnder_le_div` 📖	mathematical	`Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.IsBoundedUnder` `Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm`	—	`Filter.eventually_congr` `Filter.Eventually.mono` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff`
`isBigO_mul_iff_isBigO_div` 📖	mathematical	`Filter.Eventually` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	`IsBigO` `NormedDivisionRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`isBigO_iff_isBigOWith` `isBigOWith_mul_iff_isBigOWith_div`
`isBigO_nat_atTop_iff` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`IsBigO` `NormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder` `Real` `Real.instLE` `Norm.norm` `Real.instMul`	—	`Nat.cofinite_eq_atTop` `isBigO_cofinite_iff`
`isBigO_nat_atTop_induction` 📖	mathematical	`Filter.Eventually` `Filter.atTop` `Nat.instPreorder` `Real`	`IsBigO` `NormedAddCommGroup.toNorm`	—	`Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.Eventually.and` `Filter.eventually_forall_ge_atTop` `isBigO_iff` `Filter.eventually_ge_atTop` `Finset.nonempty_Icc` `Set.mem_setOf` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Finset.le_sup'` `Finset.mem_def` `norm_nonneg` `Filter.mp_mem` `Filter.univ_mem'` `le_imp_le_of_le_of_le` `le_refl`
`isBigO_nat_atTop_induction_of_eventually_pos` 📖	mathematical	`Filter.Eventually` `Real` `Real.instLE` `Real.instZero` `Filter.atTop` `Nat.instPreorder` `Real.instLT`	`IsBigO` `Real.norm`	—	`isBigO_nat_atTop_induction` `Filter.mp_mem` `Filter.univ_mem'` `Filter.eventually_forall_ge_atTop` `Filter.eventually_ge_atTop`
`isBigO_of_div_tendsto_nhds` 📖	mathematical	`Filter.Eventually` `Filter.Tendsto` `Pi.instDiv` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing`	`IsBigO` `NormedDivisionRing.toNorm`	—	`isBigO_iff_div_isBoundedUnder` `Filter.Tendsto.isBoundedUnder_le` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Filter.Tendsto.norm`
`isBigO_of_div_tendsto_nhds_of_ne_zero` 📖	mathematical	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing`	`IsBigO` `NormedDivisionRing.toNorm`	—	`add_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `LT.lt.ne'` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsBigO_def` `isBigOWith_of_div_tendsto_nhds`
`isBigO_one_iff` 📖	mathematical	—	`IsBigO` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	—	`NormOneClass.norm_one` `mul_one`
`isBigO_one_nat_atTop_iff` 📖	mathematical	—	`IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instOne` `Real.instLE` `Norm.norm`	—	`isBigO_nat_atTop_iff` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `mul_one`
`isBigO_one_nhds_ne_iff` 📖	mathematical	—	`IsBigO` `nhdsWithin` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `nhds`	—	`Filter.mp_mem` `eventually_nhdsWithin_iff` `Filter.univ_mem'` `eq_or_ne` `le_max_right` `LE.le.trans` `le_max_left` `IsBigO.mono` `nhdsWithin_le_nhds`
`isBigO_pi` 📖	mathematical	—	`IsBigO` `SeminormedAddCommGroup.toNorm` `Pi.seminormedAddCommGroup`	—	`Finite.of_fintype` `Filter.eventually_congr` `Filter.eventually_atTop` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `isBigOWith_pi`
`isBigO_principal` 📖	mathematical	—	`IsBigO` `Filter.principal` `Real` `Real.instLE` `Norm.norm` `Real.instMul`	—	—
`isBigO_top` 📖	mathematical	—	`IsBigO` `Top.top` `Filter` `Filter.instTop` `Real` `Real.instLE` `Norm.norm` `Real.instMul`	—	—
`isLittleO_const_const_iff` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`not_tendsto_atTop_of_tendsto_nhds` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `tendsto_const_nhds`
`isLittleO_const_id_atBot` 📖	mathematical	—	`IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Filter.atBot` `Real.instPreorder`	—	`isLittleO_const_left` `Filter.tendsto_abs_atBot_atTop` `Real.instIsOrderedAddMonoid`
`isLittleO_const_id_atTop` 📖	mathematical	—	`IsLittleO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `Filter.atTop` `Real.instPreorder`	—	`isLittleO_const_left` `Filter.tendsto_abs_atTop_atTop`
`isLittleO_const_id_cobounded` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`isLittleO_const_left` `tendsto_norm_cobounded_atTop`
`isLittleO_const_iff` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`isLittleO_const_iff_isLittleO_one` `NormedDivisionRing.to_normOneClass` `isLittleO_one_iff`
`isLittleO_const_iff_isLittleO_one` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm`	—	`IsLittleO.trans_isBigOWith` `isBigOWith_const_one` `norm_pos_iff` `IsLittleO.trans_isBigO` `isBigO_const_const`
`isLittleO_const_left` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Filter.Tendsto` `Real` `Norm.norm` `Filter.atTop` `Real.instPreorder`	—	`eq_or_ne` `isLittleO_const_left_of_ne`
`isLittleO_const_left_of_ne` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `Filter.Tendsto` `Real` `Norm.norm` `Filter.atTop` `Real.instPreorder`	—	`isLittleO_one_left_iff` `NormedDivisionRing.to_normOneClass` `IsBigO.trans_isLittleO` `isBigO_const_const` `isBigO_const_one`
`isLittleO_const_smul_left` 📖	mathematical	—	`IsLittleO` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_ne_zero_iff` `isLittleO_norm_left` `norm_smul` `isLittleO_const_mul_left_iff` `NormedDivisionRing.toNormMulClass`
`isLittleO_const_smul_right` 📖	mathematical	—	`IsLittleO` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`norm_ne_zero_iff` `isLittleO_norm_right` `norm_smul` `isLittleO_const_mul_right_iff` `NormedDivisionRing.toNormMulClass`
`isLittleO_id_const` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`isLittleO_const_iff` `Continuous.tendsto` `continuous_id`
`isLittleO_id_one` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Pi.instOne`	—	`isLittleO_id_const` `one_ne_zero`
`isLittleO_iff_exists_eq_mul` 📖	mathematical	—	`IsLittleO` `NormedDivisionRing.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`IsLittleO.tendsto_div_nhds_zero` `Filter.EventuallyEq.symm` `IsLittleO.eventually_mul_div_cancel` `IsLittleO_def` `isBigOWith_of_eq_mul` `Filter.Eventually.mono` `NormedAddCommGroup.tendsto_nhds_zero` `le_of_lt`
`isLittleO_iff_tendsto` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	`IsLittleO` `NormedDivisionRing.toNorm` `Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	—	`isLittleO_iff_tendsto'` `Filter.Eventually.of_forall`
`isLittleO_iff_tendsto'` 📖	mathematical	`Filter.Eventually`	`IsLittleO` `NormedDivisionRing.toNorm` `Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`IsLittleO.tendsto_div_nhds_zero` `IsLittleO.congr'` `IsLittleO.mul_isBigO` `NormedDivisionRing.toNormMulClass` `isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `isBigO_refl` `Filter.Eventually.mono` `div_mul_cancel_of_imp` `Filter.Eventually.of_forall` `one_mul`
`isLittleO_mul_iff_isLittleO_div` 📖	mathematical	`Filter.Eventually` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	`IsLittleO` `NormedDivisionRing.toNorm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing`	—	`isLittleO_iff_forall_isBigOWith` `isBigOWith_mul_iff_isBigOWith_div`
`isLittleO_norm_pow_id` 📖	mathematical	—	`IsLittleO` `Real` `Real.norm` `SeminormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm`	—	`isLittleO_norm_pow_norm_pow` `isLittleO_norm_right` `pow_one`
`isLittleO_norm_pow_norm_pow` 📖	mathematical	—	`IsLittleO` `Real` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`IsLittleO.comp_tendsto` `isLittleO_pow_pow` `tendsto_norm_zero`
`isLittleO_of_tendsto` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	`IsLittleO` `NormedDivisionRing.toNorm`	—	`isLittleO_iff_tendsto`
`isLittleO_of_tendsto'` 📖	mathematical	`Filter.Eventually` `Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	`IsLittleO` `NormedDivisionRing.toNorm`	—	`isLittleO_iff_tendsto'`
`isLittleO_one_iff` 📖	mathematical	—	`IsLittleO` `SeminormedAddGroup.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SeminormedAddGroup.toAddGroup`	—	`NormOneClass.norm_one` `mul_one` `Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_closedBall` `dist_zero_right`
`isLittleO_one_left_iff` 📖	mathematical	—	`IsLittleO` `Filter.Tendsto` `Real` `Norm.norm` `Filter.atTop` `Real.instPreorder`	—	`isLittleO_iff_nat_mul_le_aux` `NormOneClass.norm_one` `Real.instZeroLEOneClass` `mul_one` `Filter.HasBasis.tendsto_right_iff` `Filter.HasCountableBasis.toHasBasis` `atTop_hasCountableBasis_of_archimedean` `Real.instIsOrderedRing` `Real.instArchimedean`
`isLittleO_pi` 📖	mathematical	—	`IsLittleO` `SeminormedAddCommGroup.toNorm` `Pi.seminormedAddCommGroup`	—	`IsLittleO_def`
`isLittleO_pow_id` 📖	mathematical	—	`IsLittleO` `NormedDivisionRing.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`pow_one` `isLittleO_pow_pow`
`isLittleO_pow_pow` 📖	mathematical	—	`IsLittleO` `NormedDivisionRing.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`lt_iff_exists_add` `Nat.instCanonicallyOrderedAdd` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsBigO.mul_isLittleO` `NormedDivisionRing.toNormMulClass` `isBigO_refl` `IsLittleO.pow` `isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `Filter.tendsto_id` `pow_add` `one_pow` `mul_one`
`isLittleO_pow_sub_pow_sub` 📖	mathematical	—	`IsLittleO` `Real` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`IsLittleO.comp_tendsto` `isLittleO_pow_pow` `tendsto_norm_sub_self`
`isLittleO_pow_sub_sub` 📖	mathematical	—	`IsLittleO` `Real` `Real.norm` `SeminormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`pow_one` `isLittleO_pow_sub_pow_sub`
`isLittleO_principal` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `SeminormedAddCommGroup.toNorm` `Filter.principal` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`norm_le_zero_iff` `Filter.Tendsto.mono_left` `Continuous.tendsto'` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuous_id` `continuous_const` `MulZeroClass.zero_mul` `inf_le_left` `le_of_tendsto_of_tendsto` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `nhdsGT_neBot` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `tendsto_const_nhds` `eventually_nhdsWithin_iff` `Filter.Eventually.of_forall` `Filter.eventually_principal` `IsLittleO.congr'` `isLittleO_zero` `Filter.EventuallyEq.rfl`
`isLittleO_pure` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `Filter` `Filter.instPure` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`isLittleO_congr` `isLittleO_const_const_iff` `Filter.pure_neBot`
`isLittleO_top` 📖	mathematical	—	`IsLittleO` `NormedAddCommGroup.toNorm` `SeminormedAddCommGroup.toNorm` `Top.top` `Filter` `Filter.instTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—

Asymptotics.IsBigO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_summable_norm` 📖	—	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Norm.norm` `SummationFilter.unconditional`	—	—	`summable_of_isBigO` `Real.instCompleteSpace` `comp_tendsto` `norm_norm` `tendsto_zero_iff_norm_tendsto_zero` `Summable.tendsto_cofinite_zero` `instIsTopologicalAddGroupReal`
`const_smul_left` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`isBigOWith` `Asymptotics.IsBigOWith.isBigO` `Asymptotics.IsBigOWith.const_smul_left`
`const_smul_self` 📖	mathematical	—	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.IsBigOWith.isBigO` `Asymptotics.IsBigOWith.const_smul_self`
`eq_zero_of_norm_pow` 📖	mathematical	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`eq_zero_of_norm_pow_within` `nhdsWithin_univ` `Set.mem_univ`
`eq_zero_of_norm_pow_within` 📖	mathematical	`Asymptotics.IsBigO` `Real` `NormedAddCommGroup.toNorm` `Real.norm` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Set` `Set.instMembership`	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`mem_of_mem_nhdsWithin` `eq_zero_imp` `sub_self` `norm_zero` `zero_pow`
`exists_eq_mul` 📖	mathematical	`Asymptotics.IsBigO` `NormedDivisionRing.toNorm`	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	—	`Asymptotics.isBigO_iff_exists_eq_mul`
`finsetProd` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing` `NormedField.toNorm`	`Finset.prod` `CommRing.toCommMonoid` `SeminormedCommRing.toCommRing` `Field.toCommRing` `NormedField.toField`	—	`multisetProd`
`isBoundedUnder_le` 📖	mathematical	`Asymptotics.IsBigO`	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	—	`bound` `Filter.eventually_map`
`listProd` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	—	`NormedDivisionRing.to_normOneClass` `instReflLe` `mul` `NormedDivisionRing.toNormMulClass`
`multisetProd` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing` `NormedField.toNorm`	`Multiset.prod` `CommRing.toCommMonoid` `SeminormedCommRing.toCommRing` `Multiset.map` `Field.toCommRing` `NormedField.toField`	—	`Quotient.mk_surjective` `listProd`
`natCast_atTop` 📖	mathematical	`Asymptotics.IsBigO` `Filter.atTop` `PartialOrder.toPreorder`	`Nat.instPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`comp_tendsto` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing`
`nat_of_atTop` 📖	—	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.atTop` `Nat.instPreorder` `Filter.Eventually`	—	—	`Asymptotics.bound_of_isBigO_nat_atTop` `Asymptotics.isBigO_iff` `Filter.mp_mem` `Filter.univ_mem'` `norm_zero` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`of_pow` 📖	—	`Asymptotics.IsBigO` `NormedDivisionRing.toNorm` `SeminormedRing.toNorm` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Ring.toSemiring` `SeminormedRing.toRing`	—	—	`exists_pos` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.Eventually.and` `Filter.eventually_ge_atTop` `Filter.Tendsto.eventually_ge_atTop` `Filter.tendsto_pow_atTop` `Asymptotics.IsBigOWith.isBigO` `Asymptotics.IsBigOWith.of_pow` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass`
`pow_of_le_right` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `Pi.instOne` `Real.instOne`	`Asymptotics.IsBigO` `Real.norm` `Pi.instPow` `Monoid.toNatPow` `Real.instMonoid`	—	`Asymptotics.IsBigO_def` `Asymptotics.IsBigOWith_def` `Filter.Eventually.mono` `norm_pow` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `abs_eq_self` `Real.instIsOrderedAddMonoid` `LE.le.trans` `zero_le_one` `Real.instZeroLEOneClass` `one_mul` `pow_le_pow_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`smul` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`isBigOWith` `Asymptotics.IsBigOWith.isBigO` `Asymptotics.IsBigOWith.smul`
`smul_isLittleO` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm` `Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`Asymptotics.IsLittleO_def` `exists_pos` `Asymptotics.IsBigOWith.congr_const` `Asymptotics.IsBigOWith.smul` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_div_cancel₀` `ne_of_gt`
`trans_tendsto` 📖	—	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—	`Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `trans_isLittleO`
`trans_tendsto_nhds` 📖	—	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`trans` `Filter.Tendsto.isBigO_one`

Asymptotics.IsBigOWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul_left` 📖	mathematical	`Asymptotics.IsBigOWith` `SeminormedAddCommGroup.toNorm`	`Real` `Real.instMul` `Norm.norm` `SeminormedRing.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`trans` `const_smul_self` `norm_nonneg`
`const_smul_self` 📖	mathematical	—	`Asymptotics.IsBigOWith` `SeminormedAddCommGroup.toNorm` `Norm.norm` `SeminormedRing.toNorm` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.isBigOWith_of_le'` `norm_smul_le`
`exists_eq_mul` 📖	mathematical	`Asymptotics.IsBigOWith` `NormedDivisionRing.toNorm` `Real` `Real.instLE` `Real.instZero`	`Filter.Eventually` `Norm.norm` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	—	`Asymptotics.isBigOWith_iff_exists_eq_mul`
`right_le_add_of_lt_one` 📖	mathematical	`Asymptotics.IsBigOWith` `SeminormedAddCommGroup.toNorm` `Real` `Real.instLT` `Real.instOne`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`congr` `of_neg_left` `neg_right` `right_le_sub_of_lt_one` `neg_sub` `sub_neg_eq_add`
`right_le_sub_of_lt_one` 📖	mathematical	`Asymptotics.IsBigOWith` `SeminormedAddCommGroup.toNorm` `Real` `Real.instLT` `Real.instOne`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`of_bound` `Filter.mem_of_superset` `bound` `mul_comm` `one_div` `div_eq_mul_inv` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_sub` `mul_one` `le_trans` `sub_le_sub_left` `norm_sub_norm_le`
`smul` 📖	mathematical	`Asymptotics.IsBigOWith` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm` `SeminormedAddCommGroup.toNorm`	`Real` `Real.instMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`Asymptotics.IsBigOWith_def` `Filter.mp_mem` `Filter.univ_mem'` `le_trans` `norm_smul_le` `norm_smul` `mul_mul_mul_comm` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `norm_nonneg`

Asymptotics.IsLittleO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_smul_left` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.IsBigO.trans_isLittleO` `Asymptotics.IsBigO.const_smul_self`
`exists_eq_mul` 📖	mathematical	`Asymptotics.IsLittleO` `NormedDivisionRing.toNorm`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Filter.EventuallyEq` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Asymptotics.isLittleO_iff_exists_eq_mul`
`finsetProd` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing` `NormedField.toNorm` `Finset` `Finset.instMembership` `Asymptotics.IsLittleO`	`Finset.prod` `CommRing.toCommMonoid` `SeminormedCommRing.toCommRing` `Field.toCommRing` `NormedField.toField`	—	`multisetProd`
`listProd` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm` `Asymptotics.IsLittleO`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedDivisionRing.toNormedRing`	—	`mul_isBigO` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsBigO.listProd` `Asymptotics.IsBigO.mul_isLittleO`
`multisetProd` 📖	mathematical	`Asymptotics.IsBigO` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing` `NormedField.toNorm` `Multiset` `Multiset.instMembership` `Asymptotics.IsLittleO`	`Multiset.prod` `CommRing.toCommMonoid` `SeminormedCommRing.toCommRing` `Multiset.map` `Field.toCommRing` `NormedField.toField`	—	`Quotient.mk_surjective` `listProd`
`natCast_atTop` 📖	mathematical	`Asymptotics.IsLittleO` `Filter.atTop` `PartialOrder.toPreorder`	`Nat.instPreorder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`comp_tendsto` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing`
`of_tendsto_div_atBot` 📖	mathematical	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Filter.atBot` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Asymptotics.IsLittleO` `NormedField.toNorm`	—	`of_neg_left` `of_tendsto_div_atTop` `Filter.tendsto_neg_atBot_iff` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `div_neg_eq_neg_div` `neg_neg`
`of_tendsto_div_atTop` 📖	mathematical	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Asymptotics.IsLittleO` `NormedField.toNorm`	—	`Asymptotics.isLittleO_of_tendsto'` `Filter.Eventually.mono` `Filter.Tendsto.eventually_ge_atTop` `zero_div` `inv_div` `Filter.Tendsto.comp` `tendsto_inv_atTop_zero`
`right_isBigO_add` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsBigO` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`Asymptotics.IsBigOWith.isBigO` `Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsBigOWith.right_le_add_of_lt_one` `def'` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `one_half_lt_one`
`right_isBigO_add'` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsBigO` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`right_isBigO_add` `add_comm`
`right_isBigO_sub` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm`	`Asymptotics.IsBigO` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`Asymptotics.IsBigOWith.isBigO` `Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsBigOWith.right_le_sub_of_lt_one` `def'` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `one_half_lt_one`
`smul` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`smul_isBigO` `isBigO`
`smul_isBigO` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedRing.toNorm` `NormedDivisionRing.toNorm` `Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	—	`Asymptotics.IsLittleO_def` `Asymptotics.IsBigO.exists_pos` `Asymptotics.IsBigOWith.congr_const` `Asymptotics.IsBigOWith.smul` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `div_mul_cancel₀` `ne_of_gt`
`tendsto_div_nhds_zero` 📖	mathematical	`Asymptotics.IsLittleO` `NormedDivisionRing.toNorm`	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `div_eq_mul_inv` `mul_isBigO` `NormedDivisionRing.toNormMulClass` `Asymptotics.isBigO_refl` `Asymptotics.isBigO_of_le` `norm_div` `NormOneClass.norm_one` `Real.instZeroLEOneClass`
`tendsto_inv_smul_nhds_zero` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm` `NormedDivisionRing.toNorm`	`Filter.Tendsto` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`div_eq_inv_mul` `tendsto_div_nhds_zero` `norm_norm`
`tendsto_zero_of_tendsto` 📖	mathematical	`Asymptotics.IsLittleO` `SeminormedAddCommGroup.toNorm` `NormedDivisionRing.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing`	`SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`trans_isBigO` `Filter.Tendsto.isBigO_one` `NormedDivisionRing.to_normOneClass` `Asymptotics.isLittleO_one_iff`
`trans_tendsto` 📖	—	`Asymptotics.IsLittleO` `NormedAddCommGroup.toNorm` `Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	—	`Asymptotics.IsBigO.trans_tendsto` `isBigO`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigOWith_principal` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `IsCompact`	`Asymptotics.IsBigOWith` `SeminormedAddGroup.toNorm` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `SupSet.sSup` `Real.instSupSet` `Set.image` `Norm.norm` `Filter.principal`	—	`Asymptotics.isBigOWith_principal` `div_mul_cancel₀` `IsCompact.isLUB_sSup` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `IsCompact.image` `IsCompact.image_of_continuousOn` `continuous_norm` `Set.image_nonempty` `Set.mem_image_of_mem`
`isBigOWith_rev_principal` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `NormedAddGroup.toSeminormedAddGroup` `IsCompact`	`Asymptotics.IsBigOWith` `SeminormedAddGroup.toNorm` `NormedAddGroup.toNorm` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Norm.norm` `InfSet.sInf` `Real.instInfSet` `Set.image` `Filter.principal`	—	`Asymptotics.isBigOWith_principal` `mul_comm_div` `IsCompact.image` `IsCompact.image_of_continuousOn` `continuous_norm` `IsCompact.isGLB_sInf` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Set.image_nonempty` `le_mul_of_one_le_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `one_le_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsCompact.sInf_mem` `IsGLB.nonempty` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Ne.lt_of_le` `norm_ne_zero_iff` `Set.mem_image_of_mem`
`isBigO_principal` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `IsCompact`	`Asymptotics.IsBigO` `SeminormedAddGroup.toNorm` `Filter.principal`	—	`Asymptotics.IsBigOWith.isBigO` `isBigOWith_principal`
`isBigO_rev_principal` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `NormedAddGroup.toSeminormedAddGroup` `IsCompact`	`Asymptotics.IsBigO` `SeminormedAddGroup.toNorm` `NormedAddGroup.toNorm` `Filter.principal`	—	`Asymptotics.IsBigOWith.isBigO` `isBigOWith_rev_principal`

Filter.IsBoundedUnder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigO_const` 📖	mathematical	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	`Asymptotics.IsBigO` `NormedAddCommGroup.toNorm`	—	`Asymptotics.IsBigO.trans` `isBigO_one` `NormedDivisionRing.to_normOneClass` `Asymptotics.isBigO_const_const`
`isBigO_one` 📖	mathematical	`Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm`	`Asymptotics.IsBigO`	—	`Asymptotics.isBigO_one_iff`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigO_one` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm`	—	`Filter.IsBoundedUnder.isBigO_one` `isBoundedUnder_le` `BoundedLENhdsClass.of_closedIciTopology` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `norm`

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigOWith_congr` 📖	mathematical	—	`Asymptotics.IsBigOWith` `nhds` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`OpenPartialHomeomorph.isBigOWith_congr`
`isBigO_congr` 📖	mathematical	—	`Asymptotics.IsBigO` `nhds` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Asymptotics.IsBigO_def` `isBigOWith_congr`
`isLittleO_congr` 📖	mathematical	—	`Asymptotics.IsLittleO` `nhds` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `symm`	—	`Asymptotics.IsLittleO_def` `isBigOWith_congr`

NormedField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_zero_smul_of_tendsto_zero_of_bounded` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Filter.IsBoundedUnder` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	`Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `mul_one` `Asymptotics.IsLittleO.smul_isBigO` `NormMulClass.toNormSMulClass` `NormedDivisionRing.toNormMulClass` `Filter.IsBoundedUnder.isBigO_const` `one_ne_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBigOWith_congr` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv`	`Asymptotics.IsBigOWith` `nhds` `toFun'` `symm`	—	`Asymptotics.IsBigOWith.comp_tendsto` `continuousAt` `map_target` `rightInvOn` `ContinuousAt.eq_1` `Asymptotics.IsBigOWith.congr'` `continuousAt_symm` `Filter.Eventually.mono` `eventually_right_inverse`
`isBigO_congr` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv`	`Asymptotics.IsBigO` `nhds` `toFun'` `symm`	—	`Asymptotics.IsBigO_def` `isBigOWith_congr`
`isLittleO_congr` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `toPartialEquiv`	`Asymptotics.IsLittleO` `nhds` `toFun'` `symm`	—	`Asymptotics.IsLittleO_def` `isBigOWith_congr`

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_tendsto_const` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `NormedRing.toNorm` `SummationFilter.unconditional` `Filter.Tendsto` `Filter.cofinite` `nhds` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing`	`ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`summable_of_isBigO` `one_mul` `mul_one` `Asymptotics.IsBigO.mul` `Asymptotics.isBigO_const_mul_self` `Filter.Tendsto.isBigO_one`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`summable_of_isBigO` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional` `Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Real.norm` `Filter.cofinite`	`AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Asymptotics.IsBigO.isBigOWith` `Summable.of_norm_bounded_eventually` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Summable.abs` `Real.instIsOrderedAddMonoid` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `Asymptotics.IsBigOWith.bound`
`summable_of_isBigO_nat` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SummationFilter.unconditional` `Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder`	`AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`summable_of_isBigO` `Nat.cofinite_eq_atTop`

---

← Back to Index