hf_zero'

Mathlib.NumberTheory.LSeries.AbstractFuncEq

URI: https://scilib.ai/kg/mathlib#StrongFEPair.hf_zero'

← MathLib Explorer

English

Equivalent restatement of hf_top' with the same content in a different language of presentation.

Русский

Эквивалентное утверждение hf_top' в иной формулировке.

LaTeX

$$f = O[atTop] (·^r) (для произвольного r)$$

Lean4

/-- As `x → 0`, `f x` decays faster than any power of `x`. -/
theorem hf_zero' (r : ℝ) : P.f =O[𝓝[>] 0] (· ^ r) := by simpa using (P.hg₀ ▸ P.hf_zero r :)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru