Asymptotic

📁 Source: Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean

Statistics

Metric	Count
Definitions	0
Theorems one_isLittleO_logCounting_single, zero_iff_logCounting_bounded, logCounting_isBigO_one_iff_analyticOnNhd	3
Total	3

Function.locallyFinsuppWithin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_isLittleO_logCounting_single 📖	mathematical	—	Asymptotics.IsLittleO Real Real.norm Filter.atTop Real.instPreorder Pi.instOne Real.instOne DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid Set.univ AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting single	—	Asymptotics.isLittleO_iff abs_one Real.instIsOrderedRing instIsDirectedOrder Real.instArchimedean Real.one_le_exp le_of_lt Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_nonneg inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.le_exp_log Real.exp_monotone le_add_of_le_of_nonneg le_abs_self LT.lt.le inv_pos inv_mul_le_iff₀ mul_one abs_of_nonneg logCounting_nonneg single_pos logCounting_single_eq_log_sub_const Int.cast_one Real.log_exp one_mul IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le logCounting_mono Set.mem_Ioi Real.exp_pos LT.lt.trans_le one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
zero_iff_logCounting_bounded 📖	mathematical	Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.univ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing instLE instZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.univ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing instZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Asymptotics.IsBigO Real Real.norm Filter.atTop Real.instPreorder DFunLike.coe AddMonoidHom Function.locallyFinsupp AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting Pi.instOne Real.instOne	—	map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass Asymptotics.isBigO_of_le' norm_zero CStarRing.norm_of_mem_unitary instCStarRingReal Real.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass mul_one instReflLe Mathlib.Tactic.Contrapose.contrapose₁ exists_single_le_pos lt_of_le_of_ne Asymptotics.isBigO_iff'' Mathlib.Tactic.Push.not_and_eq abs_one Real.instIsOrderedRing instIsDirectedOrder Real.instArchimedean Filter.eventually_atTop Asymptotics.isLittleO_iff one_isLittleO_logCounting_single IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono abs_le_abs_of_nonneg logCounting_nonneg LT.lt.le single_pos logCounting_le le_of_lt mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing abs_of_nonneg logCounting_strictMono

ValueDistribution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
logCounting_isBigO_one_iff_analyticOnNhd 📖	mathematical	Meromorphic	Asymptotics.IsBigO Real Real.norm Filter.atTop Real.instPreorder logCounting Top.top WithTop WithTop.top Pi.instOne Real.instOne AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace toMeromorphicNFOn Set.univ	—	Function.locallyFinsuppWithin.zero_iff_logCounting_bounded negPart_nonneg MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt meromorphicNFOn_toMeromorphicNFOn meromorphicOrderAt_toMeromorphicNFOn Meromorphic.meromorphicOn WithTop.untop₀_nonneg MeromorphicOn.divisor_apply negPart_eq_zero Int.instAddLeftMono Function.locallyFinsuppWithin.negPart_apply IsOrderedAddMonoid.toAddLeftMono Function.locallyFinsuppWithin.instIsOrderedAddMonoid Int.instIsOrderedAddMonoid MeromorphicOn.divisor_of_toMeromorphicNFOn MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd

---

← Back to Index