Basic

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

Statistics

Metric	Count
Definitions logCounting, toClosedBall, logCounting	3
Theorems logCounting_divisor_eq_circleAverage_sub_const, logCounting_eval_zero, logCounting_even, logCounting_eventuallyLE, logCounting_eventually_le, logCounting_le, logCounting_mono, logCounting_nonneg, toClosedBall_divisor, toClosedBall_eval_within, toClosedBall_support_subset_closedBall, logCounting_add_analyticOn, logCounting_add_const, logCounting_add_top_eventuallyLE, logCounting_add_top_le, logCounting_coe, logCounting_coe_eq_logCounting_sub_const_zero, logCounting_congr_codiscrete, logCounting_const, logCounting_const_zero, logCounting_eval_zero, logCounting_even, logCounting_eventually_nonneg, logCounting_inv, logCounting_monotoneOn, logCounting_mul_top_eventuallyLE, logCounting_mul_top_le, logCounting_mul_zero_eventuallyLE, logCounting_mul_zero_le, logCounting_nonneg, logCounting_pow_top, logCounting_pow_zero, logCounting_sub_const, logCounting_sum_top_eventuallyLE, logCounting_sum_top_le, logCounting_top, logCounting_top_mul_eventually_le, logCounting_top_mul_le, logCounting_zero, logCounting_zero_mul_eventually_le, logCounting_zero_mul_le, logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, log_counting_zero_sub_logCounting_top, logCounting_divisor	44
Total	47

Function.locallyFinsuppWithin

Definitions

Name	Category	Theorems
logCounting 📖	CompOp	14 math math: ValueDistribution.logCounting_zero, logCounting_nonneg, logCounting_eval_zero, ValueDistribution.logCounting_top, logCounting_eventually_le, logCounting_eventuallyLE, ValueDistribution.characteristic_sub_characteristic_inv, locallyFinsuppWithin.logCounting_divisor, logCounting_divisor_eq_circleAverage_sub_const, logCounting_mono, logCounting_le, ValueDistribution.logCounting_coe, ValueDistribution.log_counting_zero_sub_logCounting_top, logCounting_even
toClosedBall 📖	CompOp	3 math math: toClosedBall_support_subset_closedBall, toClosedBall_divisor, toClosedBall_eval_within

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
logCounting_divisor_eq_circleAverage_sub_const 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike logCounting Complex.instProperSpace MeromorphicOn.divisor Top.top Set BooleanAlgebra.toTop Set.instBooleanAlgebra Real.instSub Real.circleAverage Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex.instNorm Complex.instZero meromorphicTrailingCoeffAt	—	Complex.instProperSpace MeromorphicOn.circleAverage_log_norm zero_sub norm_neg add_sub_cancel_right toClosedBall_divisor MeromorphicOn.divisor_apply dist_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
logCounting_eval_zero 📖	mathematical	—	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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike logCounting Real.instZero	—	MulZeroClass.zero_mul Real.log_zero MulZeroClass.mul_zero finsum_zero add_zero
logCounting_even 📖	mathematical	—	Function.Even Real Real.instNeg 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 SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting	—	restrictMonoidHom_apply dist_zero_right Int.cast_ite Int.cast_zero ite_mul MulZeroClass.zero_mul abs_neg neg_mul Real.log_neg_eq_log
logCounting_eventuallyLE 📖	mathematical	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 instLE Set.univ	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Int.instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' logCounting_le
logCounting_eventually_le 📖	mathematical	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 instLE Set.univ	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Int.instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting	—	logCounting_eventuallyLE
logCounting_le 📖	mathematical	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 instLE Set.univ Real Real.instLE Real.instOne	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Int.instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting	—	sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid map_sub AddMonoidHom.instAddMonoidHomClass logCounting_nonneg instIsOrderedAddMonoid Int.instIsOrderedAddMonoid
logCounting_mono 📖	mathematical	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 instLE Set.univ instZero Int.instAddCommGroup	MonotoneOn Real Real.instPreorder DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting Set.Ioi Real.instZero	—	add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add finiteSupport TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ProperSpace.isCompact_closedBall finsum_eq_sum_of_support_subset Function.support_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike Set.Finite.coe_toFinset Set.mem_of_indicator_ne_zero toClosedBall_eval_within abs_of_pos dist_zero_right 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.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Finset.sum_le_sum dist_self norm_zero inv_zero MulZeroClass.mul_zero Real.log_zero toClosedBall_support_subset_closedBall Set.Finite.mem_toFinset mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.log_le_log mul_pos IsStrictOrderedRing.toPosMulStrictMono inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE norm_pos_iff mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono le_of_lt Int.cast_nonneg Real.instZeroLEOneClass apply_eq_zero_of_notMem Int.cast_zero MulZeroClass.zero_mul mul_nonneg Real.log_nonneg le_mul_inv_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono one_mul
logCounting_nonneg 📖	mathematical	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 instLE Set.univ instZero Int.instAddCommGroup Real Real.instLE Real.instOne	Real.instZero DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass Real.instAddMonoid AddMonoidHom.instFunLike logCounting	—	lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add 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.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing toClosedBall_eval_within dist_self IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add norm_zero inv_zero MulZeroClass.mul_zero Real.log_zero mul_nonneg IsOrderedRing.toPosMulMono Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.log_nonneg mul_comm one_le_inv_mul₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono norm_pos_iff abs_of_pos dist_zero_right apply_eq_zero_of_notMem Int.cast_zero MulZeroClass.zero_mul add_nonneg finsum_nonneg
toClosedBall_divisor 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	MeromorphicOn.divisor Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero abs Real Real.lattice Real.instAddGroup DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing Function.locallyFinsuppWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Set.univ Int.instAddCommGroup AddMonoidHom.instFunLike toClosedBall	—	restrictMonoidHom_apply MeromorphicOn.divisor_restrict
toClosedBall_eval_within 📖	mathematical	Set Set.instMembership Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup abs Real Real.lattice Real.instAddGroup	DFunLike.coe Function.locallyFinsuppWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing instFunLike AddMonoidHom Function.locallyFinsupp AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Set.univ Int.instAddCommGroup AddMonoidHom.instFunLike toClosedBall	—	restrictMonoidHom_apply dist_zero_right
toClosedBall_support_subset_closedBall 📖	mathematical	—	Set Set.instHasSubset support UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Metric.closedBall NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup abs Real Real.lattice Real.instAddGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing DFunLike.coe AddMonoidHom Function.locallyFinsupp Function.locallyFinsuppWithin AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Set.univ Int.instAddCommGroup AddMonoidHom.instFunLike toClosedBall	—	restrictMonoidHom_apply dist_zero_right

ValueDistribution

Definitions

Name	Category	Theorems
logCounting 📖	CompOp	33 math math: logCounting_zero, logCounting_zero_mul_le, logCounting_pow_top, logCounting_eval_zero, logCounting_coe_eq_logCounting_sub_const_zero, logCounting_add_top_le, logCounting_const_zero, logCounting_mul_zero_eventuallyLE, logCounting_top, logCounting_mul_top_eventuallyLE, logCounting_nonneg, logCounting_const, logCounting_sub_const, logCounting_add_analyticOn, logCounting_add_top_eventuallyLE, logCounting_mul_top_le, logCounting_top_mul_eventually_le, logCounting_congr_codiscrete, locallyFinsuppWithin.logCounting_divisor, logCounting_zero_mul_eventually_le, logCounting_sum_top_eventuallyLE, logCounting_add_const, logCounting_top_mul_le, logCounting_pow_zero, logCounting_sum_top_le, logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, logCounting_eventually_nonneg, logCounting_coe, log_counting_zero_sub_logCounting_top, logCounting_monotoneOn, logCounting_inv, logCounting_mul_zero_le, logCounting_even

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
logCounting_add_analyticOn 📖	mathematical	Meromorphic AnalyticOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Set.univ	logCounting Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top	—	MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right Meromorphic.meromorphicOn IsOpen.analyticOn_iff_analyticOnNhd isOpen_univ
logCounting_add_const 📖	mathematical	Meromorphic	logCounting Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top	—	logCounting_add_analyticOn analyticOn_const
logCounting_add_top_eventuallyLE 📖	mathematical	Meromorphic	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder logCounting Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top Real.instAdd	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' logCounting_add_top_le
logCounting_add_top_le 📖	mathematical	Meromorphic Real Real.instLE Real.instOne	logCounting Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top Real.instAdd	—	AddMonoidHom.map_add Function.locallyFinsuppWithin.logCounting_le MeromorphicOn.negPart_divisor_add_le_add Meromorphic.meromorphicOn
logCounting_coe 📖	mathematical	—	logCounting WithTop.some DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike Function.locallyFinsuppWithin.logCounting PosPart.posPart Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instPosPart Function.locallyFinsuppWithin.instLattice instLatticeInt MeromorphicOn.divisor SubNegMonoid.toSub NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—
logCounting_coe_eq_logCounting_sub_const_zero 📖	mathematical	—	logCounting WithTop.some Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup WithTop WithTop.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	WithTop.untop₀_zero sub_zero
logCounting_congr_codiscrete 📖	mathematical	Filter.EventuallyEq Complex Filter.codiscrete UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	logCounting DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instProperSpace	—	Complex.instProperSpace MeromorphicOn.divisor_congr_codiscreteWithin isOpen_univ Filter.mp_mem Filter.univ_mem'
logCounting_const 📖	mathematical	—	logCounting Pi.instZero Real Real.instZero	—	MeromorphicOn.divisor_const negPart_of_nonpos IsOrderedAddMonoid.toAddLeftMono Function.locallyFinsuppWithin.instIsOrderedAddMonoid Int.instIsOrderedAddMonoid neg_zero map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass posPart_zero
logCounting_const_zero 📖	mathematical	—	logCounting Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Real Real.instZero	—	logCounting_const
logCounting_eval_zero 📖	mathematical	—	logCounting Real Real.instZero	—	Function.locallyFinsuppWithin.logCounting_eval_zero
logCounting_even 📖	mathematical	—	Function.Even Real Real.instNeg logCounting	—	Function.locallyFinsuppWithin.logCounting_even
logCounting_eventually_nonneg 📖	mathematical	—	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder Pi.instZero Real.instZero logCounting	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' logCounting_nonneg
logCounting_inv 📖	mathematical	—	logCounting NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace Pi.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield NormedField.toField Top.top WithTop WithTop.top WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	logCounting_top MeromorphicOn.divisor_inv negPart_neg logCounting_zero
logCounting_monotoneOn 📖	mathematical	—	MonotoneOn Real Real.instPreorder logCounting Set.Ioi Real.instZero	—	Function.locallyFinsuppWithin.logCounting_mono negPart_nonneg posPart_nonneg
logCounting_mul_top_eventuallyLE 📖	mathematical	Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop WithTop.top Pi.instAdd Real.instAdd	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' logCounting_mul_top_le
logCounting_mul_top_le 📖	mathematical	Real Real.instLE Real.instOne Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop WithTop.top Pi.instAdd Real.instAdd	—	MeromorphicOn.divisor_mul Meromorphic.meromorphicOn AddMonoidHom.map_add Function.locallyFinsuppWithin.logCounting_le Function.locallyFinsuppWithin.negPart_add Int.instIsOrderedAddMonoid
logCounting_mul_zero_eventuallyLE 📖	mathematical	Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instAdd Real.instAdd	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' logCounting_mul_zero_le
logCounting_mul_zero_le 📖	mathematical	Real Real.instLE Real.instOne Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instAdd Real.instAdd	—	WithTop.untop₀_zero sub_zero MeromorphicOn.divisor_mul Meromorphic.meromorphicOn AddMonoidHom.map_add Function.locallyFinsuppWithin.logCounting_le Function.locallyFinsuppWithin.posPart_add Int.instIsOrderedAddMonoid
logCounting_nonneg 📖	mathematical	Real Real.instLE Real.instOne	Real.instZero logCounting	—	Function.locallyFinsuppWithin.logCounting_nonneg negPart_nonneg posPart_nonneg
logCounting_pow_top 📖	mathematical	Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	logCounting Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Top.top WithTop WithTop.top AddMonoid.toNatSMul Pi.addMonoid Real Real.instAddMonoid	—	MeromorphicOn.divisor_pow Meromorphic.meromorphicOn Function.locallyFinsuppWithin.nsmul_negPart Int.instIsOrderedAddMonoid map_nsmul AddMonoidHom.instAddMonoidHomClass nsmul_eq_mul
logCounting_pow_zero 📖	mathematical	Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	logCounting Pi.instPow Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing AddMonoid.toNatSMul Pi.addMonoid Real Real.instAddMonoid	—	WithTop.untop₀_zero sub_zero MeromorphicOn.divisor_fun_pow Meromorphic.meromorphicOn Function.locallyFinsuppWithin.nsmul_posPart Int.instIsOrderedAddMonoid map_nsmul AddMonoidHom.instAddMonoidHomClass nsmul_eq_mul
logCounting_sub_const 📖	mathematical	Meromorphic	logCounting Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Top.top WithTop WithTop.top	—	sub_eq_add_neg logCounting_add_const
logCounting_sum_top_eventuallyLE 📖	mathematical	Meromorphic	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder logCounting Finset.sum Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top Real.instAddCommMonoid	—	Filter.mp_mem Filter.eventually_ge_atTop Filter.univ_mem' logCounting_sum_top_le
logCounting_sum_top_le 📖	mathematical	Meromorphic Real Real.instLE Real.instOne	logCounting Finset.sum Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Top.top WithTop WithTop.top Real.instAddCommMonoid	—	Finset.induction logCounting_const_zero Finset.sum_apply Finset.sum_insert logCounting_add_top_le Meromorphic.sum add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_refl
logCounting_top 📖	mathematical	—	logCounting Top.top WithTop WithTop.top DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike Function.locallyFinsuppWithin.logCounting NegPart.negPart Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instNegPart Function.locallyFinsuppWithin.instLattice instLatticeInt MeromorphicOn.divisor	—	—
logCounting_top_mul_eventually_le 📖	mathematical	Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop WithTop.top Pi.instAdd Real.instAdd	—	logCounting_mul_top_eventuallyLE
logCounting_top_mul_le 📖	mathematical	Real Real.instLE Real.instOne Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Top.top WithTop WithTop.top Pi.instAdd Real.instAdd	—	logCounting_mul_top_le
logCounting_zero 📖	mathematical	—	logCounting WithTop WithTop.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike Function.locallyFinsuppWithin.logCounting PosPart.posPart Function.locallyFinsuppWithin SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing instPosPart Function.locallyFinsuppWithin.instLattice instLatticeInt MeromorphicOn.divisor	—	WithTop.untop₀_zero sub_zero
logCounting_zero_mul_eventually_le 📖	mathematical	Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	Filter.EventuallyLE Real Real.instLE Filter.atTop Real.instPreorder logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instAdd Real.instAdd	—	logCounting_mul_zero_eventuallyLE
logCounting_zero_mul_le 📖	mathematical	Real Real.instLE Real.instOne Meromorphic NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	logCounting Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing WithTop WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instAdd Real.instAdd	—	logCounting_mul_zero_le
logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const 📖	mathematical	Meromorphic Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	Pi.instSub Real Real.instSub logCounting Complex.instProperSpace WithTop WithTop.zero Complex.instZero Top.top WithTop.top Real.circleAverage Real.normedAddCommGroup Real.instRCLike RCLike.toInnerProductSpaceReal Real.log Norm.norm Complex.instNorm meromorphicTrailingCoeffAt	—	Complex.instProperSpace locallyFinsuppWithin.logCounting_divisor Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const
log_counting_zero_sub_logCounting_top 📖	mathematical	—	DFunLike.coe AddMonoidHom Function.locallyFinsupp UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike Function.locallyFinsuppWithin.logCounting MeromorphicOn.divisor Pi.instSub Real.instSub logCounting WithTop WithTop.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Top.top WithTop.top	—	posPart_sub_negPart IsOrderedAddMonoid.toAddLeftMono Function.locallyFinsuppWithin.instIsOrderedAddMonoid Int.instIsOrderedAddMonoid logCounting_zero logCounting_top map_sub AddMonoidHom.instAddMonoidHomClass

locallyFinsuppWithin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
logCounting_divisor 📖	mathematical	—	DFunLike.coe AddMonoidHom Function.locallyFinsupp Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Int.instNormedCommRing AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Function.locallyFinsuppWithin.instAddCommGroup Set.univ Int.instAddCommGroup Pi.addZeroClass Real Real.instAddMonoid AddMonoidHom.instFunLike Function.locallyFinsuppWithin.logCounting Complex.instProperSpace MeromorphicOn.divisor DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace Top.top Set BooleanAlgebra.toTop Set.instBooleanAlgebra Pi.instSub Real.instSub ValueDistribution.logCounting WithTop WithTop.zero Complex.instZero WithTop.top	—	Complex.instProperSpace WithTop.untop₀_zero sub_zero AddMonoidHom.map_sub posPart_sub_negPart IsOrderedAddMonoid.toAddLeftMono Function.locallyFinsuppWithin.instIsOrderedAddMonoid Int.instIsOrderedAddMonoid

---

← Back to Index