Theorems · Theorem · number theory

IsStrongFEPair.hf_top

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → ∀ (r : ℝ), P.f =O[Filter.atTop] fun x => x ^ r

As x → ∞, f x decays faster than any power of x.

Defined in

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Cited by

0 results in Mathlib

Foundations

Depth 194 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace