Documentation

PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics

source
theorem Asymptotics.isLittleO_const_id_cocompact {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [ProperSpace F''] (c : E'') :
(fun (_x : F'') => c) =o[Filter.cocompact F''] id
Inspect dependencies

Asymptotics.isLittleO_const_id_cocompact · compiled type and proof/definition references.

source
theorem Asymptotics.isLittleO_const_id_atTop2 {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [LinearOrder F''] [NoMaxOrder F''] [ClosedIciTopology F''] [ProperSpace F''] (c : E'') :
(fun (_x : F'') => c) =o[Filter.atTop] id
Inspect dependencies

Asymptotics.isLittleO_const_id_atTop2 · compiled type and proof/definition references.

source
theorem Asymptotics.isLittleO_const_id_atBot2 {E'' : Type u_9} {F'' : Type u_10} [NormedAddCommGroup E''] [NormedAddCommGroup F''] [LinearOrder F''] [NoMinOrder F''] [ClosedIicTopology F''] [ProperSpace F''] (c : E'') :
(fun (_x : F'') => c) =o[Filter.atBot] id
Inspect dependencies

Asymptotics.isLittleO_const_id_atBot2 · compiled type and proof/definition references.

source
theorem Filter.Eventually.natCast {f : ℝ → Prop} (hf : ∀ᶠ (x : ℝ) in atTop, f x) :
∀ᶠ (n : ℕ) in atTop, f ↑n
Inspect dependencies

Filter.Eventually.natCast · compiled type and proof/definition references.

source
theorem Asymptotics.IsBigO.natCast {E : Type u_3} [Norm E] {f g : ℝ → E} (h : f =O[Filter.atTop] g) :
(fun (n : ℕ) => f ↑n) =O[Filter.atTop] fun (n : ℕ) => g ↑n
Inspect dependencies

Asymptotics.IsBigO.natCast · compiled type and proof/definition references.