Theorems · Theorem · complex analysis

Function.locallyFinsuppWithin.logCounting_isBigO_log_of_finite_support

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {D : Function.locallyFinsupp E ℤ},
  (Function.locallyFinsuppWithin.support D).Finite →
    Function.locallyFinsuppWithin.logCounting D =O[Filter.atTop] Real.log

A function with finite support has a logarithmic counting function that is big-O of log.

Defined in: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Cited by: 1 results in Mathlib
Foundations: Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup ProperSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
Set.univstatement · cited by 3,945
AddMonoidHomstatement · cited by 3,230
Filter.atTopstatement and proof · cited by 2,405
Set.Finitestatement and proof · cited by 1,814
Real.logstatement and proof · cited by 939
Asymptotics.IsBigOstatement and proof · cited by 506
map_sumproof · cited by 455
Set.Finite.toFinsetproof · cited by 351
ProperSpacestatement and proof · cited by 190

Cited by1

Results whose statement or proof uses this declaration.

Function.locallyFinsuppWithin.finite_support_iff_logCounting_isBigO_logproof · cited by 1