expGrowthSup_const

Mathlib.Analysis.Asymptotics.ExpGrowth

URI: https://scilib.ai/kg/mathlib#ExpGrowth.expGrowthSup_const

← MathLib Explorer

English

If b ≠ 0 and b ≠ ∞, then expGrowthSup (n ↦ b) = 0.

Русский

Если b ≠ 0 и b ≠ ∞, то expGrowthSup (постоянная b) = 0.

LaTeX

$$$b \neq 0 \land b \neq \infty \Rightarrow \expGrowthSup(\lambda n. b) = 0$$$

Lean4

theorem expGrowthSup_const (h : b ≠ 0) (h' : b ≠ ∞) : expGrowthSup (fun _ ↦ b) = 0 :=
  (tendsto_const_div_atTop_nhds_zero_nat (fun k ↦ h (log_eq_bot_iff.1 k)) (fun k ↦ h' (log_eq_top_iff.1 k))).limsup_eq

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

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

Разделы

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

Аффилиация

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