Theorems · Theorem · number theory

WeakFEPair.hf_top

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

Defined in

Mathlib.NumberTheory.LSeries.AbstractFuncEq

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace